also disable async TC in bv_decide et al

leanprover · Dec 12, 2024 · 282c65c · 282c65c
1 parent 9df65ba
commit 282c65c
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 4 deletions.
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
@@ -308,7 +308,7 @@ def bvDecide (g : MVarId) (ctx : TacticContext) : MetaM Result := do
       throwError (← addMessageContextFull errorMessage)
 
 @[builtin_tactic Lean.Parser.Tactic.bvDecide]
-def evalBvTrace : Tactic := fun
+def evalBvDecide : Tactic := fun
   | `(tactic| bv_decide $cfg:optConfig) => do
     let cfg ← elabBVDecideConfig cfg
     IO.FS.withTempFile fun _ lratFile => do
@@ -319,4 +319,3 @@ def evalBvTrace : Tactic := fun
 
 end Frontend
 end Lean.Elab.Tactic.BVDecide
-
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean
@@ -197,8 +197,10 @@ def LratCert.toReflectionProof [ToExpr α] (cert : LratCert) (cfg : TacticContex
       (← mkEqRefl (toExpr true))
   try
     let auxLemma ←
-      withTraceNode `sat (fun _ => return "Verifying LRAT certificate") do
-        mkAuxLemma [] auxType auxProof
+      -- disable async TC so we can catch its exceptions
+      withOptions (Elab.async.set · false) do
+        withTraceNode `sat (fun _ => return "Verifying LRAT certificate") do
+          mkAuxLemma [] auxType auxProof
     return mkApp3 (mkConst unsat_of_verifier_eq_true) reflectedExpr certExpr (mkConst auxLemma)
   catch e =>
     throwError m!"Failed to check the LRAT certificate in the kernel:\n{e.toMessageData}"