chore: update to 2024-10-22 (#714)

opencompl · Oct 22, 2024 · 16b9c51 · 16b9c51
1 parent 806cae7
commit 16b9c51
Show file tree

Hide file tree

Showing 5 changed files with 9 additions and 61 deletions.
diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
@@ -510,10 +510,6 @@ theorem shiftLeft_and_distrib' {x y : BitVec w} {n m : Nat} :
     x <<< n &&& y <<< (m + n) = (x &&& y <<< m) <<< n := by
   simp [BitVec.shiftLeft_and_distrib, BitVec.shiftLeft_add]
 
-@[simp]
-theorem zero_sub {x : BitVec w} : 0#w - x = - x := by
-    simp [bv_toNat]
-
 theorem msb_neg {x : BitVec w} :
     (-x).msb = (~~~x + 1#w).msb := by
   rw [neg_eq_not_add]

diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean
@@ -137,10 +137,7 @@ macro "bv_auto": tactic =>
         -/
         try solve
           | ext; simp [BitVec.negOne_eq_allOnes, BitVec.allOnes_sub_eq_xor];
-            try cases BitVec.getLsbD _ _ <;> try simp
-            try cases BitVec.getLsbD _ _ <;> try simp
-            try cases BitVec.getLsbD _ _ <;> try simp
-            try cases BitVec.getLsbD _ _ <;> try simp
+            try bv_decide
           | simp [bv_ofBool]
           /-
           There are 2 main kinds of operations on BitVecs

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "46aeb3a35eea7490f9baf307f9c931c9b229310d",
+   "rev": "e770c1b554bcc2f96de51f2a95b5014b1f49df3e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "032cf93147e1fc5af7cbddc1075acea78c89a075",
+   "rev": "5632ca0c8675a572e875e501c19575d7785b9b38",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.44-pre",
+   "inputRev": "v0.0.44-pre3",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/mhuisi/lean4-cli.git",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6b657150b3c7294404ba85f0185391a898432a78",
+   "rev": "0b2215ab3149293ce640c44a02341e25881433ef",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -75,50 +75,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "407a4459e2005e212bb230d2746afe980eba7003",
+   "rev": "5d9876da9e139761f55a9d3bba56cbd11fe5ecf4",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing-2024-10-19",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/acmepjz/md4lean",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
-   "name": "MD4Lean",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "7afce91e4fcee25c1ed06dca8d71b82bed396776",
-   "name": "UnicodeBasic",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/dupuisf/BibtexQuery",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "0a294fe9bf23b396c5cc955054c50b9b652ec5ad",
-   "name": "BibtexQuery",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/doc-gen4",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "1b0072fea2aa6a0ef8ef8b506ec5223b184cb4d0",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing-2024-10-22",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/hargoniX/Leanwuzla.git",

diff --git a/lakefile.toml b/lakefile.toml
@@ -4,18 +4,13 @@ defaultTargets = ["SSA"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "nightly-testing-2024-10-19"
+rev = "nightly-testing-2024-10-22"
 
 [[require]]
 name = "Cli"
 git = "https://github.com/mhuisi/lean4-cli.git"
 rev = "nightly"
 
-[[require]]
-name = "doc-gen4"
-git = "https://github.com/leanprover/doc-gen4"
-rev = "main"
-
 [[require]]
 name = "leanwuzla"
 git = "https://github.com/hargoniX/Leanwuzla.git"

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-10-19
+leanprover/lean4:nightly-2024-10-22