From 34d00cb50d68771c91b8a00a1cac24cfe8fc7f66 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sun, 5 Apr 2026 15:11:39 +0200 Subject: [PATCH] feat: add checkSystem calls to bv_decide for cancellation responsiveness (#13284) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds `checkSystem` calls to the `bv_decide` tactic's main loops to improve IDE cancellation responsiveness. Previously, `bv_decide` had zero `checkSystem` calls in its entire codebase, meaning long-running invocations could not be cancelled promptly. Insertion points: - `fixpointPipeline` (normalization fixpoint loop) - `ReifiedBVExpr.of.go` (recursive BitVec expression reification) - `ReifiedBVLogical.of.go` (recursive boolean expression reification) - `reflectBV` (hypothesis loop) These cover the MetaM-based phases of `bv_decide`. The pure computation phases (bitblasting via `IO.lazyPure`, AIG→CNF conversion) remain without checks and would require restructuring to address. Gap measurements (at 6.0 Ginstr/s, using `LEAN_CHECK_SYSTEM_INTERVAL_INSN` from #13212): - `bv_decide_large_aig.lean`: before ~3.3s max gap (19,899M insn), after: pure bitblast/AIG gaps remain but reification and normalization phases are now interruptible - Other bv_decide bench files: normalization and reification loops are now responsive to cancellation Note: the largest remaining gaps in bv_decide benchmarks are in the kernel type checker (proof term checking, up to 10.5s on `bv_decide_mod.lean`) and in pure bitblasting — both out of scope for this PR. Co-authored-by: Claude Opus 4.6 --- src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean | 1 + src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean | 2 ++ src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean | 1 + 3 files changed, 4 insertions(+) diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean index dc25332165..d2e29adf82 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean @@ -357,6 +357,7 @@ def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do let mut sats := #[] let mut unusedHypotheses := {} for hyp in hyps do + checkSystem "bv_decide" if let (some reflected, lemmas) ← (SatAtBVLogical.of (mkFVar hyp)).run then sats := (sats ++ lemmas).push reflected else diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean index 07ce17a40e..c53119d9f3 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean @@ -33,6 +33,7 @@ where Reify `x`, returns `none` if the reification procedure failed. -/ go (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do + checkSystem "bv_decide" match_expr origExpr with | BitVec.ofNat _ _ => goBvLit origExpr | HAnd.hAnd _ _ _ _ lhsExpr rhsExpr => @@ -340,6 +341,7 @@ where Reify `t`, returns `none` if the reification procedure failed. -/ go (origExpr : Expr) : LemmaM (Option ReifiedBVLogical) := do + checkSystem "bv_decide" match_expr origExpr with | Bool.true => ReifiedBVLogical.mkBoolConst true | Bool.false => ReifiedBVLogical.mkBoolConst false diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean index 229a1e6212..9ec9621bd8 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean @@ -159,6 +159,7 @@ Repeatedly run a list of `Pass` until they either close the goal or an iteration the goal anymore. -/ partial def fixpointPipeline (passes : List Pass) (goal : MVarId) : PreProcessM (Option MVarId) := do + checkSystem "bv_decide" let mut newGoal := goal for pass in passes do if let some nextGoal ← pass.run newGoal then