chore: Update Lean to v4.33.1

.github/workflows/update.yml

@@ -24,20 +24,31 @@ jobs:
           client-id: ${{ secrets.TOKEN_APP_ID }}
           private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}
 
-      # `dev` carries the fork's bump_mode/release_channel support; `main` only
-      # mirrors upstream, which silently ignores these inputs. A PR is opened
-      # on an update/lean-{release} branch whether or not the build passes, so
-      # an incompatible release shows up as a failing PR to review. Dependencies
-      # pinned to a Lean version tag move with the toolchain; a dependency
-      # pinned to a commit hash is reported and left alone.
-      - uses: argumentcomputer/lean-update@dev
+      # `exclude-dir` carries the fork's bump_mode/release_channel support plus
+      # the `!` exclusion syntax below; `main` only mirrors upstream, which
+      # silently ignores these inputs. Move back to `dev` once the exclusion
+      # lands there. A PR is opened on an update/lean-{release} branch whether
+      # or not the build passes, so an incompatible release shows up as a
+      # failing PR to review. Dependencies pinned to a Lean version tag move
+      # with the toolchain; a dependency pinned to a commit hash is reported
+      # and left alone.
+      - uses: argumentcomputer/lean-update@exclude-dir
         with:
-          # The root package plus every package under Benchmarks/ — `/**`
-          # walks the whole tree (catching Catalog's nested fixture
-          # workspaces) and skips dotted directories, so `.lake`
-          # dependency checkouts are never swept up. This includes
-          # Benchmarks/CompileFC, previously pinned to an old toolchain.
-          lake_package_directory: ". Benchmarks/**"
+          # The root package plus the benchmark packages. `/**` walks a whole
+          # subtree, reaching packages nested inside another package (Catalog's
+          # relocation fixtures, Compile's TruthMines) and skipping dotted
+          # directories so `.lake` dependency checkouts are never swept up.
+          #
+          # `!` subtracts a directory and everything beneath it, so the glob can
+          # cover Benchmarks while sparing CompileFC, which must stay pinned: it
+          # builds against formal-conjectures at a commit hash, which the action
+          # leaves alone, so moving its toolchain off v4.27.0 only breaks the
+          # build. An exclusion takes no glob of its own, and one matching
+          # nothing is reported in the log rather than passing silently.
+          lake_package_directory: >-
+            .
+            Benchmarks/**
+            !Benchmarks/CompileFC
           bump_mode: pinned-tags
           pr: true
           token: ${{ steps.app-token.outputs.token }}

lakefile.lean

@@ -7,13 +7,15 @@ package ix where
 require LSpec from git
   "https://github.com/argumentcomputer/LSpec" @ "ab4d5eb461941837f48eb891be755c8c73e89fdd"
 
-/- Blake3's `blake3_rs_shared` target builds `blake3-rs` as a `cdylib`
-alongside the staticlib. `ix_native_decide_dynlib` fetches it to supply the
-BLAKE3 backend to Lean's native evaluator, and that dynlib gates every
-`IxTcVerify` module, so this pin must stay at or after the revision that
-introduced the target. -/
+/- Blake3 precompiles its libraries, so Lake loads their shared objects -- which
+bundle the C and Rust FFI objects -- into any process elaborating a module that
+imports them. That is what supplies the BLAKE3 backend to Lean's native evaluator
+for the `native_decide` proofs in `IxTcVerify`, so this pin must stay at or after
+the revision that turned precompilation on. Before it, Blake3 exposed a
+`blake3_rs_shared` cdylib that `ix_native_decide_dynlib` had to fetch and link;
+that target no longer exists. -/
 require Blake3 from git
-  "https://github.com/argumentcomputer/Blake3.lean" @ "1b0fbd2bd78b2b873e14264037af8c8b1536b9e9"
+  "https://github.com/argumentcomputer/Blake3.lean" @ "5ff5e70b6c7fc371cc6b454b83844f1f5b44ac96"
 
 require Cli from git
   "https://github.com/leanprover/lean4-cli" @ "v4.33.0"
@@ -197,29 +199,20 @@ opaque `@[extern]` it reaches, both symbol layers must be loadable up front:
 * the raw Rust symbol it forwards to, taken from that crate's `cdylib`, recorded
   by absolute path so no `LD_LIBRARY_PATH` is needed.
 
-Covered externs: `Blake3.Rust` hashing (with the `Blake3` base module, which
-holds the `HasherOps.hash` orchestration `Address.blake3` calls) against
-`blake3_rs`, and `Ix.Unsigned.toLEBytes` against `ix-ffi-dyn`. -/
+Covers Ix's own externs only -- currently `Ix.Unsigned.toLEBytes` against
+`ix-ffi-dyn`. Blake3's are not here: that package precompiles its libraries, so
+Lake loads their shared objects into the elaborating process by itself. -/
 target ix_native_decide_dynlib pkg : Dynlib := do
-  let some blake3Base ← findModule? `Blake3
-    | error "module `Blake3` not found; is the Blake3 dependency available?"
-  let some blake3Rust ← findModule? `Blake3.Rust
-    | error "module `Blake3.Rust` not found; is the Blake3 dependency available?"
   let some ixUnsigned ← findModule? `Ix.Unsigned
     | error "module `Ix.Unsigned` not found"
-  -- Raw symbols come from each crate's cdylib, recorded by path, and are built
-  -- by fetching the owning package's target (no direct cargo calls here):
-  -- Blake3 via its `blake3_rs_shared`, Ix via the minimal `ix_ffi_dyn`.
-  let blake3Cdylib := (← blake3Rust.pkg.fetchTargetJob `blake3_rs_shared).map fun _ =>
-    blake3Rust.pkg.dir / "rust" / "target" / "release" / nameToSharedLib "blake3_rs"
+  -- Raw symbols come from the crate's cdylib, recorded by path, and are built
+  -- by fetching the owning target (no direct cargo calls here).
   let ixCdylib ← ix_ffi_dyn.fetch
-  -- Boxed entry points are Lean's own generated objects for the declaring modules.
-  let mut boxedObjs := #[]
-  for mod in #[blake3Base, blake3Rust, ixUnsigned] do
-    boxedObjs := boxedObjs ++ (← (mod.nativeFacets true).mapM (·.fetch mod))
+  -- Boxed entry points are Lean's own generated objects for the declaring module.
+  let boxedObjs ← (ixUnsigned.nativeFacets true).mapM (·.fetch ixUnsigned)
   buildSharedLib "ix_native_decide"
     (pkg.buildDir / nameToSharedLib "ix_native_decide")
-    (boxedObjs.push blake3Cdylib |>.push ixCdylib) #[]
+    (boxedObjs.push ixCdylib) #[]
 
 /- Formal verification of `Ix.Tc` against the lean4lean `Theory` spec.
 Non-default: `lake build ix` never