From 0ba9a4ded6beb0f2ccc45fc2c875ac0da86e1ca0 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 27 Aug 2026 14:32:59 -0400 Subject: [PATCH 1/4] ci: Exclude CompileFC from lean-update MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CompileFC builds against formal-conjectures pinned to a commit hash, which lean-update reports and leaves alone, and mathlib reaches it as an inherited dependency at v4.27.0. Bumping only its lean-toolchain — which #591 opted it into by globbing Benchmarks/** — therefore pairs a v4.33.1 toolchain with a v4.27.0 mathlib and cannot build. The v4.33.1 PR branch had exactly that bump as its sole remaining change. The action's lake_package_directory accepts literal paths, /* and /**, with no exclusion syntax, so the package list is enumerated instead. /** matches descendants only, hence Benchmarks/Compile listed alongside Benchmarks/Compile/**. The resulting set is unchanged apart from CompileFC: root, Catalog's two relocation fixtures, Compile, Compile/TruthMines, TruthMines. --- .github/workflows/update.yml | 23 +++++++++++++++++------ 1 file changed, 17 insertions(+), 6 deletions(-) diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml index a5089f05..4c6bb647 100644 --- a/.github/workflows/update.yml +++ b/.github/workflows/update.yml @@ -32,12 +32,23 @@ jobs: # pinned to a commit hash is reported and left alone. - uses: argumentcomputer/lean-update@dev 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; it + # matches descendants only, hence Benchmarks/Compile alongside it. + # + # The list is spelled out rather than globbed as Benchmarks/** because + # the action has no exclusion syntax and Benchmarks/CompileFC 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. A new benchmark package has to be added here. + lake_package_directory: >- + . + Benchmarks/Catalog/** + Benchmarks/Compile + Benchmarks/Compile/** + Benchmarks/TruthMines bump_mode: pinned-tags pr: true token: ${{ steps.app-token.outputs.token }} From 024bc5192a00e58fa151af51c43a8431994c16da Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 27 Aug 2026 21:19:46 -0400 Subject: [PATCH 2/4] lakefile: drop Blake3 from the native-decide dynlib Blake3 now 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. The Blake3 half of `ix_native_decide_dynlib` was assembling that by hand from a `blake3_rs_shared` cdylib, and that target no longer exists upstream. The target keeps Ix's own externs, which nothing else supplies. Precompiling `Ix.Unsigned` instead would work, but only as its own library declared after `Ix`: both would claim the module, `Package.findModule?` resolves with `findSomeRev?`, and losing that race silently stops precompiling it -- with the symptom appearing as a missing native implementation inside a proof file rather than as a configuration error. A local dynlib naming its modules outright is worth more than the lines it costs. --- lakefile.lean | 39 ++++++++++++++++----------------------- 1 file changed, 16 insertions(+), 23 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 40936169..44606054 100644 --- a/lakefile.lean +++ b/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 From cdcc54b72304aed45b8b0c8b6b6c2ae0c151e466 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 27 Aug 2026 22:20:34 -0400 Subject: [PATCH 3/4] ci: Glob Benchmarks and exclude CompileFC by name lean-update gained a `!` prefix on `lake_package_directory` that subtracts a directory and everything beneath it, so the enumerated package list can go back to a `Benchmarks/**` sweep with CompileFC carved out by name. CompileFC still has to stay pinned: it builds against formal-conjectures at a commit hash, which the action reports and leaves alone, so moving its toolchain off v4.27.0 only breaks the build. The resulting set is unchanged -- root, Catalog's two relocation fixtures, Compile, Compile/TruthMines, TruthMines -- but a benchmark package added later is now swept up on its own rather than needing a line here, which is what the enumeration got wrong. Tracks the action's `exclude-dir` branch until the exclusion reaches `dev`. --- .github/workflows/update.yml | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml index 4c6bb647..719d1684 100644 --- a/.github/workflows/update.yml +++ b/.github/workflows/update.yml @@ -24,31 +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 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; it - # matches descendants only, hence Benchmarks/Compile alongside it. + # directories so `.lake` dependency checkouts are never swept up. # - # The list is spelled out rather than globbed as Benchmarks/** because - # the action has no exclusion syntax and Benchmarks/CompileFC 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. A new benchmark package has to be added here. + # `!` 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/Catalog/** - Benchmarks/Compile - Benchmarks/Compile/** - Benchmarks/TruthMines + Benchmarks/** + !Benchmarks/CompileFC bump_mode: pinned-tags pr: true token: ${{ steps.app-token.outputs.token }} From a82579a0ac689b5a7d71881db4c641f51bbdda90 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 27 Aug 2026 22:44:49 -0400 Subject: [PATCH 4/4] chore: Update lean4-nix to e014934 Carries the lean4-nix support for the v4.33.1 toolchain this branch moves to, so the Nix build tracks the same Lean release as lean-toolchain. Only this input moves; nothing else in the lock changes. --- flake.lock | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/flake.lock b/flake.lock index a5b07edb..c2cf58b1 100644 --- a/flake.lock +++ b/flake.lock @@ -255,11 +255,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1787412565, - "narHash": "sha256-M1y7JYDUzvOSYv0DWcCCmkL2DqDfQZePsKDrQf/Or6U=", + "lastModified": 1787593167, + "narHash": "sha256-TJ/Lq/p8sXXINpodMSjpotERiCoDfoJDuvBn+bVL9Y8=", "owner": "argumentcomputer", "repo": "lean4-nix", - "rev": "1ecad9d6f99cf3255a858861c9a2e6966cdd0290", + "rev": "e014934f9c2b634aea3be072c7b0e6053a5cb211", "type": "github" }, "original": {