Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
8fef03d1cc
This is from a ~~pair~~triple programming session with @tydeu and @mhuisi. If stage 1 is built with `-DUSE_LAKE=ON`, the CMake run will generate `lakefile.toml` files for the root, `src`, and `tests`. These Lake configuration files can then be used to build core oleans. While they do not yet allow Lake to be used to build the Lean binaries. they do allow Lake to be used for working interactively with the Lean source. In our preliminary experiments, this allowed updates to `Init.Data.Nat` to be noticed automatically when reloading downstream files, rather than requiring a full manual compiler rebuild. This will make it easier to work on the system. As part of this change, Lake is added to stage 0. This allows Lake to function in `src`, which uses the stage 0 toolchain. --------- Co-authored-by: Mac Malone <tydeu@hatpress.net> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| releases_drafts | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .ignore | ||
| CMakeLists.txt | ||
| CMakePresets.json | ||
| CODEOWNERS | ||
| CONTRIBUTING.md | ||
| 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).