Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
d3b04871f5
This PR adds a `Core.checkInterrupted` call in `checkInferTypeCache` on cache miss, allowing cancellation to be detected during large type inference traversals. Previously, `inferTypeImp` could run for >100ms without any interruption check when processing large expressions (e.g. BVDecide proof terms), making IDE cancellation unresponsive. The check is only on cache miss (actual computation), so cache hits have zero overhead. `checkInterrupted` is used instead of the heavier `checkSystem` to minimize performance impact — local benchmarks show no measurable regression on `tests/elab/5664.lean`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> |
||
|---|---|---|
| .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.