fix: add checkSystem to LCNF compiler passes by nomeata · Pull Request #13231 · leanprover/lean4

nomeata · 2026-04-01T13:24:11Z

This PR adds checkSystem calls to the LCNF compiler to improve IDE cancellation responsiveness during compilation of large declarations.

Two changes:

Pass.mkPerDeclaration now calls checkSystem before processing each declaration, allowing interruption between declarations.
The LCNF simp pass calls checkSystem every 128 recursive visits, allowing interruption within large single-declaration simplifications.

Note: LCNF simp has its own custom withIncRecDepth (in SimpM.lean) that does not call checkInterrupted, unlike Core.withIncRecDepth. So this checkSystem call is the only cancellation check on this code path.

Performance: unconditional checkSystem added +0.44% instructions on big_do.lean per CI benchmarks. Amortizing to every 128 visits brings overhead to noise level while keeping the max simp gap under ~80M instructions (~14ms at 6 Ginstr/s).

Before (measured with LEAN_CHECK_SYSTEM_INTERVAL_INSN on the instrumentation branch):

Test	Largest LCNF gap	Time at 6 Ginstr/s
`big_do.lean`	12,623M insn (simp)	2.1s
`riscv-ast.lean`	1,162M insn (simp)	194ms
`riscv-ast.lean`	37 gaps total	—

After:

Test	Largest LCNF gap	Time at 6 Ginstr/s
`big_do.lean`	869M insn (resetReuse)	145ms
`riscv-ast.lean`	232M insn (simp)	39ms
`riscv-ast.lean`	reduced gap count	—

Co-Authored-By: Claude Opus 4.6 noreply@anthropic.com

This PR adds a periodic `checkSystem` call to the LCNF simplifier's recursive traversal, checking every 512 visited nodes. This breaks up multi-second gaps (observed up to 2.3s on `big_do.lean`) without measurable performance regression — the amortized cost is effectively zero on benchmarks like `big_do` and `simp_local`. An unconditional `checkSystem` on every node caused a 0.4% instruction count regression, which is why the amortized approach is used instead. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

nomeata · 2026-04-01T13:28:08Z

!radar

leanprover-radar · 2026-04-01T13:28:15Z

Benchmark results for ce6b715 against 978bde4 are in. There are no significant changes. @nomeata

🟥 build//instructions: +3.5G (+0.03%)

Small changes (2🟥)

🟥 build/module/Lean.Compiler.LCNF.Simp.Main//instructions: +146.5M (+2.55%) (reduced significance based on *//lines)
🟥 elab/big_do//instructions: +35.7M (+0.15%)

nomeata · 2026-04-01T14:13:22Z

Ok, this looks cheap enough.

nomeata · 2026-04-01T14:25:31Z

(Taking this off the queue, measurement since shows that 512 may be too rare to get latency into the 50ms area)

mathlib-lean-pr-testing · 2026-04-01T14:32:53Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 978bde4a0f9d260b245e3c131b9202897d896c7b --onto fc0cf68539ad3b481a1802414c22c44506519c9d. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-01 14:32:53)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3c6ea49d0e4ff3a924452809ca5aeb41b0611bef --onto fc0cf68539ad3b481a1802414c22c44506519c9d. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-04 07:50:05)
❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-04-04 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-04 20:39:12)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9efba691e7415dbee9741a2c2a9ea261d5966e62 --onto fc0cf68539ad3b481a1802414c22c44506519c9d. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-05 08:58:19)

leanprover-bot · 2026-04-01T14:32:56Z

Reference manual CI status:

❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 978bde4a0f9d260b245e3c131b9202897d896c7b --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-04-01 14:32:55)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 978bde4a0f9d260b245e3c131b9202897d896c7b --onto 861bc19e0c1c45b5766cc5c9ef0488568368b236. You can force reference manual CI using the force-manual-ci label. (2026-04-03 21:26:29)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 3c6ea49d0e4ff3a924452809ca5aeb41b0611bef --onto 861bc19e0c1c45b5766cc5c9ef0488568368b236. You can force reference manual CI using the force-manual-ci label. (2026-04-04 07:50:06)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-04 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-04-04 20:39:13)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9efba691e7415dbee9741a2c2a9ea261d5966e62 --onto 861bc19e0c1c45b5766cc5c9ef0488568368b236. You can force reference manual CI using the force-manual-ci label. (2026-04-05 08:58:21)

nomeata · 2026-04-03T06:34:50Z

Looks like my other changes made this one obsolete.

nomeata · 2026-04-03T20:27:16Z

Wrong, may still be needed.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

nomeata · 2026-04-04T07:08:01Z

!radar

leanprover-radar · 2026-04-04T07:08:08Z

Benchmark results for 65f5fbf against 3c6ea49 are in. Significant changes detected! @nomeata

🟥 build//instructions: +15.5G (+0.13%)

Medium changes (1🟥)

🟥 elab/big_do//instructions: +104.4M (+0.44%)

Small changes (66🟥)

Too many entries to display here. View the full report on radar instead.

nomeata · 2026-04-04T19:50:00Z

Closing: this PR is no longer needed after #13258 landed on master.

#13258 adds checkInterrupted to Core.withIncRecDepth, which covers the LCNF simp path — the sub-operations within simp (normExpr, normLetDecl, betaReduce, etc.) make CoreM calls that go through Core.withIncRecDepth and get checkInterrupted there.

Verified with a clean build from scratch: zero gaps at 50ms threshold across all 46 elab_bench tests and all previously problematic files (4595_slowdown, simp_local, big_do, aStructPerfIssue, cbv_iter) without any LCNF simp checkSystem.

nomeata · 2026-04-04T19:56:46Z

Reopening — the gap testing was incorrectly run on a branch without the monitoring instrumentation, so the zero-gap results were meaningless. Need to re-verify.

nomeata · 2026-04-04T21:54:02Z

Closing: this PR is no longer needed after #13258 landed on master.

Verified with a clean build on the instrumented branch (joachim/checkSystemTime) which has LEAN_CHECK_SYSTEM_INTERVAL_MS monitoring in both C++ check_system and Lean checkInterrupted. Key findings:

No LCNF simp gaps at any threshold. Core.withIncRecDepth (#13258) calls checkInterrupted, which covers all CoreM sub-operations called within LCNF simp (normExpr, normLetDecl, betaReduce, etc.). The LCNF simp custom withIncRecDepth (SimpM.lean:146) doesn't call checkInterrupted itself, but it doesn't need to — the sub-operations it calls do.

Previously problematic files — zero gaps at 50ms:

4595_slowdown.lean — 0 gaps (was 4621ms before perf: add checkInterrupted to inferType cache miss path #13258)
aStructPerfIssue.lean — 0 gaps
cbv_iter.lean — 0 gaps
simp_local.lean — 0 gaps at 50ms from LCNF simp (remaining 255ms gap is sharecommon in kernel)

Remaining gaps (elab_bench at 50ms) are all outside LCNF simp:

"type checker" — kernel/sharecommon gaps (up to 3.6s on cbv tests)
"interpreter" — Lean interpreter gaps
"Lean elaborator" — elaboration paths not covered by withIncRecDepth

None of these would be helped by adding checkSystem to LCNF simp.

…heckSystem

Add checkSystem calls in two places: - In `Pass.mkPerDeclaration`, check before processing each declaration, so passes over many declarations can be interrupted between them. - In LCNF `simp`, check on every recursive call to the main `simp` function, so large single-declaration simplifications can be interrupted. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

nomeata · 2026-04-05T11:49:19Z

!radar

leanprover-radar · 2026-04-05T11:49:26Z

Benchmark results for 2d50bf9 against 9efba69 are in. Significant changes detected! @nomeata

🟥 build//instructions: +14.9G (+0.12%)

Medium changes (1🟥)

🟥 elab/big_do//instructions: +104.5M (+0.44%)

Small changes (80🟥)

Too many entries to display here. View the full report on radar instead.

nomeata · 2026-04-06T06:35:20Z

!radar

leanprover-radar · 2026-04-06T06:35:37Z

Benchmark results for c494cc2 against 9efba69 are in. There are no significant changes. @nomeata

🟥 build//instructions: +6.3G (+0.05%)

Small changes (1✅, 4🟥)

🟥 build/module/Lean.Compiler.LCNF.PassManager//instructions: +29.5M (+1.25%)
🟥 build/module/Lean.Compiler.LCNF.Simp.Main//instructions: +142.8M (+2.48%) (reduced significance based on *//lines)
🟥 elab/big_do//instructions: +43.7M (+0.18%)
✅ mvcgen/sym/AddSubCancel/500/kernel//wall-clock: -2ms (-1.79%)
🟥 mvcgen/sym/AddSubCancelDeep/100/vcgen//wall-clock: +9ms (+5.88%)

Unconditional checkSystem added +0.44% instructions on big_do.lean. Amortizing to every 128 visits brings overhead to noise level while keeping max simp gap under 10M instructions (~1.7ms at 6 Ginstr/s). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

nomeata · 2026-04-06T08:55:20Z

!radar

leanprover-radar · 2026-04-06T08:55:26Z

Benchmark results for 83b1369 against 9efba69 are in. There are no significant changes. @nomeata

🟥 build//instructions: +5.8G (+0.05%)

Small changes (2✅, 3🟥)

🟥 build/module/Lean.Compiler.LCNF.PassManager//instructions: +29.4M (+1.24%)
🟥 build/module/Lean.Compiler.LCNF.Simp.Main//instructions: +143.6M (+2.49%) (reduced significance based on *//lines)
✅ compiled/ilean_roundtrip//task-clock: -61ms (-4.88%)
✅ compiled/ilean_roundtrip//wall-clock: -62ms (-4.91%)
🟥 elab/big_do//instructions: +37.3M (+0.16%)

This PR adds checkSystem calls to the LCNF compiler to improve IDE cancellation responsiveness during compilation of large declarations. Two changes: 1. `Pass.mkPerDeclaration` now calls `checkSystem` before processing each declaration, allowing interruption between declarations. 2. The LCNF `simp` pass calls `checkSystem` every 128 recursive visits, allowing interruption within large single-declaration simplifications. Note: LCNF simp has its own custom `withIncRecDepth` (in `SimpM.lean`) that does **not** call `checkInterrupted`, unlike `Core.withIncRecDepth`. So this `checkSystem` call is the only cancellation check on this code path. Performance: unconditional `checkSystem` added +0.44% instructions on `big_do.lean` per CI benchmarks. Amortizing to every 128 visits brings overhead to noise level while keeping the max simp gap under ~80M instructions (~14ms at 6 Ginstr/s). **Before** (measured with `LEAN_CHECK_SYSTEM_INTERVAL_INSN` on the instrumentation branch): | Test | Largest LCNF gap | Time at 6 Ginstr/s | |------|------------------|-------------------| | `big_do.lean` | 12,623M insn (simp) | 2.1s | | `riscv-ast.lean` | 1,162M insn (simp) | 194ms | | `riscv-ast.lean` | 37 gaps total | — | **After:** | Test | Largest LCNF gap | Time at 6 Ginstr/s | |------|------------------|-------------------| | `big_do.lean` | 869M insn (resetReuse) | 145ms | | `riscv-ast.lean` | 232M insn (simp) | 39ms | | `riscv-ast.lean` | reduced gap count | — | Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

nomeata requested review from hargoniX and leodemoura as code owners April 1, 2026 13:24

nomeata added the changelog-compiler Compiler, runtime, and FFI label Apr 1, 2026

nomeata added this pull request to the merge queue Apr 1, 2026

nomeata removed this pull request from the merge queue due to a manual request Apr 1, 2026

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 1, 2026

nomeata closed this Apr 3, 2026

nomeata reopened this Apr 3, 2026

nomeata marked this pull request as draft April 3, 2026 20:27

fix: add checkSystem to LCNF simp

65f5fbf

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

nomeata changed the title ~~fix: add amortized checkSystem to LCNF simp~~ fix: add checkSystem to LCNF simp Apr 4, 2026

nomeata mentioned this pull request Apr 4, 2026

feat: add optional check_system interval monitoring #13212

Open

nomeata closed this Apr 4, 2026

nomeata reopened this Apr 4, 2026

nomeata closed this Apr 4, 2026

nomeata reopened this Apr 5, 2026

nomeata and others added 2 commits April 5, 2026 08:08

Merge remote-tracking branch 'origin/master' into joachim/lcnf-simp-c…

87e7819

…heckSystem

nomeata changed the title ~~fix: add checkSystem to LCNF simp~~ fix: add checkSystem to LCNF compiler passes Apr 5, 2026

nomeata force-pushed the joachim/lcnf-simp-checkSystem branch from c494cc2 to 83b1369 Compare April 6, 2026 08:53

nomeata marked this pull request as ready for review April 6, 2026 09:35

nomeata enabled auto-merge April 6, 2026 09:35

nomeata added this pull request to the merge queue Apr 6, 2026

nomeata added the changelog-no Do not include this PR in the release changelog label Apr 6, 2026

Merged via the queue into master with commit c4a664e Apr 6, 2026
30 checks passed

Conversation

nomeata commented Apr 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Apr 1, 2026

Uh oh!

leanprover-radar commented Apr 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Apr 1, 2026

Uh oh!

Uh oh!

nomeata commented Apr 1, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Apr 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Apr 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Apr 3, 2026

Uh oh!

nomeata commented Apr 3, 2026

Uh oh!

nomeata commented Apr 4, 2026

Uh oh!

leanprover-radar commented Apr 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Apr 4, 2026

Uh oh!

nomeata commented Apr 4, 2026

Uh oh!

nomeata commented Apr 4, 2026

Uh oh!

nomeata commented Apr 5, 2026

Uh oh!

leanprover-radar commented Apr 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Apr 6, 2026

Uh oh!

leanprover-radar commented Apr 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Apr 6, 2026

Uh oh!

leanprover-radar commented Apr 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

nomeata commented Apr 1, 2026 •

edited

Loading

leanprover-radar commented Apr 1, 2026 •

edited

Loading

mathlib-lean-pr-testing bot commented Apr 1, 2026 •

edited

Loading

leanprover-bot commented Apr 1, 2026 •

edited

Loading

leanprover-radar commented Apr 4, 2026 •

edited

Loading

leanprover-radar commented Apr 5, 2026 •

edited

Loading

leanprover-radar commented Apr 6, 2026 •

edited

Loading

leanprover-radar commented Apr 6, 2026 •

edited

Loading