Update to v4.14.0

Duper/ClauseStreamHeap.lean

@@ -138,9 +138,9 @@ def ProverM.postProcessInferenceResult (cp : ClauseProof) : ProverM Unit := do
   let allClauses ← getAllClauses
   let parentClauseInfoOpts ← proof.parents.mapM
     (fun p =>
-      match allClauses.find? p.clause with
+      match allClauses.get? p.clause with
       | some pi => pure pi
-      | none => throwError "ProverM.postProcessInferenceResult: Unable to find parent clause {p.clause}")
+      | none => throwError "ProverM.postProcessInferenceResult: Unable to find parent clause {p.clause.toForallExpr}")
   -- c's generation number is one greater than the sum of its parents generation numbers
   let generationNumber := parentClauseInfoOpts.foldl (fun acc parentInfo => acc + parentInfo.generationNumber) 1
   -- c's goalDistance is at most maxGoalDistance and is otherwise one greater than the distance of the parent closest to the goal

Duper/ProverM.lean

@@ -98,9 +98,6 @@ instance : AddMessageContext ProverM where
 @[inline] def ProverM.run' (x : ProverM α) (ctx : Context := {}) (s : State := {}) : MetaM α :=
   Prod.fst <$> x.run ctx s
 
-instance [MetaEval α] : MetaEval (ProverM α) :=
-  ⟨fun env opts x _ => MetaEval.eval env opts x.run' true⟩
-
 initialize
   registerTraceClass `duper.prover.saturate
   registerTraceClass `duper.createdClauses

Duper/Selection.lean

@@ -131,7 +131,7 @@ def selectMaxLitComplex (c : MClause) (alreadyReduced : Bool) : RuleM (List Nat)
     selectMaxLitComplex but uses the number of positive literals with a shared predicate symbol as a tiebreaker (preferring
     to select literals that share a predicate symbol with as few positive literals as possible). For this, specification, I
     am defining a predicate symbol as the top symbol for the lhs of a literal of the form `e = True` or `e = False`.
-    
+
     Note: According to "Extending a Brainiac Prover to Lambda-Free Higher-Order Logic", SelectMaxLComplexAvoidPosPred
     (aka SelectMLCAPP) should be have very similarly to E's SelectMLCAPPPreferAppVar and SelectMLCAPPAvoidAppVar. So
     it should be unnecessary to separately implement those two selection functions. -/
@@ -204,7 +204,7 @@ def selectMaxLitComplexAvoidPosPred (c : MClause) (alreadyReduced : Bool) : Rule
     literal of the form `e = True` or `e = False`). If there are multiple negative literals with the same largest predicate, then
     the size difference between the lit's lhs and rhs will be the tiebreaker (with larger size differences being preferred). -/
 def selectCQIPrecWNTNp (c : MClause) (alreadyReduced : Bool) : RuleM (List Nat) := do
-  let idxLitPairs := c.lits.mapIdx (fun idx l => (idx.1, l))
+  let idxLitPairs := c.lits.mapIdx (fun idx l => (idx, l))
   let idxPredPairs := idxLitPairs.filterMap
     (fun (idx, l) =>
       -- Since we only select negative literals, and since we need a predicate, the only form we allow `l` to have is `e = False`
@@ -217,10 +217,10 @@ def selectCQIPrecWNTNp (c : MClause) (alreadyReduced : Bool) : RuleM (List Nat)
     )
   let symbolPrecMap ← getSymbolPrecMap -- Recall that low values in symbolPrecMap correspond to high precedence
   let idxPredPairsSorted := idxPredPairs.qsort -- Sorting so that highest precedence symbols will be first in idxPredPairsSorted
-    (fun (idx1, pred1Opt) (idx2, pred2Opt) =>
+    (fun (_idx1, pred1Opt) (_idx2, pred2Opt) =>
       match pred1Opt, pred2Opt with
       | some pred1, some pred2 =>
-        match symbolPrecMap.find? pred1, symbolPrecMap.find? pred2 with
+        match symbolPrecMap.get? pred1, symbolPrecMap.get? pred2 with
         | none, _ => false -- Never sort symbol not found in symbolPrecMap before anything else
         | some _, none => true -- Symbols found in symbolPrecMap are sorted before symbols found in symbolPrecMap
         | some prec1, some prec2 => prec1 < prec2 -- Low values in symbolPrecMap correspond to higher precedence
@@ -287,12 +287,12 @@ def litSelected (c : MClause) (i : Nat) (alreadyReduced : Bool) : RuleM Bool :=
   return sel.contains i
 
 /-- Data type to capture whether a literal in a clause is eligible.
-If it is not eligible, we distinguish the cases where there might 
+If it is not eligible, we distinguish the cases where there might
 be substitutions that make the literal eligble (`potentiallyEligible`)
 or not (`notEligible`).-/
-inductive Eligibility 
-  | eligible 
-  | potentiallyEligible 
+inductive Eligibility
+  | eligible
+  | potentiallyEligible
   | notEligible
 deriving Inhabited, BEq, Repr, Hashable
 
@@ -343,4 +343,4 @@ def eligibilityPostUnificationCheck (c : MClause) (alreadyReduced := false) (i :
   else if preUnificationResult == Eligibility.notEligible then return false
   else c.isMaximalLit (← getOrder) alreadyReduced i (strict := strict)
 
-end Duper
+end Duper

Duper/Tactic.lean

@@ -39,8 +39,8 @@ def getIgnoreUnusableFactsM : CoreM Bool := do
   for each constructor, a proof of the equation, and the contained level
   parameters. -/
 def addRecAsFact (recVal : RecursorVal): TacticM (List (Expr × Expr × Array Name)) := do
-  let some (.inductInfo indVal) := (← getEnv).find? recVal.getInduct
-    | throwError "Expected inductive datatype: {recVal.getInduct}"
+  let some (.inductInfo indVal) := (← getEnv).find? recVal.getMajorInduct
+    | throwError "Expected inductive datatype: {recVal.getMajorInduct}"
   let expr := mkConst recVal.name (recVal.levelParams.map Level.param)
   let res ← forallBoundedTelescope (← inferType expr) recVal.getMajorIdx fun xs _ => do
     let expr := mkAppN expr xs

lake-manifest.json

@@ -1,25 +1,25 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/lean-auto.git",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "915802517242f70b284fbcd5eac55bdaae29535e",
-   "name": "auto",
+   "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "915802517242f70b284fbcd5eac55bdaae29535e",
+   "inputRev": "v4.14.0",
    "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/batteries",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18",
-   "name": "batteries",
+   "rev": "4d73b99262f1ce80a33ac832bef26549cf3c2034",
+   "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.13.0",
+   "inputRev": "4d73b99262f1ce80a33ac832bef26549cf3c2034",
    "inherited": false,
-   "configFile": "lakefile.toml"}],
+   "configFile": "lakefile.lean"}],
  "name": "Duper",
  "lakeDir": ".lake"}

lakefile.lean

@@ -2,8 +2,8 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"915802517242f70b284fbcd5eac55bdaae29535e"
-require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.13.0"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"4d73b99262f1ce80a33ac832bef26549cf3c2034"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.14.0"
 
 package Duper {
   precompileModules := true

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.13.0
+leanprover/lean4:v4.14.0