diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index 7430f32..2c81c7f 100644 --- a/.devcontainer/Dockerfile +++ b/.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}" diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 51fdc9b..9af9e7f 100644 --- a/.devcontainer/devcontainer.json +++ b/.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" ], diff --git a/README.md b/README.md index cbb03ff..86c2492 100644 --- a/README.md +++ b/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 diff --git a/lake-manifest.json b/lake-manifest.json index 5b727d9..45532ab 100644 --- a/lake-manifest.json +++ b/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", diff --git a/lakefile.toml b/lakefile.toml index c7293d7..7948487 100644 --- a/lakefile.toml +++ b/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" diff --git a/lean-toolchain b/lean-toolchain index 4bd92b6..be1fbc3 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.25.1 +leanprover/lean4:v4.26.0-rc2 diff --git a/package-lock.json b/package-lock.json index 1217de5..302fd80 100644 --- a/package-lock.json +++ b/package-lock.json @@ -4,6 +4,7 @@ "requires": true, "packages": { "": { + "name": "lean-project", "devDependencies": { "@commitlint/cli": "20.1.0", "@commitlint/config-conventional": "20.0.0", @@ -1628,76 +1629,6 @@ "lefthook-windows-x64": "2.0.4" } }, - "node_modules/lefthook-darwin-arm64": { - "version": "2.0.4", - "resolved": "https://registry.npmjs.org/lefthook-darwin-arm64/-/lefthook-darwin-arm64-2.0.4.tgz", - "integrity": "sha512-AR63/O5UkM7Sc6x5PhP4vTuztTYRBeBroXApeWGM/8e5uZyoQug/7KTh7xhbCMDf8WJv6vdFeXAQCPSmDyPU3Q==", - "cpu": [ - "arm64" - ], - "dev": true, - "license": "MIT", - "optional": true, - "os": [ - "darwin" - ] - }, - "node_modules/lefthook-darwin-x64": { - "version": "2.0.4", - "resolved": "https://registry.npmjs.org/lefthook-darwin-x64/-/lefthook-darwin-x64-2.0.4.tgz", - "integrity": "sha512-618DVUttSzV9egQiqTQoxGfnR240JoPWYmqRVHhiegnQKZ2lp5XJ+7NMxeRk/ih93VVOLzFO5ky3PbpxTmJgjQ==", - "cpu": [ - "x64" - ], - "dev": true, - "license": "MIT", - "optional": true, - "os": [ - "darwin" - ] - }, - "node_modules/lefthook-freebsd-arm64": { - "version": "2.0.4", - "resolved": "https://registry.npmjs.org/lefthook-freebsd-arm64/-/lefthook-freebsd-arm64-2.0.4.tgz", - "integrity": "sha512-mTAQym1BK38fKglHBQ/0GXPznVC4LoStHO5lAI3ZxaEC0FQetqGHYFzhWbIH5sde9JhztE2rL/aBzMHDoAtzSw==", - "cpu": [ - "arm64" - ], - "dev": true, - "license": "MIT", - "optional": true, - "os": [ - "freebsd" - ] - }, - "node_modules/lefthook-freebsd-x64": { - "version": "2.0.4", - "resolved": "https://registry.npmjs.org/lefthook-freebsd-x64/-/lefthook-freebsd-x64-2.0.4.tgz", - "integrity": "sha512-sy02aSxd8UMd6XmiPFVl/Em0b78jdZcDSsLwg+bweJQQk0l+vJhOfqFiG11mbnpo+EBIZmRe6OH5LkxeSU36+w==", - "cpu": [ - "x64" - ], - "dev": true, - "license": "MIT", - "optional": true, - "os": [ - "freebsd" - ] - }, - "node_modules/lefthook-linux-arm64": { - "version": "2.0.4", - "resolved": "https://registry.npmjs.org/lefthook-linux-arm64/-/lefthook-linux-arm64-2.0.4.tgz", - "integrity": "sha512-W0Nlr/Cz2QTH9n4k5zNrk3LSsg1C4wHiJi8hrAiQVTaAV/N1XrKqd0DevqQuouuapG6pw/6B1xCgiNPebv9oyw==", - "cpu": [ - "arm64" - ], - "dev": true, - "license": "MIT", - "optional": true, - "os": [ - "linux" - ] - }, "node_modules/lefthook-linux-x64": { "version": "2.0.4", "resolved": "https://registry.npmjs.org/lefthook-linux-x64/-/lefthook-linux-x64-2.0.4.tgz", @@ -1712,62 +1643,6 @@ "linux" ] }, - "node_modules/lefthook-openbsd-arm64": { - "version": "2.0.4", - "resolved": "https://registry.npmjs.org/lefthook-openbsd-arm64/-/lefthook-openbsd-arm64-2.0.4.tgz", - "integrity": "sha512-VmOhJO3pYzZ/1C2WFXtL/n5pq4/eYOroqJJpwTJfmCHyw4ceLACu8MDyU5AMJhGMkbL8mPxGInJKxg5xhYgGRw==", - "cpu": [ - "arm64" - ], - "dev": true, - "license": "MIT", - "optional": true, - "os": [ - "openbsd" - ] - }, - "node_modules/lefthook-openbsd-x64": { - "version": "2.0.4", - "resolved": "https://registry.npmjs.org/lefthook-openbsd-x64/-/lefthook-openbsd-x64-2.0.4.tgz", - "integrity": "sha512-U8MZz1xlHUdflkQQ2hkMQsei6fSZbs8tuE4EjCIHWnNdnAF4V8sZ6n1KbxsJcoZXPyBZqxZSMu1o/Ye8IAMVKg==", - "cpu": [ - "x64" - ], - "dev": true, - "license": "MIT", - "optional": true, - "os": [ - "openbsd" - ] - }, - "node_modules/lefthook-windows-arm64": { - "version": "2.0.4", - "resolved": "https://registry.npmjs.org/lefthook-windows-arm64/-/lefthook-windows-arm64-2.0.4.tgz", - "integrity": "sha512-543H3y2JAwNdvwUQ6nlNBG7rdKgoOUgzAa6pYcl6EoqicCRrjRmGhkJu7vUudkkrD2Wjm7tr9hU9poP2g5fRFQ==", - "cpu": [ - "arm64" - ], - "dev": true, - "license": "MIT", - "optional": true, - "os": [ - "win32" - ] - }, - "node_modules/lefthook-windows-x64": { - "version": "2.0.4", - "resolved": "https://registry.npmjs.org/lefthook-windows-x64/-/lefthook-windows-x64-2.0.4.tgz", - "integrity": "sha512-UDEPK9RWKm60xsNOdS/DQOdFba0SFa4w3tpFMXK1AJzmRHhosoKrorXGhtTr6kcM0MGKOtYi8GHsm++ArZ9wvQ==", - "cpu": [ - "x64" - ], - "dev": true, - "license": "MIT", - "optional": true, - "os": [ - "win32" - ] - }, "node_modules/lines-and-columns": { "version": "1.2.4", "resolved": "https://registry.npmjs.org/lines-and-columns/-/lines-and-columns-1.2.4.tgz",