Lean を v4.15.0 に更新

Author: Seasawher

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "ec10d9ba44225d66e790787d0f5b19a14830337e",
+   "rev": "c8e9d14233399d0c195b8dfd478fd96d4364fb10",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "ec10d9ba44225d66e790787d0f5b19a14830337e",
+   "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/Seasawher/mdgen",
@@ -25,10 +25,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35",
+   "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -45,10 +45,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377",
+   "rev": "9a0b533c2fbd6195df067630be18e11e4349051c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
@@ -65,30 +65,30 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a4a08d92be3de00def5298059bf707c72dfd3c66",
+   "rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac",
+   "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "v4.15.0",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f007bfe46ea8fb801ec907df9ab540054abcc5fd",
+   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",

lakefile.lean

@@ -24,7 +24,7 @@ require mdgen from git
   "https://github.com/Seasawher/mdgen" @ "main"
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @ "ec10d9ba44225d66e790787d0f5b19a14830337e"
+  "https://github.com/leanprover-community/mathlib4.git" @ "master"
 
 @[default_target]
 lean_lib LeanByExample where

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.15.0-rc1
+leanprover/lean4:v4.15.0