From 28ff6cef4fb476886eeb96edc4ef518f98f027b7 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Wed, 23 Aug 2023 15:24:06 +1000
Subject: [PATCH] chore: bump to nightly-2023-08-19

---
 lean-toolchain                         |  2 +-
 test/bench/Basic.lean.leanInk.expected |  2 +-
 test/dep/lake-manifest.json            | 40 +++++++++++++++++++-------
 test/dep/lakefile.lean                 |  2 +-
 test/dep/lean-toolchain                |  2 +-
 5 files changed, 33 insertions(+), 15 deletions(-)

diff --git a/lean-toolchain b/lean-toolchain
index cbd5420..1b34910 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-06-07
+leanprover/lean4:nightly-2023-08-19
diff --git a/test/bench/Basic.lean.leanInk.expected b/test/bench/Basic.lean.leanInk.expected
index 714bbdd..f5825ea 100644
--- a/test/bench/Basic.lean.leanInk.expected
+++ b/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,
diff --git a/test/dep/lake-manifest.json b/test/dep/lake-manifest.json
index ce282b9..22ad2c8 100644
--- a/test/dep/lake-manifest.json
+++ b/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}}]}
diff --git a/test/dep/lakefile.lean b/test/dep/lakefile.lean
index 41c7635..27f4294 100644
--- a/test/dep/lakefile.lean
+++ b/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
diff --git a/test/dep/lean-toolchain b/test/dep/lean-toolchain
index cbd5420..1b34910 100644
--- a/test/dep/lean-toolchain
+++ b/test/dep/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-06-07
+leanprover/lean4:nightly-2023-08-19