chore: bump to nightly-2023-08-19

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-06-07
+leanprover/lean4:nightly-2023-08-19

test/bench/Basic.lean.leanInk.expected

@@ -980,7 +980,7 @@
     "The `simp` tactic uses lemmas and hypotheses to simplify the main goal target or\nnon-dependent hypotheses. It has many variants:\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged\n  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.\n  If an `hᵢ` is a defined constant `f`, then the equational lemmas associated with\n  `f` are used. This provides a convenient way to unfold `f`.\n- `simp [*]` simplifies the main goal target using the lemmas tagged with the\n  attribute `[simp]` and all hypotheses.\n- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.\n- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged\n  with the attribute `[simp]`, but removes the ones named `idᵢ`.\n- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If\n  the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis\n  `hᵢ` is introduced, but the old one remains in the local context.\n- `simp at *` simplifies all the hypotheses and the target.\n- `simp [*] at *` simplifies target and all (propositional) hypotheses using the\n  other hypotheses.\n",
     "_type": "token"},
    {"typeinfo":
-    {"type": "{α : Type ?u.3347} → [self : BEq α] → α → α → Bool",
+    {"type": "{α : Type ?u.3247} → [self : BEq α] → α → α → Bool",
      "name": "BEq.beq",
      "_type": "typeinfo"},
     "semanticType": null,

test/dep/lake-manifest.json

@@ -1,33 +1,51 @@
-{"version": 4,
+{"version": 5,
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
    {"url": "https://github.com/EdAyers/ProofWidgets4",
     "subDir?": null,
-    "rev": "3b157dc3f6162615de001a8ebe7e01d629c97448",
+    "rev": "a0c2cd0ac3245a0dade4f925bcfa97e06dd84229",
+    "opts": {},
     "name": "proofwidgets",
-    "inputRev?": "v0.0.10"}},
+    "inputRev?": "v0.0.13",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/mhuisi/lean4-cli.git",
+    "subDir?": null,
+    "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
+    "opts": {},
+    "name": "Cli",
+    "inputRev?": "nightly",
+    "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "932071475e7e89428d81af9d7b2fab6c0b88bf3c",
+    "rev": "cf479f4ee9e6e5e54f8b3ddea0011c3f816350d4",
+    "opts": {},
     "name": "mathlib",
-    "inputRev?": "932071475e7e89428d81af9d7b2fab6c0b88bf3c"}},
+    "inputRev?": "cf479f4ee9e6e5e54f8b3ddea0011c3f816350d4",
+    "inherited": false}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
-    "rev": "c71f94e34c1cda52eef5c93dc9da409ab2727420",
+    "rev": "81cc13c524a68d0072561dbac276cd61b65872a6",
+    "opts": {},
     "name": "Qq",
-    "inputRev?": "master"}},
+    "inputRev?": "master",
+    "inherited": true}},
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "ca73109cc40837bc61df8024c9016da4b4f99d4c",
+    "rev": "086c98bb129ca856381d4414dc0afd6e3e4ae2ef",
+    "opts": {},
     "name": "aesop",
-    "inputRev?": "master"}},
+    "inputRev?": "master",
+    "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "d5471b83378e8ace4845f9a029af92f8b0cf10cb",
+    "rev": "49353fa54abdac7221fe27f7b57a6ed9ff559d5c",
+    "opts": {},
     "name": "std",
-    "inputRev?": "main"}}]}
+    "inputRev?": "main",
+    "inherited": true}}]}

test/dep/lakefile.lean

@@ -3,7 +3,7 @@ open Lake DSL
 
 package dep
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "932071475e7e89428d81af9d7b2fab6c0b88bf3c"
+require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "cf479f4ee9e6e5e54f8b3ddea0011c3f816350d4"
 
 @[default_target]
 lean_lib dep

test/dep/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-06-07
+leanprover/lean4:nightly-2023-08-19