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. diff --git a/flake.lock b/flake.lock index e414a289c..99d8fbcc3 100644 --- a/flake.lock +++ b/flake.lock @@ -198,15 +198,16 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1790785453, - "narHash": "sha256-d25LPK3rcJKXkUC2XfF9jN5SlUCIwyWDffidGDqxn38=", + "lastModified": 1790958786, + "narHash": "sha256-7uPDQl+EmzmtXhrC7YbghNySsuPWQyCc++jqMrHz94w=", "owner": "argumentcomputer", "repo": "lean4-nix", - "rev": "e828640c7710bb571eb052d02f1adb2ed5694c5e", + "rev": "a85438f70bc005863dfac72074485169757f0745", "type": "github" }, "original": { "owner": "argumentcomputer", + "ref": "install-modes", "repo": "lean4-nix", "type": "github" } diff --git a/flake.nix b/flake.nix index 1a7014c4d..9ea1a475c 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"; @@ -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"; } );