fix: Improve Nix build & CI time

.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

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.

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";
@@ -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;
 
@@ -273,58 +267,39 @@
             // {
               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";
             }
           );
-          lakeBinArgs = lakeBuildArgs // {
+          # 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.
+          exeArgs = {
             lakeArtifacts = ixLib;
-            # Binaries that import Ix.Meta need .olean files at runtime via LEAN_PATH
-            installArtifacts = true;
+            installBin = true;
           };
-          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
-            '';
-          # The CLI links rustPkgNet (lakefile: `ix` uses `ix_rs_net`), reusing
-          # ixLib's oleans.
-          ixCLI = wrapBin (
-            lake2nix.mkPackage (
-              lakeNetBuildArgs
-              // {
-                lakeArtifacts = ixLib;
-                installArtifacts = true;
-                name = "ix";
-              }
-            )
+          lakeBinArgs = lakeBuildArgs // exeArgs;
+          # The CLI reuses ixLib's oleans and links the same static library.
+          ixCLI = lake2nix.mkPackage (
+            lakeBinArgs
+            // {
+              name = "ix";
+            }
           );
-          # Test binary links rustPkg (with test-ffi) instead of rustPkgRelease
-          ixTest = wrapBin (
-            lake2nix.mkPackage (
-              lakeTestBuildArgs
-              // {
-                lakeArtifacts = ixLib;
-                name = "IxTests";
-                installArtifacts = true;
-              }
-            )
+          # Test binary links rustPkgTest (with test-ffi) instead of rustPkg
+          ixTest = lake2nix.mkPackage (
+            lakeTestBuildArgs
+            // exeArgs
+            // {
+              name = "IxTests";
+            }
           );
-          ZKVotingProver = wrapBin (
-            lake2nix.mkPackage (
-              lakeBinArgs
-              // {
-                name = "Apps.ZKVoting.Prover";
-                installArtifacts = true;
-              }
-            )
+          ZKVotingProver = lake2nix.mkPackage (
+            lakeBinArgs
+            // {
+              name = "Apps.ZKVoting.Prover";
+            }
           );
         in
         {
@@ -338,7 +313,7 @@
               craneArgs
               // {
                 inherit cargoArtifacts;
-                cargoExtraArgs = "--locked --workspace";
+                cargoExtraArgs = "--locked --workspace --features ${hostFeatures},test-ffi";
                 cargoNextestExtraArgs = "--profile ci --run-ignored only";
               }
             );
@@ -362,7 +337,7 @@
               craneArgs
               // {
                 inherit cargoArtifacts;
-                cargoExtraArgs = "--locked --workspace";
+                cargoExtraArgs = "--locked --workspace --features ${hostFeatures},test-ffi";
                 cargoNextestExtraArgs = "--profile ci";
               }
             );