chore: Update Lean to v4.33.0

.github/workflows/update.yml

@@ -32,6 +32,9 @@ jobs:
       # pinned to a commit hash is reported and left alone.
       - uses: argumentcomputer/lean-update@dev
         with:
+          # The root package and the compile benchmarks; Benchmarks/CompileFC
+          # is deliberately left on its old toolchain, so no glob here.
+          lake_package_directory: ". Benchmarks/Compile"
           bump_mode: pinned-tags
-          on_update_fails: pr
+          pr: true
           token: ${{ steps.app-token.outputs.token }}

Benchmarks/Compile/lake-manifest.json

@@ -1,24 +1,24 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8a178386ffc0f5fef0b77738bb5449d50efeea95",
+   "rev": "db584cd6d46c92f209a44c0f1c829460d327499d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
+   "inputRev": "v4.33.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/ImperialCollegeLondon/FLT",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2d9083d31e10033122dedbcd9406389c2df5be86",
+   "rev": "45eb9afc55ce36516fc98ba10618c010fdced7dc",
    "name": "flt",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
+   "inputRev": "v4.33.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"type": "path",
@@ -32,7 +32,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3",
+   "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -42,7 +42,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -52,7 +52,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "48d5698bc464786347c1b0d859b18f938420f060",
+   "rev": "16f02aa7642864af59f1ff0e384a015994db9118",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -62,17 +62,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3",
+   "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.95",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7152850e7b216a0d409701617721b6e469d34bf6",
+   "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -82,7 +82,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d",
+   "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -92,22 +92,12 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "756e3321fd3b02a85ffda19fef789916223e578c",
+   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
    "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": "7802da01beb530bf051ab657443f9cd9bc3e1a29",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
   {"url": "https://github.com/PatrickMassot/checkdecls.git",
    "type": "git",
    "subDir": null,
@@ -118,35 +108,46 @@
    "inputRev": null,
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/digama0/lean4lean",
+  {"url": "https://github.com/argumentcomputer/lean4lean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8865b155abbf68d3a827fb3568bf6839780163c2",
+   "rev": "4844eda4fe376a7ab7e23a4b9755189d3c2ffe5b",
    "name": "lean4lean",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "8865b155abbf68d3a827fb3568bf6839780163c2",
+   "inputRev": "4844eda4fe376a7ab7e23a4b9755189d3c2ffe5b",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.33.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/argumentcomputer/Blake3.lean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
+   "rev": "730f910a59fe883cd71454bf186c7726a0c2d0d1",
    "name": "Blake3",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
+   "inputRev": "730f910a59fe883cd71454bf186c7726a0c2d0d1",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/argumentcomputer/LSpec",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
+   "rev": "e780f4188c9649aef988270f4d126651460ca9c4",
    "name": "LSpec",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
+   "inputRev": "e780f4188c9649aef988270f4d126651460ca9c4",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Compile",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

Benchmarks/Compile/lakefile.toml

@@ -33,9 +33,9 @@ path = "../.."
 [[require]]
 name = "flt"
 git = "https://github.com/ImperialCollegeLondon/FLT"
-rev = "v4.29.0"
+rev = "v4.33.0"
 
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "v4.29.0"
+rev = "v4.33.0"

Benchmarks/Compile/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.29.0
+leanprover/lean4:v4.33.0

Cargo.toml

@@ -38,8 +38,8 @@ ixon = { path = "crates/ixon" }
 ix-kernel = { path = "crates/kernel" }
 
 # lean-ffi tree (lean-ffi crate + factored-out bignat sub-crate)
-bignat = { git = "https://github.com/argumentcomputer/lean-ffi.git", rev = "839b405de708b80504fda39abe1402114b4135a5" }
-lean-ffi = { git = "https://github.com/argumentcomputer/lean-ffi.git", rev = "839b405de708b80504fda39abe1402114b4135a5" }
+bignat = { git = "https://github.com/argumentcomputer/lean-ffi.git", rev = "a6e781bc55cec99b99fa7a4bee105c5000cec967" }
+lean-ffi = { git = "https://github.com/argumentcomputer/lean-ffi.git", rev = "a6e781bc55cec99b99fa7a4bee105c5000cec967" }
 
 # External shared deps
 anyhow = "1"