From 402a6096b909eae534a96c82e43b8ee45de52ef1 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 1 Apr 2026 14:54:57 +0200 Subject: [PATCH] fix: add checkSystem calls to long-running elaboration paths (#13220) This PR adds `checkSystem` calls to several code paths that can run for extended periods without checking for cancellation, heartbeat limits, or stack overflow. This improves responsiveness of the cancellation mechanism in the language server. Affected paths: - `simpLoop` step loop (`Simp/Main.lean`) - `simp` rewrite candidate loops (`Rewrite.lean`) - `simpAppUsingCongr` argument traversal (`Types.lean`) - `synthesizeSyntheticMVarsStep` mvar loop (`SyntheticMVars.lean`) - `abstractNestedProofs` visitor (`AbstractNestedProofs.lean`) - `transform`/`transformWithCache` visitors (`Transform.lean`) - LCNF compiler pass runner loop (`LCNF/Main.lean`) - LCNF checker recursive traversal (`LCNF/Check.lean`) - `whnfImp` top-level reduction (`WHNF.lean`) Intentionally *not* instrumented (too hot, measurable regression): - `whnfCore.go` inner recursion - `simpImpl` entry point (redundant with `simpLoop`) - LCNF `simp` inner recursion (0.4% regression on `big_do`) Also adds a docstring to `checkInterrupted` clarifying its relationship to `checkSystem`. Found using `LEAN_CHECK_SYSTEM_INTERVAL_MS` monitoring from #13218. Co-authored-by: Claude Opus 4.6 --- src/Lean/Compiler/LCNF/Check.lean | 1 + src/Lean/Compiler/LCNF/Main.lean | 1 + src/Lean/CoreM.lean | 3 +++ src/Lean/Elab/SyntheticMVars.lean | 1 + src/Lean/Meta/AbstractNestedProofs.lean | 1 + src/Lean/Meta/Tactic/Simp/Main.lean | 1 - src/Lean/Meta/Tactic/Simp/Rewrite.lean | 2 ++ src/Lean/Meta/Tactic/Simp/Types.lean | 1 + src/Lean/Meta/Transform.lean | 2 ++ src/Lean/Meta/WHNF.lean | 2 +- 10 files changed, 13 insertions(+), 2 deletions(-) diff --git a/src/Lean/Compiler/LCNF/Check.lean b/src/Lean/Compiler/LCNF/Check.lean index 98a391466c..594588f2c3 100644 --- a/src/Lean/Compiler/LCNF/Check.lean +++ b/src/Lean/Compiler/LCNF/Check.lean @@ -232,6 +232,7 @@ partial def checkCases (c : Cases .pure) : CheckM Unit := do withParams params do check k partial def check (code : Code .pure) : CheckM Unit := do + checkSystem "LCNF check" match code with | .let decl k => checkLetDecl decl; withFVarId decl.fvarId do check k | .fun decl k => diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean index 2f6189f17a..11023abb4d 100644 --- a/src/Lean/Compiler/LCNF/Main.lean +++ b/src/Lean/Compiler/LCNF/Main.lean @@ -188,6 +188,7 @@ where profileitM Exception profilerName (← getOptions) do let mut state : (pu : Purity) × Array (Decl pu) := ⟨inPhase, decls⟩ for pass in passes do + checkSystem "LCNF compiler" state ← withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do let decls ← withPhase pass.phase do state.fst.withAssertPurity pass.phase.toPurity fun h => do diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 3403cbfde6..ead24ad2a0 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -453,6 +453,9 @@ Throws an internal interrupt exception if cancellation has been requested. The e caught by `try catch` but is intended to be caught by `Command.withLoggingExceptions` at the top level of elaboration. In particular, we want to skip producing further incremental snapshots after the exception has been thrown. + +Like `checkSystem` but without the global heartbeat check, for callers that have their own +heartbeat tracking (e.g. `SynthInstance`). -/ @[inline] def checkInterrupted : CoreM Unit := do if let some tk := (← read).cancelTk? then diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index 310e9927b3..7b7f039bfa 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -582,6 +582,7 @@ mutual -- We use `filterRevM` instead of `filterM` to make sure we process the synthetic metavariables using the order they were created. -- It would not be incorrect to use `filterM`. let remainingPendingMVars ← pendingMVars.filterRevM fun mvarId => do + checkSystem "synthesize pending MVars" -- We use `traceM` because we want to make sure the metavar local context is used to trace the message traceM `Elab.postpone (mvarId.withContext do addMessageContext m!"resuming {mkMVar mvarId}") let succeeded ← synthesizeSyntheticMVar mvarId postponeOnError runTactics diff --git a/src/Lean/Meta/AbstractNestedProofs.lean b/src/Lean/Meta/AbstractNestedProofs.lean index 3b27b6f36b..b931c2cf05 100644 --- a/src/Lean/Meta/AbstractNestedProofs.lean +++ b/src/Lean/Meta/AbstractNestedProofs.lean @@ -70,6 +70,7 @@ structure Context where abbrev M := ReaderT Context $ MonadCacheT ExprStructEq Expr MetaM partial def visit (e : Expr) : M Expr := do + checkSystem "abstract nested proofs" if e.isAtomic then pure e else diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index f8c2607a24..b648566cb9 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -714,7 +714,6 @@ where set_option compiler.ignoreBorrowAnnotation true in @[export lean_simp] def simpImpl (e : Expr) : SimpM Result := withIncRecDepth do - checkSystem "simp" if (← isProof e) then return { expr := e } trace[Meta.Tactic.simp.heads] "{repr e.toHeadIndex}" diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index 49d1c5d503..1ef7505199 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -219,6 +219,7 @@ where else let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority for (thm, numExtraArgs) in candidates do + checkSystem "simp" if inErasedSet thm then continue if rflOnly then unless thm.rfl do @@ -246,6 +247,7 @@ where else let candidates := candidates.insertionSort fun e₁ e₂ => e₁.priority > e₂.priority for thm in candidates do + checkSystem "simp" unless inErasedSet thm || (rflOnly && !thm.rfl) do let result? ← withNewMCtxDepth do let val ← thm.getValue diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 6583ec6ae6..c2d1d673f0 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -722,6 +722,7 @@ def simpAppUsingCongr (e : Expr) : SimpM Result := do if i == 0 then simp f else + checkSystem "simp" let i := i - 1 let .app f a := e | unreachable! let fr ← visit f i diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean index f75d4da31c..e526c71d75 100644 --- a/src/Lean/Meta/Transform.lean +++ b/src/Lean/Meta/Transform.lean @@ -50,6 +50,7 @@ partial def transform {m} [Monad m] [MonadLiftT CoreM m] [MonadControlT CoreM m] let _ : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := CoreM) (liftM (m := ST IO.RealWorld) x) } let rec visit (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := checkCache { val := e : ExprStructEq } fun _ => Core.withIncRecDepth do + Core.checkSystem "transform" let rec visitPost (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do match (← post e) with | .done e => pure e @@ -107,6 +108,7 @@ partial def transformWithCache {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT let _ : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := MetaM) (liftM (m := ST IO.RealWorld) x) } let rec visit (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := checkCache { val := e : ExprStructEq } fun _ => Meta.withIncRecDepth do + (Core.checkSystem "transform" : MetaM Unit) let rec visitPost (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do match (← post e) with | .done e => pure e diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 74fcfef37f..0ce0dcac22 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -650,7 +650,7 @@ expand let-expressions, expand assigned meta-variables, unfold aux declarations. partial def whnfCore (e : Expr) : MetaM Expr := go e where - go (e : Expr) : MetaM Expr := + go (e : Expr) : MetaM Expr := do whnfEasyCases e fun e => do trace[Meta.whnf] e match e with