max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: add checkInterrupted to Core.withIncRecDepth (#13290)

Browse source 
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>

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
Joachim Breitner 2026-04-06 15:45:30 +02:00 • committed by GitHub
parent c4a664eb5d
commit d48863fc2b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/CoreM.lean
View file

@ -446,10 +446,6 @@ Note that the value of `ctx.initHeartbeats` is ignored and replaced with `IO.get
@[inline] def CoreM.toIO' (x : CoreM α) (ctx : Context) (s : State) : IO α :=
(·.1) <$> x.toIO ctx s
/-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`. -/
protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)
/--
Throws an internal interrupt exception if cancellation has been requested. The exception is not
caught by `try catch` but is intended to be caught by `Command.withLoggingExceptions` at the top
@ -464,6 +460,12 @@ heartbeat tracking (e.g. `SynthInstance`).
if (← tk.isSet) then
throwInterruptException
/-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`.
Also checks for cancellation, so that recursive elaboration functions
(inferType, whnf, isDefEq, …) respond promptly to interrupt requests. -/
protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
controlAt CoreM fun runInBase => do checkInterrupted; withIncRecDepth (runInBase x)
register_builtin_option debug.moduleNameAtTimeout : Bool := {
defValue := true
descr := "include module name in deterministic timeout error messages.\nRemark: we set this option to false to increase the stability of our test suite"