Skip to content

fix: add checkInterrupted to Core.withIncRecDepth#13290

Merged
nomeata merged 1 commit intomasterfrom
joachim/withIncRecDepth-checkInterrupted
Apr 6, 2026
Merged

fix: add checkInterrupted to Core.withIncRecDepth#13290
nomeata merged 1 commit intomasterfrom
joachim/withIncRecDepth-checkInterrupted

Conversation

@nomeata
Copy link
Copy Markdown
Collaborator

@nomeata nomeata commented Apr 6, 2026

This PR adds a checkInterrupted call to Core.withIncRecDepth, so that all recursive CoreM-based operations (inferType, whnf, isDefEq, simp, …) check for cancellation on each recursion step. Previously, these operations could run for seconds without responding to IDE cancellation requests.

This is the single highest-impact change for IDE cancellation responsiveness. It covers all recursive MetaM/TacticM operations at once, eliminating the vast majority of multi-second gaps identified by the LEAN_CHECK_SYSTEM_INTERVAL_MS monitoring in #13212.

Gap measurements pending — will be added after CI benchmarks and instrumented measurement.

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

…sponsiveness

This PR adds a `checkInterrupted` call to `Core.withIncRecDepth`, so that
all recursive CoreM-based operations (inferType, whnf, isDefEq, simp, …)
check for cancellation on each recursion step. Previously, these operations
could run for seconds without responding to IDE cancellation requests.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@nomeata
Copy link
Copy Markdown
Collaborator Author

nomeata commented Apr 6, 2026

!radar

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Apr 6, 2026

Benchmark results for 4d782a6 against c4a664e are in. There are no significant changes. @nomeata

  • 🟥 build//instructions: +2.2G (+0.02%)

Small changes (8🟥)

  • 🟥 build/module/Lean.Compiler.LCNF.ToDecl//instructions: +19.0M (+0.47%)
  • 🟥 build/module/Lean.Elab.PreDefinition.Structural.Preprocess//instructions: +19.7M (+1.69%)
  • 🟥 build/module/Lean.Elab.PreDefinition.WF.FloatRecApp//instructions: +20.3M (+1.86%)
  • 🟥 build/module/Lean.Meta.PProdN//instructions: +24.1M (+0.91%)
  • 🟥 build/module/Lean.Meta.Reduce//instructions: +17.8M (+1.22%)
  • 🟥 build/module/Lean.Meta.Tactic.Delta//instructions: +20.1M (+1.60%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.MatchDiscrOnly//instructions: +21.2M (+1.30%)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Util//instructions: +36.2M (+0.88%)

@nomeata nomeata marked this pull request as ready for review April 6, 2026 13:45
@nomeata nomeata enabled auto-merge April 6, 2026 13:45
@nomeata nomeata added this pull request to the merge queue Apr 6, 2026
@nomeata nomeata added changelog-no Do not include this PR in the release changelog and removed changelog-compiler Compiler, runtime, and FFI labels Apr 6, 2026
Merged via the queue into master with commit d48863f Apr 6, 2026
34 checks passed
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 6, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c4a664eb5db2648780fa3c7a4be6d439e7233a72 --onto fc0cf68539ad3b481a1802414c22c44506519c9d. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-06 15:14:10)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c4a664eb5db2648780fa3c7a4be6d439e7233a72 --onto 861bc19e0c1c45b5766cc5c9ef0488568368b236. You can force reference manual CI using the force-manual-ci label. (2026-04-06 15:14:11)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-no Do not include this PR in the release changelog toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants