chore: update toolchain

Author: hargoniX

Leanwuzla.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide
+import Lean.Meta.Tactic.BVDecide
 
 open Lean.Parser.Tactic
 
@@ -25,6 +25,7 @@ open Std.Sat
 open Std.Tactic.BVDecide
 open Std.Tactic.BVDecide.Reflect
 open Lean.Meta
+open Lean.Meta.Tactic.BVDecide
 
 
 partial def toSMT (expr : BVLogicalExpr) (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) : String :=
@@ -116,7 +117,7 @@ where
       let binStr := t ++ s
       push "#b"
       push binStr
-    | .extract start len expr => pushUnaryOp s!"(_ extract {len - 1 + start} {start})" (goBVExpr expr)
+    | .extract start _ expr => pushUnaryOp s!"(_ extract {w - 1 + start} {start})" (goBVExpr expr)
     | .bin lhs op rhs =>
       let lhs := goBVExpr lhs
       let rhs := goBVExpr rhs
@@ -206,7 +207,7 @@ def bitwuzlaSuccess : String := "Bitwuzla thinks it's right but can't trust the
 
 def bitwuzla (g : MVarId) (reflectionResult : ReflectionResult) (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool))
     (solverPath : System.FilePath) (cfg : BVDecideConfig) :
-    MetaM (Except CounterExample UnsatProver.Result) := do
+    MetaM (Except CounterExample (UnsatProver.Result Unit)) := do
   let smt := toSMT reflectionResult.bvExpr atomsAssignment
   trace[Meta.Tactic.bv] s!"Encoded as SMT: {smt}"
   let res ←
@@ -217,12 +218,12 @@ def bitwuzla (g : MVarId) (reflectionResult : ReflectionResult) (atomsAssignment
         smtQuery solverPath path cfg.timeout
   match res with
   | .sat .. => return .error ⟨g, {}, #[]⟩
-  | .unsat => return .ok ⟨mkApp (mkConst ``bitwuzlaCorrect) (toExpr reflectionResult.bvExpr), ""⟩
+  | .unsat => return .ok ⟨mkApp (mkConst ``bitwuzlaCorrect) (toExpr reflectionResult.bvExpr), ()⟩
 
 def bvBitwuzla (g : MVarId) (solverPath : System.FilePath) (cfg : BVDecideConfig) :
     MetaM (Except CounterExample Unit) := do
   let some g ← Normalize.bvNormalize g cfg | return .ok ()
-  let unsatProver : UnsatProver := fun g reflectionResult atomsAssignment => do
+  let unsatProver : UnsatProver Unit := fun g reflectionResult atomsAssignment => do
     withTraceNode `bv (fun _ => return "Preparing LRAT reflection term") do
       bitwuzla g reflectionResult atomsAssignment solverPath cfg
   match ← closeWithBVReflection g unsatProver with

Leanwuzla/Aux.lean Leanwuzla/Auxiliary.leanLeanwuzla/Aux.lean renamed to Leanwuzla/Auxiliary.lean

@@ -1,4 +1,4 @@
-import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide
+import Lean.Meta.Tactic.BVDecide
 
 open Lean
 
@@ -22,7 +22,7 @@ def _root_.Lean.MVarId.introsP (mvarId : MVarId) : MetaM (Array FVarId × MVarId
   else
     mvarId.introNP n
 
-open Elab.Tactic.BVDecide.Frontend in
+open Meta.Tactic.BVDecide in
 structure Context where
   acNf : Bool
   parseOnly : Bool
@@ -32,7 +32,7 @@ structure Context where
   disableAndFlatten : Bool
   disableEmbeddedConstraintSubst : Bool
   disableKernel : Bool
-  solverMode : SolverMode
+  solverMode : Elab.Tactic.BVDecide.SolverMode
 
 abbrev SolverM := ReaderT Context MetaM
 
@@ -42,7 +42,7 @@ def getParseOnly : SolverM Bool := return (← read).parseOnly
 def getInput : SolverM String := return (← read).input
 def getKernelDisabled : SolverM Bool := return (← read).disableKernel
 
-def getBVDecideConfig : SolverM Elab.Tactic.BVDecide.Frontend.BVDecideConfig := do
+def getBVDecideConfig : SolverM Elab.Tactic.BVDecide.BVDecideConfig := do
   let ctx ← read
   return {
     timeout := ctx.timeout

Leanwuzla/Basic.lean

@@ -1,11 +1,10 @@
 import Leanwuzla.Basic
 
 open Lean Std.Sat Std.Tactic.BVDecide
-open Elab.Tactic.BVDecide
-open Elab.Tactic.BVDecide.Frontend
+open Meta.Tactic.BVDecide
 
 def runSolver (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.FilePath)
-    (trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool) (solverMode : SolverMode) :
+    (trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool) (solverMode : Elab.Tactic.BVDecide.SolverMode) :
     CoreM (Except (Array (Bool × Nat)) (Array LRAT.IntAction)) := do
   IO.FS.withTempFile fun cnfHandle cnfPath => do
     withTraceNode `sat (fun _ => return "Serializing SAT problem to DIMACS file") do

Leanwuzla/NoKernel.lean

@@ -1,4 +1,4 @@
-import Leanwuzla.Aux
+import Leanwuzla.Auxiliary
 import Leanwuzla.Sexp
 
 open Lean

Leanwuzla/Parser.lean

@@ -11,6 +11,7 @@ def parseSmt2File (path : System.FilePath) : MetaM Expr := do
   ofExcept (Parser.parseSmt2Query query)
 
 
+open Meta in
 open Elab in
 def decideSmt (type : Expr) : SolverM UInt8 := do
   let mv ← Meta.mkFreshExprMVar type
@@ -19,8 +20,8 @@ def decideSmt (type : Expr) : SolverM UInt8 := do
   try
     mv'.withContext $ IO.FS.withTempFile fun _ lratFile => do
       let cfg ← SolverM.getBVDecideConfig
-      let ctx ← (Tactic.BVDecide.Frontend.TacticContext.new lratFile cfg).run' { declName? := `lrat }
-      discard <| Tactic.BVDecide.Frontend.bvDecide mv' ctx
+      let ctx ← (Tactic.BVDecide.TacticContext.new lratFile cfg).run' { declName? := `lrat }
+      discard <| Tactic.BVDecide.bvDecide mv' ctx
   catch e =>
     -- TODO: improve handling of sat cases. This is a temporary workaround.
     let message ← e.toMessageData.toString
@@ -110,15 +111,15 @@ open Cli
 
 open Elab.Tactic.BVDecide.Frontend
 
-deriving instance Inhabited for SolverMode
+deriving instance Inhabited for Elab.Tactic.BVDecide.SolverMode
 
-instance : ToString SolverMode where
+instance : ToString Elab.Tactic.BVDecide.SolverMode where
   toString
   | .proof          => "proof"
   | .counterexample => "counterexample"
   | .default        => "default"
 
-instance : ParseableType SolverMode where
+instance : ParseableType Elab.Tactic.BVDecide.SolverMode where
   name := "SolverMode"
   parse?
   | "proof"           => some .proof
@@ -131,7 +132,7 @@ unsafe def runLeanwuzlaCmd (p : Parsed) : IO UInt32 := do
   let context := argsToContext p
   Lean.initSearchPath (← Lean.findSysroot)
   enableInitializersExecution
-  let env ← importModules #[`Std.Tactic.BVDecide, `Leanwuzla.Aux] {} 0 (loadExts := true)
+  let env ← importModules #[`Std.Tactic.BVDecide, `Leanwuzla.Auxiliary] {} 0 (loadExts := true)
   let coreContext := { fileName := "leanwuzla", fileMap := default, options }
   let coreState := { env }
   let code ← SolverM.run parseAndDecideSmt2File context coreContext coreState
@@ -180,7 +181,7 @@ where
       disableAndFlatten := p.hasFlag "disableAndFlatten"
       disableEmbeddedConstraintSubst := p.hasFlag "disableEmbeddedConstraintSubst"
       disableKernel := p.hasFlag "disableKernel"
-      solverMode := p.flag! "solverMode" |>.as! SolverMode
+      solverMode := p.flag! "solverMode" |>.as! Elab.Tactic.BVDecide.SolverMode
     }
 
 unsafe def leanwuzlaCmd : Cmd := `[Cli|
@@ -202,7 +203,7 @@ unsafe def leanwuzlaCmd : Cmd := `[Cli|
     disableAndFlatten; "Disable the and flattening pass."
     disableEmbeddedConstraintSubst; "Disable the embedded constraints substitution pass."
     disableKernel; "Disable the Lean kernel, that is only verify the LRAT cert, no reflection proof"
-    solverMode : SolverMode; "Select the SAT solver configuration to use (`proof`, `counterexample`, `default`)."
+    solverMode : Elab.Tactic.BVDecide.SolverMode; "Select the SAT solver configuration to use (`proof`, `counterexample`, `default`)."
 
   ARGS:
     input : String; "Path to the smt2 file to work on"
@@ -215,7 +216,7 @@ unsafe def leanwuzlaCmd : Cmd := `[Cli|
       ("pthreshold", toString trace.profiler.threshold.defValue),
       ("maxSteps", toString Lean.Meta.Simp.defaultMaxSteps),
       ("expthreshold", toString exponentiation.threshold.defValue),
-      ("solverMode", toString SolverMode.proof)
+      ("solverMode", toString Lean.Elab.Tactic.BVDecide.SolverMode.proof)
     ]
 ]
 

Main.lean

@@ -5,6 +5,8 @@ Authors: Henrik Böving
 -/
 import Leanwuzla
 
+#exit
+
 variable (a b c : Bool)
 variable (x y z : BitVec 32)
 

Test/Bitwuzla.lean

@@ -1 +1 @@
-leanprover/lean4:v4.30.0-rc2
+nightly-2026-06-08