chore: Update Lean to v4.33.1 - #593
Open
argument-ci-bot[bot] wants to merge 4 commits into
Open
Conversation
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.
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.
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`.
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.
samuelburnham
force-pushed
the
update/lean-v4.33.1
branch
from
August 28, 2026 02:47
d6764b5 to
a82579a
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
lean-toolchainand dependencies updated for Lean releasev4.33.1by lean-update.