Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
eefcbbb37b
When looking at a PR I sometimes wonder which `nightly` release is this based on, and is used for the mathlib testing. Right now, the action uses a label (`toolchain-available`) for this, but a label cannot easily carry more information. It seems a rather simple way to communicate extra information is by setting [commit statuses](https://docs.github.com/en/rest/commits/statuses?apiVersion=2022-11-28#create-a-commit-status); with this change the following statuses will appear in the PR:  One could also use [checks](https://docs.github.com/en/rest/checks/runs?apiVersion=2022-11-28#create-a-check-run) to add more information, even with a nicely formatted markdown description as in [this example](https://github.com/nomeata/lean4/pull/1/checks?check_run_id=20165137082), but it seems there you can’t set a summary that’s visible without an extra click, and Github seems to associate these checks to “the first workflow”, which is odd. So using statuses seems fine here. Often one uses bots writing PR comments for this purpose, but that's a bit noisy (extra notifications etc.), especially for stuff that happens on every PR, but isn’t always interesting/actionable If this works well, we can use this for more pieces of information, and a link can be added as well. |
||
|---|---|---|
| .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.