Bump lean to v4.26.0-rc2

.devcontainer/Dockerfile

@@ -14,5 +14,5 @@ RUN apt-get update && \
 USER vscode
 WORKDIR /home/vscode
 
-RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.25.1
+RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.26.0-rc2
 ENV PATH="/home/vscode/.elan/bin:${PATH}"

.devcontainer/devcontainer.json

@@ -16,7 +16,7 @@
 			"version": "22"
 		}
 	},
-	"postStartCommand": "rm -rf .lake/ && lake exe cache get && npm ci",
+	"onCreateCommand": "rm -rf .lake/ && lake exe cache get && npm ci",
 	"mounts": [
 		"source=lean-project-commandhistory,target=/commandhistory,type=volume"
 	],

README.md

@@ -2,7 +2,7 @@
 
 ```bash
 $ lake build
-Build completed successfully (574 jobs).
+Build completed successfully (579 jobs).
 ```
 
 ## How to use
@@ -20,7 +20,6 @@ Build completed successfully (574 jobs).
 ### VSCode Extensions
 
 - [ms-vscode-remote.remote-containers](https://marketplace.visualstudio.com/items?itemName=ms-vscode-remote.remote-containers)
-- [github.copilot](https://marketplace.visualstudio.com/items?itemName=GitHub.copilot)
 - [github.copilot-chat](https://marketplace.visualstudio.com/items?itemName=GitHub.copilot-chat)
 
 ### MCP Servers

lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0df2e3c2047ada0d7a2e33dbc6ba2788a44a6062",
+   "rev": "d5c9558e75342a10d6321e6a8c798a14f68ae23c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.25.1",
+   "inputRev": "v4.26.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0203092c2e5e26edf967000f0e177cf31c72e17a",
+   "rev": "74835c84b38e4070b8240a063c6417c767e551ae",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3611075024b3529e5798e53c733671039f06f0bd",
+   "rev": "6e3bb4bf31f731ab28891fe229eb347ec7d5dad3",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "135329b50b116dcc2c021c318c365e82a048856f",
+   "rev": "2aaad968dd10a168b644b6a5afd4b92496af4710",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.80",
+   "inputRev": "v0.0.82",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a2e4d9e9aebdbdce1ce6b6f0a19dd49e0120c990",
+   "rev": "9c70abdd9215b76019340fad65138e2e8d21843e",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9bff22d64abde45944c7b1f55bce6c89dd8307e6",
+   "rev": "a31845b5557fd5e47d52b9e2977a1b0eff3c38c3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ffad3f5b7ebe1ac3e09779ec8a863a5138c1246c",
+   "rev": "afe9302d9243cee630b0be95322b38b90342ddbf",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "cd188c6ecfbf6c00cf639e4d4fb18bf773ce8c2c",
+   "rev": "7e1ced9e049a4fab2508980ec4877ca9c46dffc9",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.25.1",
+   "inputRev": "v4.26.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Project",

lakefile.toml

@@ -4,8 +4,9 @@ defaultTargets = ["Project"]
 
 [[lean_lib]]
 name = "Project"
+leanOptions = { warningAsError = true }
 
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "v4.25.1"
+rev = "v4.26.0-rc2"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.25.1
+leanprover/lean4:v4.26.0-rc2