From f0cee7187dcd63d47af6682410d4f0233f42fa9e Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Fri, 12 Sep 2025 16:41:37 +0200
Subject: [PATCH] chore: update to 4.23.0-rc2

---
 lake-manifest.json | 80 ++++++++++++----------------------------------
 lakefile.lean      |  2 +-
 lean-toolchain     |  2 +-
 3 files changed, 22 insertions(+), 62 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 8560027..1b4505a 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,17 +1,7 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/doc-gen4",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "061dfa3b4207216f7c7a7f63e99421f551059687",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0-rc3",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/PatrickMassot/checkdecls.git",
+ [{"url": "https://github.com/PatrickMassot/checkdecls.git",
    "type": "git",
    "subDir": null,
    "scope": "",
@@ -35,57 +25,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0faf9c7e5dce691f1a9e2e5dc1aa2499e9acb2e0",
+   "rev": "839e741740619e20759a7153fd93b5c7d8df13e0",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/mhuisi/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "e22ed0883c7d7f9a7e294782b6b137b783715386",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "bb6eb5b25892aa968e9d35f6ef9ca5c6b896c16d",
-   "name": "UnicodeBasic",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/dupuisf/BibtexQuery",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "dbfe2b7630c5f7c5c1cf71e7747ffc0a30337f69",
-   "name": "BibtexQuery",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/acmepjz/md4lean",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "b16338c5c66f57ef5510d4334eb6fa4e2c6c8cd8",
-   "name": "MD4Lean",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "61c44bec841faabd47d11c2eda15f57ec2ffe9d5",
+   "rev": "240eddc1bb31420fbbc57fe5cc579435c2522493",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "140dc642f4f29944abcdcd3096e8ea9b4469c873",
+   "rev": "7c02243c07b61d493d7607ede432026781a3e47c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -115,17 +65,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "96c67159f161fb6bf6ce91a2587232034ac33d7e",
+   "rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.67",
+   "inputRev": "v0.0.71",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a62ecd0343a2dcfbcac6d1e8243f5821879c0244",
+   "rev": "3b779e9d1c73837a3764d516d81f942de391b6f0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -135,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "867d9dc77534341321179c9aa40fceda675c50d4",
+   "rev": "f85ad59c9b60647ef736719c23edd4578f723806",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -145,11 +95,21 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3cabaef23886b82ba46f07018f2786d9496477d6",
+   "rev": "a9a0cb7672b7134497c9d813e53999c9311f4037",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "cacb481a1eaa4d7d4530a27b606c60923da21caf",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Poly",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index e4e5822..42e298b 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -21,4 +21,4 @@ require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"
 
 meta if get_config? env = some "dev" then
 require «doc-gen4» from git
-  "https://github.com/leanprover/doc-gen4" @ "v4.22.0-rc3"
+  "https://github.com/leanprover/doc-gen4" @ "v4.23.0-rc2"
diff --git a/lean-toolchain b/lean-toolchain
index 28f76d1..27770b5 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.22.0-rc3
\ No newline at end of file
+leanprover/lean4:v4.23.0-rc2
\ No newline at end of file