Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
61a84c96db
This improves job captions, the grouping of logs underneath them, and the handling of import errors. It also adds a number of log-related utilities to help achieve this. **Key Changes:** * Job captions for facets now include the name of the object (e.g., module, library, facet). A caption has also been added to the top-level build of imports (e.g., for the server and `lake lean`). * Stray I/O and errors outside the build job in a build function captioned with `withRegisterJob` (e.g., user-defined targets) will now be properly grouped under that caption instead of ending up under "Computing build jobs". Stray I/O will be converted to a single informational log entry. * Builds no longer fail immediately on erroneous imports. Lake will now attempt to recover as best as possible from any import errors. Information on the import error will appear both in the build of the erroneous import and in the files which transitive import it. For example, uf `Lib.B` imports a missing module `Lib.A`, then the build of `Lib.A` will mention that the file does not exist, and the build of `Lib.B` will mention the bad import of `Lib.A`. Closes #3351. Closes #3809. |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .ignore | ||
| CMakeLists.txt | ||
| 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).