Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
ffb4c5becf
Adds Reservoir as another possible source of build caches in addition to GitHub releases. If a GitHub release is not configured for a Reservoir dependency, it will attempt download a build cache from Reservoir. Like with GitHub releases, failure will not stop the build and instead issue a warning. Many of the Lake API calls related to these build caches were refactored and renamed, with the old names remaining around as deprecated aliases. Build cache downloads (from Reservoir or GitHub) can now be disabled via the `--no-cache` CLI option or the `LAKE_NO_CACHE` environment variable. A disabled cache can be re-enable with the `--try-cache` CLI option. |
||
|---|---|---|
| .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).