From 763b2f8b113afa078c46f5630cc3e70db8f1f470 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 2 Sep 2024 23:56:06 +0900
Subject: [PATCH 1/2] =?UTF-8?q?Lean=20=E3=81=AE=E3=83=90=E3=83=BC=E3=82=B8?=
 =?UTF-8?q?=E3=83=A7=E3=83=B3=E6=9B=B4=E6=96=B0?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 lake-manifest.json | 16 ++++++++--------
 lakefile.lean      |  2 +-
 lean-toolchain     |  2 +-
 3 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 0e0f54bd..838d6578 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "64a0a0f01d2a7600cdc48623e7c78a9ba27fd637",
+   "rev": "eb0d7623bfedcf9f64402b283e135b21036362ee",
    "name": "«mk-exercise»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "lean/v4.11.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/Seasawher/mdgen",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "1a02b7d8f0888b9ac0a007904349149f92d37bc5",
+   "rev": "bdfc2e355fbd5003be7094b3c99ff9d833aff7da",
    "name": "mdgen",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "31fb27d6b89dc94cf7349df247fc44d2a1d130af",
+   "rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
+   "rev": "9d0bdd07bdfe53383567509348b1fe917fc08de4",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33",
+   "rev": "deb279eb7be16848d0bc8387f80d6e41bcdbe738",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
+   "rev": "1ef0b288623337cb37edd1222b9c26b4b77c6620",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9295e9f3fa3ffe08fd0def1341bc68ade6ed60d2",
+   "rev": "0194b29f8e8bda212a44bbd34bf8b8c37a88db25",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
diff --git a/lakefile.lean b/lakefile.lean
index f2438beb..1bb0ec4f 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -8,7 +8,7 @@ package «Lean by Example» where
   ]
 
 require «mk-exercise» from git
-  "https://github.com/Seasawher/mk-exercise.git" @ "main"
+  "https://github.com/Seasawher/mk-exercise.git" @ "lean/v4.11.0"
 
 require mdgen from git
   "https://github.com/Seasawher/mdgen" @ "main"
diff --git a/lean-toolchain b/lean-toolchain
index e7a4f40b..5a9c76dc 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.11.0-rc2
+leanprover/lean4:v4.11.0

From 2d524755d8ec4f0f3372d18efa05d9d1a3d2eee0 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 3 Sep 2024 00:04:41 +0900
Subject: [PATCH 2/2] =?UTF-8?q?mk-exercise=20=E6=9B=B4=E6=96=B0?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 lake-manifest.json | 4 ++--
 lakefile.lean      | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 838d6578..cc0d6d50 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "eb0d7623bfedcf9f64402b283e135b21036362ee",
+   "rev": "8a8526d4747854dcbef1c552b3031d17e5a956c0",
    "name": "«mk-exercise»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "lean/v4.11.0",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/Seasawher/mdgen",
diff --git a/lakefile.lean b/lakefile.lean
index 1bb0ec4f..f2438beb 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -8,7 +8,7 @@ package «Lean by Example» where
   ]
 
 require «mk-exercise» from git
-  "https://github.com/Seasawher/mk-exercise.git" @ "lean/v4.11.0"
+  "https://github.com/Seasawher/mk-exercise.git" @ "main"
 
 require mdgen from git
   "https://github.com/Seasawher/mdgen" @ "main"