ci: update the Rust toolchain weekly - #656
Merged
Merged
Conversation
A weekly run of ci-workflows' rust-version action moves rust-toolchain.toml to the latest stable release, rewrites the fenix sha256 in flake.nix and updates the fenix and crane inputs in flake.lock, then opens a PR on update/rust-<version>. The PR is opened with GITHUB_TOKEN, so a maintainer closes and reopens it to run CI.
samuelburnham
force-pushed
the
ci/update-rust
branch
from
October 2, 2026 16:41
c723afc to
b448f0e
Compare
samuelburnham
marked this pull request as ready for review
October 2, 2026 19:56
samuelburnham
enabled auto-merge
October 2, 2026 19:56
arthurpaulino
approved these changes
Oct 2, 2026
johnchandlerburnham
added a commit
that referenced
this pull request
Oct 2, 2026
…to ix-certified Brings in e328da2 (Lean v4.33.1 -> v4.34.1) and 209699b (.github/workflows/update-rust.yml). The branch was on Lean v4.34.0. Conflicts (200 files): - Ix/Tc/Verify/** (155 files): deleted on this branch (docs/kernel.md, removal ledger), edited on main (4.34.1 deprecation renames). Resolved as deleted; nothing ported. - Ix/Compile/Verify/** (33 files): deleted at the old path. Main's edits were checked against the relocated copies by a three-way merge (base = fork point, ours = relocated copy, theirs = main): * 25 files relocated under their own names (Ix/Sharing/Verify/{SharingExact, SharingExactCanon,Tiered*,Uniform*}.lean, Ix/Ixon/Verify/TagN.lean) already contain every hunk of main's: the same renames (if_pos -> ite_eq_left, if_neg -> ite_eq_right, if_true -> ite_true, if_false -> ite_false, dif_pos -> dite_eq_left, List.getElem_inj -> List.Nodup.getElem_inj). The three-way result differs from the relocated copy only in TieredTier.lean (2 lines) and UniformGain.lean (2 lines), where main still writes Ix.Compile.Verify.SharingExact.* for the relocated Ix.Sharing.Verify.SharingExact.* (namespace only). * Codec, ExprCodec, ExprSpineCodec, ConstantCodec, ConstantTablesCodec (preserved as Ix/Ixon/Verify/{Basic,Expr,ExprSpine,Constant, ConstantTables}), CompileSharingCodec (its builder part is Ix/Sharing/Verify/Builder.lean), CompileMutualCodec, CompilePreseed (retired): main's hunks are renames only; nothing to port. * Audit/Statements.lean: main moved four roots from noChoice to standard. searchComponents_eq_via and SCtx.phiE_eq_fast already carry standard in Ix/Sharing/Verify/Audit/Statements.lean; Catalog.ofEnv_finite and BlockWireTablesWF.of_preseed are retired roots. Nothing to port. - Toolchain files: lean-toolchain and Benchmarks/{Catalog/RelocFixtureA, Catalog/RelocFixtureB,Compile,Compile/TruthMines,TruthMines}/lean-toolchain set to leanprover/lean4:v4.34.1; IxKernel/ and Models/SetTheory/ lean-toolchain set to the same (CI compares the four). - lakefile.lean, lake-manifest.json, flake.nix, Benchmarks/Compile/ {lakefile.toml,lake-manifest.json}: the branch's files with main's 4.34.1 revisions: LSpec d8eb3e0d (descends from the branch's 369c09df), Blake3.lean 3f8b8056 (descends from the branch's c32002ee), Mathlib v4.34.1 (d13f23b7) in Benchmarks/Compile. Cli and batteries stay at v4.34.0 (as on main). The lean4lean (lean4ix) require, its manifest entries and its flake depOverride stay removed, as the branch retired them; main's bump of that pin is dropped. Main's 38-line change to the Benchmarks manifest is 19 revision bumps (no entries removed). - flake.lock: main's (lean4-nix e828640c, which descends from the branch's c8bce665 and adds v4.34.1; Blake3.lean 3f8b8056). The inputs are the same on both sides; `nix flake lock` on the merged tree leaves it unchanged. Semantic merge (files both sides changed without textual overlap): - primitives.tsv, prim_addrs.rs, Ix/Tc/Primitive.lean, Ix/IxVM/Kernel/ NatPrim.lean, aiur_ixvm.rs: both sides made identical edits (the same six rows: Nat.bitwise, Nat.land, Nat.lor, Nat.xor, String.back, String.Legacy.back), so 4.34.0 and 4.34.1 agree on every primitive address; confirmed by the tools on the merged tree. - Tests/Ix/Kernel/PrimeGapsReduction.lean: main replaced the deprecated Bool.and'/or'/not' with Bool.and/or/not; the branch kept the primed terms under `set_option linter.deprecated false`. Both merged cleanly into a file with unprimed terms under a now-false comment; took main's file. Nothing pins the primed terms (the original addresses are informational). - Ix/Lib.lean, Ix/Sharing/Exact/*: identical on both sides. Models/SetTheory: Mathlib rev v4.34.0 -> v4.34.1 (lakefile.toml), manifest refreshed by `lake -d Models/SetTheory update`.
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
2 participants
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.
A weekly run of ci-workflows' rust-version action moves
rust-toolchain.tomlto the latest stable release, rewrites the fenix sha256 in flake.nix and updates the fenix and crane inputs in flake.lock, then opens a PR onupdate/rust-<version>. The PR is opened with GITHUB_TOKEN, so a maintainer closes and reopens it to run CI.