From d48863fc2bb15ffbb9b393fba4b5b0bd767fe391 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 6 Apr 2026 15:45:30 +0200 Subject: [PATCH] fix: add checkInterrupted to Core.withIncRecDepth (#13290) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Co-authored-by: Claude Opus 4.6 --- src/Lean/CoreM.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index b2dee8594f..53b4d06a3c 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -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"