Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
99070bf304
Lake will now update a package's `lean-toolchain` file on `lake update` if it finds the package's direct dependencies use a newer compatible toolchain. To skip this step, use the `--keep-toolchain` CLI option. Closes #2582. Closes #2752. Closes #5615. ### Toolchain update details To determine "newest compatible" toolchain, Lake parses the toolchain listed in the packages' `lean-toolchain` files into four categories: release , nightly, PR, and other. For newness, release toolchains are compared by semantic version (e.g., `"v4.4.0" < "v4.8.0"` and `"v4.6.0-rc1" < "v4.6.0"`) and nightlies are compared by date (e.g., `"nightly-2024-01-10" < "nightly-2014-10-01"`). All other toolchain types and mixtures are incompatible. If there is not a single newest toolchain, Lake will print a warning and continue updating without changing the toolchain. If Lake does find a new toolchain, Lake updates the workspace's `lean-toolchain` file accordingly and restarts the update process on the new Lake. If Elan is detected, it will spawn the new Lake process via `elan run` with the same arguments Lake was initially run with. If Elan is missing, it will prompt the user to restart Lake manually and exit with a special error code (4). ### Other changes To implement this new logic, various other refactors were needed. Here are some key highlights: * Logs emitted during package and workspace loading are now eagerly printed. * The Elan executable used by Lake is now configurable by the `ELAN` environment variable. * The `--lean` CLI option was removed. Use the `LEAN` environment variable instead. * `Package.deps` / `Package.opaqueDeps` have been removed. Use `findPackage?` with a dependency's name instead. * The dependency resolver now uses a pure breadth-first traversal to resolve dependencies. It also resolves dependencies in reverse order, which is done for consistency with targets. Latter targets shadow earlier ones and latter dependencies take precedence over earlier ones. **These changes mean the order of dependencies in a Lake manifest will change after the first `lake update` on this version of Lake.** |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| releases_drafts | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .ignore | ||
| CMakeLists.txt | ||
| CMakePresets.json | ||
| CODEOWNERS | ||
| CONTRIBUTING.md | ||
| debug.log | ||
| flake.lock | ||
| flake.nix | ||
| lean-toolchain | ||
| lean.code-workspace | ||
| LICENSE | ||
| LICENSES | ||
| README.md | ||
| RELEASES.md | ||
This is the repository for Lean 4.
About
- Quickstart
- Homepage
- Theorem Proving Tutorial
- Functional Programming in Lean
- Manual
- Release notes starting at v4.0.0-m3
- Examples
- External Contribution Guidelines
- FAQ
Installation
See Setting Up Lean.
Contributing
Please read our Contribution Guidelines first.
Building from Source
See Building Lean (documentation source: doc/make/index.md).