From 05639fd07e0a42de814a1ad9f4c17e8bc95a663e Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Tue, 7 Nov 2023 19:02:23 -0700
Subject: [PATCH] Update toolchain.

---
 lake-manifest.json | 88 +++++++++++++++++++++++-----------------------
 lean-toolchain     |  2 +-
 2 files changed, 45 insertions(+), 45 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index df80128..b87adbe 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -2,30 +2,6 @@
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
-   {"url": "https://github.com/xubaiw/CMark.lean",
-    "subDir?": null,
-    "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
-    "opts": {},
-    "name": "CMark",
-    "inputRev?": "main",
-    "inherited": false}},
-  {"git":
-   {"url": "https://github.com/EdAyers/ProofWidgets4",
-    "subDir?": null,
-    "rev": "a0c2cd0ac3245a0dade4f925bcfa97e06dd84229",
-    "opts": {},
-    "name": "proofwidgets",
-    "inputRev?": "v0.0.13",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-    "subDir?": null,
-    "rev": "4ecf4f1f98d14d03a9e84fa1c082630fa69df88b",
-    "opts": {},
-    "name": "UnicodeBasic",
-    "inputRev?": "main",
-    "inherited": false}},
-  {"git":
    {"url": "https://github.com/mhuisi/lean4-cli",
     "subDir?": null,
     "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
@@ -34,29 +10,21 @@
     "inputRev?": "nightly",
     "inherited": false}},
   {"git":
-   {"url": "https://github.com/leanprover-community/mathlib4.git",
+   {"url": "https://github.com/xubaiw/CMark.lean",
     "subDir?": null,
-    "rev": "43718b8bde561e133edfd4ab8b5def9fb438c18d",
+    "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
     "opts": {},
-    "name": "mathlib",
-    "inputRev?": "master",
+    "name": "CMark",
+    "inputRev?": "main",
     "inherited": false}},
   {"git":
-   {"url": "https://github.com/gebner/quote4",
+   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
     "subDir?": null,
-    "rev": "e75daed95ad1c92af4e577fea95e234d7a8401c1",
+    "rev": "280d75fdfe7be8eb337be7f1bf8479b4aac09f71",
     "opts": {},
-    "name": "Qq",
-    "inputRev?": "master",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/JLimperg/aesop",
-    "subDir?": null,
-    "rev": "1a0cded2be292b5496e659b730d2accc742de098",
-    "opts": {},
-    "name": "aesop",
-    "inputRev?": "master",
-    "inherited": true}},
+    "name": "UnicodeBasic",
+    "inputRev?": "main",
+    "inherited": false}},
   {"git":
    {"url": "https://github.com/hargonix/LeanInk",
     "subDir?": null,
@@ -65,12 +33,44 @@
     "name": "leanInk",
     "inputRev?": "doc-gen",
     "inherited": false}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/mathlib4.git",
+    "subDir?": null,
+    "rev": "c97b9b00802c2ed343d9ac73e59be287428dbcf0",
+    "opts": {},
+    "name": "mathlib",
+    "inputRev?": "master",
+    "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover/std4.git",
     "subDir?": null,
-    "rev": "28459f72f3190b0f540b49ab769745819eeb1c5e",
+    "rev": "87b0742b01e45c6cc53cd3043fe3c7cdbf87a56f",
     "opts": {},
     "name": "std",
     "inputRev?": "main",
-    "inherited": false}}],
-"name": "«bookshelf»"}
+    "inherited": false}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/quote4",
+    "subDir?": null,
+    "rev": "511eb96eca98a7474683b8ae55193a7e7c51bc39",
+    "opts": {},
+    "name": "Qq",
+    "inputRev?": "master",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/aesop",
+    "subDir?": null,
+    "rev": "cb87803274405db79ec578fc07c4730c093efb90",
+    "opts": {},
+    "name": "aesop",
+    "inputRev?": "master",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/ProofWidgets4",
+    "subDir?": null,
+    "rev": "f1a5c7808b001305ba07d8626f45ee054282f589",
+    "opts": {},
+    "name": "proofwidgets",
+    "inputRev?": "v0.0.21",
+    "inherited": true}}],
+ "name": "bookshelf"}
diff --git a/lean-toolchain b/lean-toolchain
index 00004ee..734efdd 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc4
\ No newline at end of file
+leanprover/lean4:v4.3.0-rc1
\ No newline at end of file