chore: update to nightly-testing-2024-07-16 (#472)

SSA/Core/Framework.lean

@@ -745,7 +745,7 @@ def Com.changeVars : Com d Γ eff ty →
     Com d Γ' eff ty
   |  .ret e => fun varsMap => .ret (varsMap e)
   |  .var e body => fun varsMap => .var (e.changeVars varsMap)
-      (body.changeVars (fun t v => varsMap.snocMap v))
+      (body.changeVars (fun _ v => varsMap.snocMap v))
 
 /-! simp-lemmas about `changeVars`-/
 

SSA/Core/MLIRSyntax/EDSL.lean

@@ -94,3 +94,5 @@ def elabIntoCom (region : TSyntax `mlir_region) (d : Q(Dialect)) {φ : Q(Nat)}
           | .none => throwError "Expected (Sigma.mk _ _), found {expr}"
         | .none => throwError "Expected (Sigma.mk _ _), found {expr}"
     | .none => throwError "Expected `Except.ok`, found {com}"
+
+end SSA

SSA/Core/MLIRSyntax/PrettyEDSL.lean

@@ -44,3 +44,5 @@ macro_rules
       | some _ => #[t]
       | none => #[]
     `([mlir_op| $[$resName =]? $opName ($xs,*) : ($argTys,*) -> ($retTy:mlir_type,*) ])
+
+end MLIR.EDSL.Pretty

SSA/Projects/CSE/CSE.lean

@@ -484,3 +484,5 @@ info: {
 end Examples
 
 end CSE
+
+end DecEqCom

SSA/Projects/FullyHomomorphicEncryption/PrettySyntax.lean

@@ -70,3 +70,9 @@ private def fhe_test_one_rhs := [poly q, n, h | {
   }]
 
 end Test
+
+end Pretty
+
+end EDSL
+
+end MLIR

SSA/Projects/InstCombine/ForMathlib.lean

@@ -88,3 +88,5 @@ instance : CommRing (BitVec w) :=
   toFin_injective.commRing _
     toFin_zero toFin_one toFin_add toFin_mul toFin_neg toFin_sub
     toFin_nsmul toFin_zsmul toFin_pow toFin_natCast toFin_intCast
+
+end BitVec

SSA/Projects/InstCombine/LLVM/PrettyEDSL.lean

@@ -148,3 +148,7 @@ private def antiquot_test_pretty (x : Nat) := -- antiquotated constant value in
 example : antiquot_test = antiquot_test_pretty := rfl
 
 end Test
+
+end EDSL
+
+end MLIR

SSA/Projects/InstCombine/PaperExamples.lean

@@ -84,3 +84,5 @@ theorem bitvec_AddSub_1309 :
 info: 'AlivePaperExamples.bitvec_AddSub_1309' depends on axioms: [propext, Classical.choice, Quot.sound]
 -/
 #guard_msgs in #print axioms bitvec_AddSub_1309
+
+end AlivePaperExamples

SSA/Projects/InstCombine/update_alive_statements.py

@@ -63,6 +63,9 @@ def getStatement(preamble: List[str], id : int, proof: List[str]) -> str:
             name = line.split(" ")[3][0:-1]
         else:
             rewritten.append(line)
+    rewritten.append("\n\n")
+    rewritten.append("end AliveAutoGenerated\n")
+
     f.write("".join(rewritten))
     f.close()
 

SSA/Projects/LeanMlirCommon/SimplyTyped/Basic.lean

@@ -175,3 +175,9 @@ def Lets.recOn {Γ_out} {motive : ∀ {Γ_in}, Lets Op Γ_in Γ_out → Sort u}
       cast (by rfl) <| lete e lets
       --    ^^^^^^ the cast seems redundant, but Lean gives a type-error without it
       --           Similarly, term-mode `rfl` doesn't work, the `by` is needed
+
+end
+
+end SimplyTyped
+
+end MLIR

SSA/Projects/LeanMlirCommon/SimplyTyped/Substitution.lean

@@ -35,3 +35,7 @@ theorem Expr.WellTyped_of_substitute {e : UnTyped.Expr Op VarName}
   · aesop
 
 end
+
+end SimplyTyped
+
+end MLIR

SSA/Projects/Scf/ScfFunctor.lean

@@ -638,3 +638,5 @@ attribute [local simp] Ctxt.snoc
 --   }
 
 end IterateIdentity
+
+end ScfFunctor

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "39e0ffedb7fe061bbb5602539efd13ea61906da9",
+   "rev": "c4a1a9344315093fe0f70096a23651009d4b843b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "27990300a94dd6789254c2ffef4023896d3717c6",
+   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,10 +65,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "19f128e74b05759d18a7b43d96c2444279b75bba",
+   "rev": "dc7e2432738bfaddcda89afff0d692bf62db7e00",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing-2024-07-11",
+   "inputRev": "nightly-testing-2024-07-16",
    "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-07-11"
+rev = "nightly-testing-2024-07-16"
 
 [[require]]
 name = "Cli"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-07-11
+leanprover/lean4:nightly-2024-07-16