Update Lean to v4.31.0

lake-manifest.json

@@ -1,21 +1,21 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5e932f97dd25535344f80f9dd8da3aab83df0fe6",
+   "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.1",
+   "inputRev": "v4.31.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3",
+   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "48d5698bc464786347c1b0d859b18f938420f060",
+   "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4dd0959c44d1af0462bd604d0f87c5781307d709",
+   "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.95+lean-v4.29.1",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7152850e7b216a0d409701617721b6e469d34bf6",
+   "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d",
+   "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "756e3321fd3b02a85ffda19fef789916223e578c",
+   "rev": "fa08db58b30eb033edcdab331bba000827f9f785",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,11 +85,12 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29",
+   "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
+   "inputRev": "v4.31.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "proofs_lean",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

lakefile.toml

@@ -13,7 +13,7 @@ maxSynthPendingDepth = 3
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "v4.29.1"
+rev = "v4.31.0"
 
 [[lean_lib]]
 name = "proofs_lean"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.29.1
+leanprover/lean4:v4.31.0

toast.yml

@@ -86,9 +86,13 @@ tasks:
       - install_packages
     user: user
     command: |
-      # Install Rocq via opam.
+      # Install Rocq via opam. The `rocq-prover` package is a virtual package
+      # with unversioned dependencies on `rocq-core` and `rocq-stdlib`, so
+      # those two packages must be pinned explicitly.
       opam init --disable-sandboxing --yes
       eval "$(opam env)"
+      opam pin add --no-action rocq-core 9.0.0 --yes
+      opam pin add --no-action rocq-stdlib 9.0.0 --yes
       opam pin add rocq-prover 9.0.0 --yes
 
   install_tools: