Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
56fe75eef4
This PR fixes possible corruption when recovering from memory exhaustion. This code threw an `std::bad_alloc` in the case of memory exhaustion, but left the small allocator in an inconsistent state when doing so. This would mean any code catching and recovering from the allocation failure would likely find itself with a corrupt small allocator. While we could try and make this code exception safe in future, simply making it panic is better than the status quo, and is consistent with how we handle most other allocation failures. changelog-please-rerun-the-changelog-ci |
||
|---|---|---|
| .claude | ||
| .github | ||
| .vscode | ||
| doc | ||
| images | ||
| releases_drafts | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .gitpod.Dockerfile | ||
| .gitpod.yml | ||
| .ignore | ||
| AGENTS.md | ||
| 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.