fix: Improve Nix build & CI time - #657
Draft
samuelburnham wants to merge 5 commits into
Draft
samuelburnham wants to merge 5 commits into
samuelburnham wants to merge 5 commits into
Conversation
The dev-shell step compiles the Lean tree and the Rust workspace in the checkout, into the sticky disk's .lake and target directories, and never reads the derivations the sandboxed steps produce. Running it after them only serialized 6 to 11 minutes of work behind 9 to 21 minutes of Nix builds: on a kernel-touching PR the job took 33 minutes, and the step did the same amount of work it did when it was a separate job on a cold runner. The only shared state was the toolchain closure in /nix/store, which a fresh runner fetches from Cachix in under a minute. The sticky disk, sccache, and the RUSTFLAGS pin move with the step, since only the dev shell's cargo uses them. The merge-queue gate waits on both jobs.
Cargo compiles a dependency once per unified feature set. The `net` feature pulls in tokio and iroh, which enable extra features on serde, libc, once_cell, and other base crates, so a build without `net` sees different shapes for those crates than the deps-only derivation built with `parallel,test-ffi,net`, discards them, and recompiles the 57 crates above them, Plonky3 and multi-stark included. `test-ffi` declares no dependencies and changes nothing. Give the library and test builds `net` on non-macOS, matching the lakefile's `ix_rs_net`. The release and CLI builds then request the same features and collapse into one derivation, so a cache miss pays for one fewer workspace compile; the test build and nextest reuse the prebuilt dependencies like clippy already did. Measured locally with every cache forced to miss, each derivation built alone: the three package builds took 119 s, 110 s and 111 s before (two of them recompiling 57 dependencies) and the remaining two take 110 s each after, recompiling none. Wall time per build is unchanged because the workspace crates are the critical path; the saving is the removed build plus the CPU the recompiles consumed. nextest passes the same 1641 tests under both feature sets.
The executable derivations copied their whole Lake tree into the output: two copies of each 350 MB static library, the Lean library's own archive, C and IR intermediates, and a second copy of the binary. The CLI output came to 2.5 GB and IxTests to 3.8 GB, and most of each derivation's time went into writing that out and running patchelf over hundreds of non-ELF files, not into Lake. Nothing continues a build from an executable, so install only what the wrapper's LEAN_PATH serves at runtime: the binaries and the olean parts. The `.olean.server` and `.olean.private` parts stay because the toolchain's loader reads all three unconditionally for a module compiled in `module` mode, which is 107 of the CLI's 108 own modules and 99 of the test modules, and the tests import those through `get_env!`; removing them fails the import with "failed to open file". IR files are optional at load time and only serve the interpreter for declarations without native code, which these binaries all have. Measured locally, each derivation built alone: CLI 150 s, 2.5 GB -> 65 s, 653 MB IxTests 168 s, 3.8 GB -> 85 s, 1.1 GB Lake's own build phase is unchanged; the difference is the install and fixup. The Lean suite passes all 3461 tests.
lean4-nix now installs executables wrapped for standalone use, with the module files their imports read at runtime under `lib/lean`, so the hand-rolled olean install and `wrapBin` go. The outputs are self-contained: they no longer put the 1.2 GB `Ix` tree and every dependency tree on `LEAN_PATH`, so `nix run .#ix` fetches the toolchain and one 1.1 GB package instead of a 6 GB closure. The IR files stay out, as before, since every module these binaries can import is linked into them. The `Ix` library, which the executables continue from, is stored as a zstd archive: 270 MB instead of 1.2 GB. Packing and unpacking cost the same as copying the tree; the derivation is about 30 s faster only because Nix has one 270 MB file rather than 1.2 GB across 3400 files to fix up, scan and hash, and that smaller output is also what Cachix stores and every job downloads. The lean4-nix input points at the `install-modes` branch, which adds `installBin`, `binFiles` and `artifactsFormat`, until that branch is on `dev`; the URL then goes back to the default branch and the lock is bumped again.
samuelburnham
force-pushed
the
ci/split-nix-devshell
branch
from
October 2, 2026 16:05
d7564a4 to
9b62a57
Compare
lean4-nix now installs only the olean parts beside a binary unless a package asks for the IR files too, which is the set ix had been selecting by hand; the executable derivations are unchanged by dropping the override. The lock moves to the lean4-nix commit that changes the default.
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.
cargoArtifacts(parallel,net) so that dependencies don't have to be recompiled for different packages which is slow in Nix.test-ffiis a local-only feature so it doesn't add significant cost to recompile