From 769e15c0d20a07d816381764ca3f32a3a41bb767 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 1 Oct 2026 19:43:08 -0400 Subject: [PATCH 1/5] ci: Run the Nix dev shell build in its own job 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. --- .github/workflows/nix.yml | 55 ++++++++++++++++++++++++++------------- docs/ci.md | 2 +- 2 files changed, 38 insertions(+), 19 deletions(-) diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml index 6a3ab3ecc..33a7b50f8 100644 --- a/.github/workflows/nix.yml +++ b/.github/workflows/nix.yml @@ -17,25 +17,54 @@ concurrency: cancel-in-progress: true jobs: + # Sandboxed builds: every derivation compiles inside Nix, which sees neither + # the sticky disk nor sccache, so Cachix is the only cache here. The dev + # shell job below rebuilds the same tree in the checkout and shares nothing + # with these derivations, which is why it runs on its own runner. nix-test: name: Nix Tests + runs-on: runs-on=${{ github.run_id }}-nix-test-${{ github.run_attempt }}/cpu=16/family=r7i+r8i+r7a+r8a/image=ubuntu26-full-x64/volume=100gb/extras=s3-cache + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - uses: cachix/install-nix-action@13d8dd58da0234aa297dedd986986ccb8e7f3e24 # v31.11.1 + with: + nix_path: nixpkgs=channel:nixos-unstable + github_access_token: ${{ github.token }} + - uses: cachix/cachix-action@38b082610b782e7e93e209c35fd730d399dee866 # v17 + with: + name: argumentcomputer + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + # Covers `builtins.fetchGit` of the Lake manifest's `git+https` + # dependencies, which runs at flake eval time as this user; + # `install-nix-action`'s github_access_token covers only `github:` + # flake inputs, which fetch via the API. + - uses: $/.github/actions/authenticate-github-fetches + # Ix CLI + - run: nix build --print-build-logs --accept-flake-config + - run: nix run .#ix -- --help + # A single invocation lets Nix schedule independent checks concurrently. + - run: nix flake check --print-build-logs --accept-flake-config + + # Builds and tests with the real `lake` and `cargo` inside the development + # environment, as a contributor would. + nix-devshell: + name: Nix devShell Tests env: # The dev shell builds with cargo directly, where `.cargo/config.toml` # would select native code generation; the sticky cache is shared # across instance families, so pin the same baseline CI uses. RUSTFLAGS: -Ctarget-cpu=x86-64-v4 -Ctarget-feature=+avx512vbmi2,+gfni - # Sticky disks retain Lake/Cargo files; /nix uses the larger root volume - # and Cachix provides its binary cache. + # Sticky disks retain Lake/Cargo files; /nix uses the root volume and only + # holds the dev shell closure, which Cachix provides. # https://runs-on.com/docs/runners/capabilities/sticky-disks/ - runs-on: runs-on=${{ github.run_id }}-nix-test-${{ github.run_attempt }}/cpu=16/family=r7i+r8i+r7a+r8a/image=ubuntu26-full-x64/volume=150gb/sticky=nix-x86-64-v4:100gb/extras=s3-cache + runs-on: runs-on=${{ github.run_id }}-nix-devshell-${{ github.run_attempt }}/cpu=16/family=r7i+r8i+r7a+r8a/image=ubuntu26-full-x64/volume=100gb/sticky=nix-x86-64-v4:100gb/extras=s3-cache steps: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false - # sccache serves only the `nix develop` build below: `nix build` and - # `nix flake check` compile inside Nix's sandbox, which sees neither - # the wrapper nor the network, and rely on Cachix instead. The dev - # shell inherits RUSTC_WRAPPER and keeps the outer PATH, so the + # The dev shell inherits RUSTC_WRAPPER and keeps the outer PATH, so the # binary the sccache action installs resolves there (see ci.yml). - uses: runs-on/action@dfae4d98c5537a0dc7bbb7e6b9211f30ba240f6d # v2.4.0 with: @@ -52,22 +81,12 @@ jobs: with: name: argumentcomputer authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - # Covers `builtins.fetchGit` of the Lake manifest's `git+https` - # dependencies, which runs at flake eval time as this user; - # `install-nix-action`'s github_access_token covers only `github:` - # flake inputs, which fetch via the API. - uses: $/.github/actions/authenticate-github-fetches - # Ix CLI - - run: nix build --print-build-logs --accept-flake-config - - run: nix run .#ix -- --help - # A single invocation lets Nix schedule independent checks concurrently. - - run: nix flake check --print-build-logs --accept-flake-config - # Run the real build and test commands inside the development environment. - run: nix develop --accept-flake-config --command bash -c "lake build && lake test" nix-gate: if: ${{ always() }} - needs: [nix-test] + needs: [nix-test, nix-devshell] permissions: actions: read checks: read diff --git a/docs/ci.md b/docs/ci.md index fbf7a4068..5228d3d08 100644 --- a/docs/ci.md +++ b/docs/ci.md @@ -23,7 +23,7 @@ from claiming another job's matching runner. Matrix jobs use Every RunsOn label uses the `ubuntu26-full-x64` image and sets `volume=` explicitly so the root volume has room for toolchains, apt packages, and container images; sticky disks hold only the declared cache paths. Jobs use -`volume=100gb`, and the Nix job `volume=150gb`. +`volume=100gb`. Sticky disks restore with provisioned snapshot initialization; `lazy-init` makes first reads of cached binaries and oleans slow enough to dominate jobs that only run them. From 02ceab7ae4b907079c0ac7e412ae1f4dcbff3790 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 1 Oct 2026 22:23:28 -0400 Subject: [PATCH 2/5] nix: Build every Rust package with the deps-only feature set 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. --- flake.nix | 57 +++++++++++++++++++++++-------------------------------- 1 file changed, 24 insertions(+), 33 deletions(-) diff --git a/flake.nix b/flake.nix index 1a7014c4d..bcb7a88d6 100644 --- a/flake.nix +++ b/flake.nix @@ -157,46 +157,43 @@ }; # Build dependencies once with every host feature enabled so the # `net` stack (tokio/iroh) is compiled and cached here, then shared - # by the package builds and clippy. CUDA remains opt-in and is - # compiled separately in CI with the CUDA toolkit available. + # by the package builds, clippy, and nextest. CUDA remains opt-in + # and is compiled separately in CI with the CUDA toolkit available. cargoArtifacts = craneLib.buildDepsOnly ( craneArgs // { cargoExtraArgs = "--locked --features parallel,test-ffi,net"; } ); + # Every build below enables the same features as `cargoArtifacts`, + # except that `test-ffi` is left to the test library. Cargo unifies + # features across the whole graph, so dropping `net` would change + # the feature sets of serde, libc, and other base crates and make + # cargo recompile them and everything above them, discarding the + # prebuilt artifacts. `test-ffi` declares no dependencies, so + # toggling it leaves the dependency graph untouched. The lakefile's + # `ix_rs_net` target skips `net` on macOS, mirrored here. + hostFeatures = "parallel" + pkgs.lib.optionalString (!pkgs.stdenv.isDarwin) ",net"; - # Test build: parallel + test-ffi (only used by ixTest). + # Static library for the Lean library and every executable but the + # test binary; `net` carries the `ix serve` / `ix connect` iroh stack. # doCheck = false: the `nextest` check is the single place cargo # tests run, so package builds only compile. - rustPkgTest = craneLib.buildPackage ( - craneArgs - // { - inherit cargoArtifacts; - cargoExtraArgs = "--locked --features parallel,test-ffi"; - doCheck = false; - } - ); - - # Release build without test-ffi (for distribution) - rustPkgRelease = craneLib.buildPackage ( + rustPkg = craneLib.buildPackage ( craneArgs // { inherit cargoArtifacts; - cargoExtraArgs = "--locked --features parallel"; + cargoExtraArgs = "--locked --features ${hostFeatures}"; doCheck = false; } ); - # Net build for the `ix` CLI (`ix serve` / `ix connect` iroh stack), - # mirroring the lakefile's `ix_rs_net` target, which skips `net` on - # macOS. - rustPkgNet = craneLib.buildPackage ( + # Test build adds the test-only FFI symbols (only used by ixTest). + rustPkgTest = craneLib.buildPackage ( craneArgs // { inherit cargoArtifacts; - cargoExtraArgs = - "--locked --features parallel" + pkgs.lib.optionalString (!pkgs.stdenv.isDarwin) ",net"; + cargoExtraArgs = "--locked --features ${hostFeatures},test-ffi"; doCheck = false; } ); @@ -261,10 +258,7 @@ ]; }; - # Release build args (no test-ffi symbols) - lakeBuildArgs = mkLakeBuildArgs rustPkgRelease; - # CLI build args (net symbols for `ix serve` / `ix connect`) - lakeNetBuildArgs = mkLakeBuildArgs rustPkgNet; + lakeBuildArgs = mkLakeBuildArgs rustPkg; # Test build args (includes test-ffi symbols) lakeTestBuildArgs = mkLakeBuildArgs rustPkgTest; @@ -294,19 +288,16 @@ --set LEAN_PATH "${drv}/.lake/build/lib/lean:${leanPath}" done ''; - # The CLI links rustPkgNet (lakefile: `ix` uses `ix_rs_net`), reusing - # ixLib's oleans. + # The CLI reuses ixLib's oleans and links the same static library. ixCLI = wrapBin ( lake2nix.mkPackage ( - lakeNetBuildArgs + lakeBinArgs // { - lakeArtifacts = ixLib; - installArtifacts = true; name = "ix"; } ) ); - # Test binary links rustPkg (with test-ffi) instead of rustPkgRelease + # Test binary links rustPkgTest (with test-ffi) instead of rustPkg ixTest = wrapBin ( lake2nix.mkPackage ( lakeTestBuildArgs @@ -338,7 +329,7 @@ craneArgs // { inherit cargoArtifacts; - cargoExtraArgs = "--locked --workspace"; + cargoExtraArgs = "--locked --workspace --features ${hostFeatures},test-ffi"; cargoNextestExtraArgs = "--profile ci --run-ignored only"; } ); @@ -362,7 +353,7 @@ craneArgs // { inherit cargoArtifacts; - cargoExtraArgs = "--locked --workspace"; + cargoExtraArgs = "--locked --workspace --features ${hostFeatures},test-ffi"; cargoNextestExtraArgs = "--profile ci"; } ); From 6b2a0bf047bc4ac1918e6832f07520f5a5c0f00e Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Fri, 2 Oct 2026 08:04:03 -0400 Subject: [PATCH 3/5] nix: Install only binaries and oleans from executable packages 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. --- flake.nix | 29 +++++++++++++++++++++++------ 1 file changed, 23 insertions(+), 6 deletions(-) diff --git a/flake.nix b/flake.nix index bcb7a88d6..f7fdec357 100644 --- a/flake.nix +++ b/flake.nix @@ -269,11 +269,30 @@ buildLibrary = true; } ); - lakeBinArgs = lakeBuildArgs // { + # Executables continue from ixLib's artifacts and install only the + # binaries plus the module files the wrapper puts on LEAN_PATH, which + # binaries that import Ix.Meta read at runtime. The rest of Lake's + # tree (static libraries, C output, IR, traces) only serves a build + # that continues from these artifacts, and nothing continues from an + # executable; it would multiply the output size several times over + # and put every file through the ELF fixup. + exeArtifacts = { lakeArtifacts = ixLib; - # Binaries that import Ix.Meta need .olean files at runtime via LEAN_PATH - installArtifacts = true; + installArtifacts = false; + postInstall = '' + mkdir -p $out/.lake/build/lib/lean + rsync -a --prune-empty-dirs \ + --include='*/' \ + --include='*.olean' \ + --include='*.olean.private' \ + --include='*.olean.server' \ + --exclude='*' \ + .lake/build/lib/lean/ $out/.lake/build/lib/lean/ + find .lake/build/bin -maxdepth 1 -type f -executable \ + -exec install -Dm755 -t $out/bin {} + + ''; }; + lakeBinArgs = lakeBuildArgs // exeArtifacts; leanPath = pkgs.lib.concatStringsSep ":" ( map (d: "${d}/.lake/build/lib/lean") ([ ixLib ] ++ builtins.attrValues lakeDeps) ); @@ -301,10 +320,9 @@ ixTest = wrapBin ( lake2nix.mkPackage ( lakeTestBuildArgs + // exeArtifacts // { - lakeArtifacts = ixLib; name = "IxTests"; - installArtifacts = true; } ) ); @@ -313,7 +331,6 @@ lakeBinArgs // { name = "Apps.ZKVoting.Prover"; - installArtifacts = true; } ) ); From 9b62a572bd55e468bfb1a606168defc18c403462 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Fri, 2 Oct 2026 09:10:56 -0400 Subject: [PATCH 4/5] nix: Use lean4-nix's binary install mode and archive the Ix library 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. --- flake.lock | 7 +++-- flake.nix | 92 ++++++++++++++++++++---------------------------------- 2 files changed, 37 insertions(+), 62 deletions(-) diff --git a/flake.lock b/flake.lock index e414a289c..4d0093d1f 100644 --- a/flake.lock +++ b/flake.lock @@ -198,15 +198,16 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1790785453, - "narHash": "sha256-d25LPK3rcJKXkUC2XfF9jN5SlUCIwyWDffidGDqxn38=", + "lastModified": 1790953530, + "narHash": "sha256-vlmLSs5QW5c1bVsz2XgTv00rfb7p3pRNFZ1562fpkuU=", "owner": "argumentcomputer", "repo": "lean4-nix", - "rev": "e828640c7710bb571eb052d02f1adb2ed5694c5e", + "rev": "cef08efca7aa9f1d4689e6ae65131484add15291", "type": "github" }, "original": { "owner": "argumentcomputer", + "ref": "install-modes", "repo": "lean4-nix", "type": "github" } diff --git a/flake.nix b/flake.nix index f7fdec357..c740bc4aa 100644 --- a/flake.nix +++ b/flake.nix @@ -19,7 +19,7 @@ cuda-nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable"; # Lean 4 & Lake - lean4-nix.url = "github:argumentcomputer/lean4-nix"; + lean4-nix.url = "github:argumentcomputer/lean4-nix/install-modes"; # Helper: flake-parts for easier outputs flake-parts.url = "github:hercules-ci/flake-parts"; @@ -267,72 +267,46 @@ // { name = "Ix"; buildLibrary = true; + # The executables below continue from this tree; archived, it + # is a single small file for Nix and Cachix to move around. + artifactsFormat = "zstd"; } ); - # Executables continue from ixLib's artifacts and install only the - # binaries plus the module files the wrapper puts on LEAN_PATH, which - # binaries that import Ix.Meta read at runtime. The rest of Lake's - # tree (static libraries, C output, IR, traces) only serves a build - # that continues from these artifacts, and nothing continues from an - # executable; it would multiply the output size several times over - # and put every file through the ELF fixup. - exeArtifacts = { + # Executables continue from ixLib's artifacts. lean4-nix installs + # them wrapped for standalone use, with the module files that + # binaries importing Ix.Meta read at runtime. The IR files are left + # out: every module these binaries can import is linked into them, + # so the interpreter never needs IR for it. + exeArgs = { lakeArtifacts = ixLib; - installArtifacts = false; - postInstall = '' - mkdir -p $out/.lake/build/lib/lean - rsync -a --prune-empty-dirs \ - --include='*/' \ - --include='*.olean' \ - --include='*.olean.private' \ - --include='*.olean.server' \ - --exclude='*' \ - .lake/build/lib/lean/ $out/.lake/build/lib/lean/ - find .lake/build/bin -maxdepth 1 -type f -executable \ - -exec install -Dm755 -t $out/bin {} + - ''; + installBin = true; + binFiles = [ + "*.olean" + "*.olean.private" + "*.olean.server" + ]; }; - lakeBinArgs = lakeBuildArgs // exeArtifacts; - leanPath = pkgs.lib.concatStringsSep ":" ( - map (d: "${d}/.lake/build/lib/lean") ([ ixLib ] ++ builtins.attrValues lakeDeps) - ); - wrapBin = - drv: - pkgs.runCommand drv.name { nativeBuildInputs = [ pkgs.makeWrapper ]; } '' - mkdir -p $out/bin - for f in ${drv}/bin/*; do - [ -x "$f" ] || continue - makeWrapper "$f" "$out/bin/$(basename "$f")" \ - --set LEAN_SYSROOT "${lean}" \ - --set LEAN_PATH "${drv}/.lake/build/lib/lean:${leanPath}" - done - ''; + lakeBinArgs = lakeBuildArgs // exeArgs; # The CLI reuses ixLib's oleans and links the same static library. - ixCLI = wrapBin ( - lake2nix.mkPackage ( - lakeBinArgs - // { - name = "ix"; - } - ) + ixCLI = lake2nix.mkPackage ( + lakeBinArgs + // { + name = "ix"; + } ); # Test binary links rustPkgTest (with test-ffi) instead of rustPkg - ixTest = wrapBin ( - lake2nix.mkPackage ( - lakeTestBuildArgs - // exeArtifacts - // { - name = "IxTests"; - } - ) + ixTest = lake2nix.mkPackage ( + lakeTestBuildArgs + // exeArgs + // { + name = "IxTests"; + } ); - ZKVotingProver = wrapBin ( - lake2nix.mkPackage ( - lakeBinArgs - // { - name = "Apps.ZKVoting.Prover"; - } - ) + ZKVotingProver = lake2nix.mkPackage ( + lakeBinArgs + // { + name = "Apps.ZKVoting.Prover"; + } ); in { From 245f0db084a8e9d9dbea9cf3add17d6c3053597a Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Fri, 2 Oct 2026 12:47:01 -0400 Subject: [PATCH 5/5] nix: Take lean4-nix's oleans-only binary install default 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. --- flake.lock | 6 +++--- flake.nix | 9 +-------- 2 files changed, 4 insertions(+), 11 deletions(-) diff --git a/flake.lock b/flake.lock index 4d0093d1f..99d8fbcc3 100644 --- a/flake.lock +++ b/flake.lock @@ -198,11 +198,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1790953530, - "narHash": "sha256-vlmLSs5QW5c1bVsz2XgTv00rfb7p3pRNFZ1562fpkuU=", + "lastModified": 1790958786, + "narHash": "sha256-7uPDQl+EmzmtXhrC7YbghNySsuPWQyCc++jqMrHz94w=", "owner": "argumentcomputer", "repo": "lean4-nix", - "rev": "cef08efca7aa9f1d4689e6ae65131484add15291", + "rev": "a85438f70bc005863dfac72074485169757f0745", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index c740bc4aa..9ea1a475c 100644 --- a/flake.nix +++ b/flake.nix @@ -274,17 +274,10 @@ ); # Executables continue from ixLib's artifacts. lean4-nix installs # them wrapped for standalone use, with the module files that - # binaries importing Ix.Meta read at runtime. The IR files are left - # out: every module these binaries can import is linked into them, - # so the interpreter never needs IR for it. + # binaries importing Ix.Meta read at runtime. exeArgs = { lakeArtifacts = ixLib; installBin = true; - binFiles = [ - "*.olean" - "*.olean.private" - "*.olean.server" - ]; }; lakeBinArgs = lakeBuildArgs // exeArgs; # The CLI reuses ixLib's oleans and links the same static library.