Mac Malone
Mac Malone
I noticed `many1Ident` did not pretty print lines during [this](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Fun.20macro.20-.20bulleted.20argument.20lists/near/384908572) Zulip thread. Including `ppLine` within `manyIdent` will help end users get better pretty printer output without needing initmate knowledge of...
Adds `IO.Ref.modfyM` / `IO.Ref.modifyGetM` which are monadic variants of `IO.Ref.modify` (`ST.Prim.Ref.modify`) / `IO.Ref.modifyGet` (`ST.Prim.Ref.modifyGet`). Like them, it uses `ST.Prim.Ref.take` to atomically modify the reference via busy-waiting, but allow users to...
Work-in-progress PR for an alternative TOML configuration file for basic packages. ### Task list * [x] TOML parser * [x] TOML data types * [x] TOML elaborator (Syntax -> data...
This PR contains major changes to `require` DSL, the Lake manifest format, types of dependencies, and the how packages and targets are named. These changes overlap in significant ways, hence...
It has long been requested to better clarify what parts of Lake API are public and which parts are internal implementation details. This change is a small step towards that...
Helpers which I wrote for @hrmacbeth to use in her Mechanics of Proof [package](https://github.com/hrmacbeth/math2001/tree/main) to help with initializing options and attributes for a teaching environment. She suggested I PR these...
**WIP.** Currently implements the polling of finished jobs. Still need to implement printing build captions only when a job actually does something. Also needs integrating with the other refactor touchups.
This improves job captions, the grouping of logs underneath them, and the handling of import errors. It also adds a number of log-related utilities to help achieve this. **Key Changes:**...
Switches the manifest format to use `major.minor.patch` semantic versions. Major version increments indicate breaking changes (e.g., new required fields and semantic changes to existing fields). Minor version increments (after `0.x`)...
Creates a new CLI command `lake install` which adds a package to Lake's new toolchain-local package set. These packages are stored in a `lake-packages` directory in the current Elan toolchain...