max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
40057 commits 1 branch 0 tags 5.3 GiB
Find a file
Joachim Breitner 402a6096b9
fix: add checkSystem calls to long-running elaboration paths (#13220) 
This PR adds `checkSystem` calls to several code paths that can run for
extended periods without checking for cancellation, heartbeat limits, or
stack overflow. This improves responsiveness of the cancellation
mechanism
in the language server.

Affected paths:
- `simpLoop` step loop (`Simp/Main.lean`)
- `simp` rewrite candidate loops (`Rewrite.lean`)
- `simpAppUsingCongr` argument traversal (`Types.lean`)
- `synthesizeSyntheticMVarsStep` mvar loop (`SyntheticMVars.lean`)
- `abstractNestedProofs` visitor (`AbstractNestedProofs.lean`)
- `transform`/`transformWithCache` visitors (`Transform.lean`)
- LCNF compiler pass runner loop (`LCNF/Main.lean`)
- LCNF checker recursive traversal (`LCNF/Check.lean`)
- `whnfImp` top-level reduction (`WHNF.lean`)

Intentionally *not* instrumented (too hot, measurable regression):
- `whnfCore.go` inner recursion
- `simpImpl` entry point (redundant with `simpLoop`)
- LCNF `simp` inner recursion (0.4% regression on `big_do`)

Also adds a docstring to `checkInterrupted` clarifying its relationship
to
`checkSystem`.

Found using `LEAN_CHECK_SYSTEM_INTERVAL_MS` monitoring from #13218.

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
2026-04-01 12:54:57 +00:00
.claude chore: add safety notes to release command (#13225) 2026-04-01 05:01:00 +00:00
.github fix: make -DLEAN_VERSION_* CMake overrides actually work (#13226) 2026-04-01 05:31:23 +00:00
.vscode chore: replace workspace file with .vscode/ settings (#12770) 2026-03-04 01:10:04 +00:00
doc chore: strip binaries only in release builds (#13208) 2026-03-31 17:18:43 +00:00
images
releases_drafts chore: remove stale release draft notes (#12518) 2026-02-17 19:56:23 +00:00
script fix: make -DLEAN_VERSION_* CMake overrides actually work (#13226) 2026-04-01 05:31:23 +00:00
src fix: add checkSystem calls to long-running elaboration paths (#13220) 2026-04-01 12:54:57 +00:00
stage0 chore: update stage0 2026-04-01 12:56:25 +00:00
tests feat: add deprecated_syntax (#13108) 2026-04-01 10:51:59 +00:00
.gitattributes chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
.gitignore chore: replace workspace file with .vscode/ settings (#12770) 2026-03-04 01:10:04 +00:00
.gitpod.Dockerfile chore: add gitpod configuration (#6382) 2024-12-15 21:38:13 +00:00
.gitpod.yml chore: strip binaries only in release builds (#13208) 2026-03-31 17:18:43 +00:00
.ignore chore: ignore stage0/ (for rg etc.) 2022-03-18 15:28:20 +01:00
CMakeLists.txt chore: use FetchContent for mimalloc source acquisition (#13196) 2026-03-31 18:00:39 +00:00
CMakePresets.json chore: strip binaries only in release builds (#13208) 2026-03-31 17:18:43 +00:00
CODEOWNERS chore: make @hargoniX code owner of the compiler (#10732) 2025-10-10 04:43:38 +00:00
CONTRIBUTING.md chore: migrate pkg tests (#12889) 2026-03-11 18:55:46 +00:00
flake.lock chore: update to c++20 (#12117) 2026-02-11 01:17:40 +00:00
flake.nix chore: add aarch64-darwin to flake (#12915) 2026-03-18 15:55:34 +00:00
lean-toolchain chore: relative lean-toolchains (#12652) 2026-02-25 10:23:35 +00:00
LICENSE
LICENSES feat: bundle leantar with Lean (#12822) 2026-03-09 20:10:59 +00:00
README.md doc: update URLs that are currently pointing to redirects (#10397) 2025-09-17 15:50:07 +00:00
RELEASES.md chore: updates to release_checklist.md (#7817) 2025-04-04 03:45:36 +00:00

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.