Bump Lean version (#137)

Co-authored-by: Paul Lezeau <[email protected]>
ufmg-smite · Oct 26, 2024 · 8bc677e · 8bc677e
1 parent f0e6b56
commit 8bc677e
Show file tree

Hide file tree

Showing 5 changed files with 25 additions and 14 deletions.
diff --git a/Smt/Data/Graph.lean b/Smt/Data/Graph.lean
@@ -11,7 +11,7 @@ import Lean.Message
 
 open Lean Std
 
-def Graph (α) (β) [BEq α] [Hashable α] := HashMap α (HashMap α β)
+def Graph (α) (β) [BEq α] [Hashable α] := Lean.HashMap α (Lean.HashMap α β)
 
 namespace Graph
 
@@ -39,7 +39,7 @@ partial def dfs [Monad m] (f : α → m Unit) : m Unit :=
     for v in g.vertices do
       visitVertex v
 where
-  visitVertex (v : α) : StateT (HashSet α) m Unit := do
+  visitVertex (v : α) : StateT (Lean.HashSet α) m Unit := do
     let vs ← get
     if vs.contains v then
       return
@@ -53,7 +53,7 @@ partial def orderedDfs [Monad m] (vs : List α) (f : α → m Unit) : m Unit :=
     for v in vs do
       visitVertex v
 where
-  visitVertex (v : α) : StateT (HashSet α) m Unit := do
+  visitVertex (v : α) : StateT (Lean.HashSet α) m Unit := do
     let vs ← get
     if vs.contains v then
       return

diff --git a/Smt/Reconstruct/BitVec/Bitblast.lean b/Smt/Reconstruct/BitVec/Bitblast.lean
@@ -48,7 +48,8 @@ def adc' (x y : BitVec w) : Bool → Bool × BitVec w :=
 
 theorem adc_eq_adc' : @adc = @adc' := by
   funext x y c
-  simp only [adc, adc', adcb_eq_adcb']
+  rw [adc, adc', adcb_eq_adcb']
+  rfl
 
 theorem add_eq_adc' (x y : BitVec w) : x + y = (adc' x y false).snd := by
   rw [add_eq_adc, adc_eq_adc']

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
+   "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9d0bdd07bdfe53383567509348b1fe917fc08de4",
+   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "deb279eb7be16848d0bc8387f80d6e41bcdbe738",
+   "rev": "28fa80508edc97d96ed6342c9a771a67189e0baa",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -45,10 +45,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
+   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.41",
+   "inputRev": "v0.0.42",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -65,20 +65,30 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1ef0b288623337cb37edd1222b9c26b4b77c6620",
+   "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "20c73142afa995ac9c8fb80a9bb585a55ca38308",
+   "rev": "809c3fb3b5c8f5d7dace56e200b426187516535a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.11.0",
+   "inputRev": "v4.12.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "smt",

diff --git a/lakefile.lean b/lakefile.lean
@@ -6,7 +6,7 @@ require cvc5 from
   git "https://github.com/abdoo8080/lean-cvc5.git" @ "c97ff4cfc218c11af8c1598b8225a6fcc094f5cd"
 
 require mathlib from
-  git "https://github.com/leanprover-community/mathlib4.git" @ "v4.11.0"
+  git "https://github.com/leanprover-community/mathlib4.git" @ "v4.12.0"
 
 def libcpp : String :=
   if System.Platform.isWindows then "libstdc++-6.dll"

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.11.0
+leanprover/lean4:v4.12.0