chore: update to nightly-2024-08-08 (#522)

SSA/Projects/InstCombine/AliveHandwrittenExamples.lean

@@ -10,7 +10,6 @@ import SSA.Projects.InstCombine.ForStd
 import SSA.Core.ErasedContext
 
 open MLIR AST
-open Std (BitVec)
 open Ctxt (Var DerivedCtxt)
 open InstCombine (MOp)
 

SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean

@@ -114,7 +114,6 @@ def MulDivRem805_rhs (w : ℕ) : Com InstCombine.LLVM
   /- r = -/ Com.var (select w /-%c-/ 1 /-X-/ 5 /-c0-/ 0) <|
   Com.ret ⟨/-r-/0, by simp [Ctxt.snoc]⟩
 
-open Std (BitVec) in
 def alive_simplifyMulDivRem805 (w : Nat) :
   MulDivRem805_lhs w ⊑ MulDivRem805_rhs w := by
   unfold MulDivRem805_lhs MulDivRem805_rhs
@@ -223,7 +222,6 @@ info: 'AliveHandwritten.MulDivRem.alive_simplifyMulDivRem805' depends on axioms:
 -/
 #guard_msgs in #print axioms alive_simplifyMulDivRem805
 
-open Std (BitVec) in
 def alive_simplifyMulDivRem805' (w : Nat) :
   MulDivRem805_lhs w ⊑ MulDivRem805_rhs w := by
   unfold MulDivRem805_lhs MulDivRem805_rhs

SSA/Projects/Scf/ScfFunctor.lean

@@ -9,7 +9,6 @@ import SSA.Core.Tactic
 import SSA.Core.ErasedContext
 import SSA.Core.Util
 
-open Std (BitVec)
 open Ctxt(Var)
 
 namespace ScfFunctor
@@ -491,7 +490,7 @@ theorem correct : Com.denote (lhs v0) Γv = Com.denote (rhs v0) Γv := by
   simp only [lhs, rhs, for_, axpy, cst, add]
   simp_peephole at Γv
   intros A B
-  simp only [Ctxt.Valuation.snoc, Var.casesOn, Ctxt.get?, Var.zero_eq_last, cast_eq]
+  simp only [Ctxt.Valuation.snoc, Var.casesOn, Ctxt.get?, Var.zero_eq_last, BitVec.cast_eq]
   rw [Scf.LoopBody.counterDecorator.const_index_fn_iterate (f' := fun v => v0 + v)] <;> try rfl
   simp only [add_left_iterate, nsmul_eq_mul, Int.mul_comm]
 

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f910a1ff8498ff25924fbd64b1748a0bc2edd88b",
+   "rev": "9b5453767f2f0aa5b454de21dd47874514b53dec",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -15,30 +15,30 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5",
+   "rev": "61cc01564763dc5650ff5576575eb7bc5d84809f",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6058ab8d938c5104eace7d0fb5ac17b21cb067b1",
+   "rev": "1de41af60894808271289f27bd1348448ad3aca0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c87908619cccadda23f71262e6898b9893bffa36",
+   "rev": "3c9678698f8b59489086d0c37f53b62e14678b17",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.40",
+   "inputRev": "v0.0.42-pre",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/mhuisi/lean4-cli.git",
@@ -55,20 +55,20 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "033082103b7b53f35ccee18702a995382503d6ef",
+   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "76800560a1efa8663ed89214fc1196c97b89ff89",
+   "rev": "e5bb136c344af28c9fc510ec6efa05466306413a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing-2024-08-03",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/acmepjz/md4lean",

lakefile.toml

@@ -4,7 +4,7 @@ defaultTargets = ["SSA"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "nightly-testing-2024-08-03"
+rev = "nightly-testing"
 
 [[require]]
 name = "Cli"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-08-03
+leanprover/lean4:nightly-2024-08-08