From d3b04871f54a85da29e880be6ba51c8d71b9dc4d Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 3 Apr 2026 08:03:55 +0200 Subject: [PATCH] perf: add checkInterrupted to inferType cache miss path (#13258) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds a `Core.checkInterrupted` call in `checkInferTypeCache` on cache miss, allowing cancellation to be detected during large type inference traversals. Previously, `inferTypeImp` could run for >100ms without any interruption check when processing large expressions (e.g. BVDecide proof terms), making IDE cancellation unresponsive. The check is only on cache miss (actual computation), so cache hits have zero overhead. `checkInterrupted` is used instead of the heavier `checkSystem` to minimize performance impact — local benchmarks show no measurable regression on `tests/elab/5664.lean`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.6 --- src/Lean/Meta/InferType.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean index eb82f2bca2..3f8c4a081c 100644 --- a/src/Lean/Meta/InferType.lean +++ b/src/Lean/Meta/InferType.lean @@ -180,12 +180,14 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do @[inline] private def checkInferTypeCache (e : Expr) (inferType : MetaM Expr) : MetaM Expr := do if !(← read).cacheInferType || e.hasMVar then + Core.checkInterrupted inferType else let key ← mkExprConfigCacheKey e match (← get).cache.inferType.find? key with | some type => return type | none => + Core.checkInterrupted let type ← inferType unless type.hasMVar do modifyInferTypeCache fun c => c.insert key type