Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
1884c3b2ed
This PR adds the option `LEAN_MI_SECURE` to our CMake build. It can be configured with values `0` through `4`. Every increment enables additional memory safety mitigations in mimalloc, at the cost of 2%-20% instruction count, depending on the benchmark. The option is disabled by default in our release builds as most of our users do not use the Lean runtime in security sensitive situations. Distributors and organization deploying production Lean code should consider enabling the option as a hardening measure. The effects of the various levels can be found at https://github.com/microsoft/mimalloc/blob/v2.2.7/include/mimalloc/types.h#L56-L60. |
||
|---|---|---|
| .claude | ||
| .github | ||
| .vscode | ||
| doc | ||
| images | ||
| releases_drafts | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .gitpod.Dockerfile | ||
| .gitpod.yml | ||
| .ignore | ||
| CMakeLists.txt | ||
| CMakePresets.json | ||
| CODEOWNERS | ||
| CONTRIBUTING.md | ||
| flake.lock | ||
| flake.nix | ||
| lean-toolchain | ||
| LICENSE | ||
| LICENSES | ||
| README.md | ||
| RELEASES.md | ||
This is the repository for Lean 4.
About
- Quickstart
- Homepage
- Theorem Proving Tutorial
- Functional Programming in Lean
- Documentation Overview
- Language Reference
- Release notes starting at v4.0.0-m3
- Examples
- External Contribution Guidelines
Installation
See Install Lean.
Contributing
Please read our Contribution Guidelines first.
Building from Source
See Building Lean.