Update to lean v4.12.0

Duper/Fingerprint.lean

@@ -113,7 +113,7 @@ def emptyCFP : ClauseFingerprintTrie := mkEmptyWithDepth numFingerprintFeatures
    I could be quite off-base on that. -/
 structure RootCFPTrie where
   root : ClauseFingerprintTrie := emptyCFP
-  filterSet : HashSet Clause := {} -- Keeps track of the set of clauses that should be filtered out (i.e. "removed" clauses)
+  filterSet : Std.HashSet Clause := {} -- Keeps track of the set of clauses that should be filtered out (i.e. "removed" clauses)
 deriving Inhabited
 
 namespace RootCFPTrie

Duper/Rules/SyntacticTautologyDeletion3.lean

@@ -10,8 +10,8 @@ open SimpResult
     duper often gets cluttered with clauses of the form "x = True ∨ x = False". Neither syntacticTautologyDeletion1 nor
     syntacticTautologyDeletion2 remove clauses of this form, so that is what syntacticTautologyDeletion3 targets. -/
 def syntacticTautologyDeletion3 : MSimpRule := fun c => do
-  let mut eqTrueSet : HashSet Lean.Expr := mkHashSet -- Stores Lean expressions equated to True in c
-  let mut eqFalseSet : HashSet Lean.Expr := mkHashSet -- Stores Lean expressions equated to False in c
+  let mut eqTrueSet : Std.HashSet Lean.Expr := Std.HashSet.empty -- Stores Lean expressions equated to True in c
+  let mut eqFalseSet : Std.HashSet Lean.Expr := Std.HashSet.empty -- Stores Lean expressions equated to False in c
   for lit in c.lits do
     if lit.sign then
       if lit.rhs == mkConst ``True then
@@ -41,4 +41,4 @@ def syntacticTautologyDeletion3 : MSimpRule := fun c => do
         else eqTrueSet := eqTrueSet.insert lit.rhs
   return none
 
-end Duper
+end Duper

Duper/Tactic.lean

@@ -87,7 +87,7 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do
         if sort.isProp then
           ret := ret.push (← elabFactAux stx)
         -- Generate definitional equation for the fact
-        if let some eqns ← getEqnsFor? exprConstName (nonRec := true) then
+        if let some eqns ← getEqnsFor? exprConstName then
           ret := ret.append (← eqns.mapM fun eq => do elabFactAux (← `($(mkIdent eq))))
         trace[duper.elabFact.debug] "Adding definition {expr} as the following facts: {ret.map (fun x => x.1)}"
         return ret

lake-manifest.json

@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5149acf1aaa07a62a53a7e0979ff79d85812287d",
+   "rev": "680d6d58ce2bb65d15e5711d93111b2e5b22cb1a",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "5149acf1aaa07a62a53a7e0979ff79d85812287d",
+   "inputRev": "680d6d58ce2bb65d15e5711d93111b2e5b22cb1a",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
+   "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.11.0",
+   "inputRev": "v4.12.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Duper",

lakefile.lean

@@ -2,8 +2,8 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"5149acf1aaa07a62a53a7e0979ff79d85812287d"
-require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.11.0"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"680d6d58ce2bb65d15e5711d93111b2e5b22cb1a"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.12.0"
 
 package Duper {
   precompileModules := true

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.11.0
+leanprover/lean4:v4.12.0