Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
c1e76e8976
This PR improves performance of LRAT trimming in bv_decide. The underlying idea is taken from LRAT trimming as implemented in [`lrat-trim`](https://github.com/arminbiere/lrat-trim/t): As we only filter about half to two thirds of the LRAT proof steps anyway, there is no need to use tree or hash maps to store information about them and we can instead use arrays indexed by the proof step directly. This does not meaningfully increase the amount of memory required but makes the trimming step basically disappear from profiles, e.g. `smt/non-incremental/QF_BV/20210312-Bouvier/vlsat3_a72.smt2` [used to](https://share.firefox.dev/41kJTle) have 8% of its time spent in trimming [now](https://share.firefox.dev/3QAKI4w) 1.5%. |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| releases | ||
| 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 | ||
| 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
- Documentation Overview
- Language Reference
- 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).