Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
f356d8830e
Following up on #2986, stop running the test suite in ci.yml in quick mode; the test suite is run in the Nix job, and we do not need to run it twice. With a cold nix cache, when `lean` is rebuilt, not much changes, as both jobs take ~20mins. But when `lean` is unchanged, the nix build should be faster, and shaving off the (currently) 4mins in the CI.yaml run should get us to a green PR sooner. Another benefit is that we get the PR release sooner and even get it when the test suite fails, which can be useful if you want to test mathlib or other things before fixing the lean test suite. |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .ignore | ||
| CMakeLists.txt | ||
| CODEOWNERS | ||
| CONTRIBUTING.md | ||
| default.nix | ||
| flake.lock | ||
| flake.nix | ||
| lean-toolchain | ||
| lean.code-workspace | ||
| LICENSE | ||
| LICENSES | ||
| README.md | ||
| RELEASES.md | ||
| shell.nix | ||
This is the repository for Lean 4.
We provide nightly releases and have just begun regular stable point releases.
About
- Quickstart
- Walkthrough installation video
- Quick tour video
- 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.