fix: add checkSystem to LCNF simp

[nomeata]

This PR adds a checkSystem call to the LCNF simplifier's recursive
traversal. This breaks up multi-second gaps (observed up to 1.75s on
big_do.lean) that prevent prompt cancellation in the IDE.

Local benchmarks on big_do and simp_local show no measurable
wall-clock regression with unconditional checking (no amortization
needed).

Found using LEAN_CHECK_SYSTEM_INTERVAL_MS monitoring from #13218.

[nomeata]

!radar

[leanprover-radar]

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]

Ok, this looks cheap enough.

[nomeata]

(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]

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)

[leanprover-bot]

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)

[nomeata]

Looks like my other changes made this one obsolete.

[nomeata]

Wrong, may still be needed.

[nomeata]

!radar

[leanprover-radar]

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]

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]

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]

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.