From 7409aab4abe50d2e8090fbe047903926b1c76583 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Tue, 29 Sep 2026 13:59:46 -0400 Subject: [PATCH 1/8] ci: run the CI jobs on pushes to main to warm the sticky disks RunsOn files a sticky-disk snapshot under the run's git ref and falls back to the default branch's snapshot for a ref that has none. Nothing ran these jobs on main, so the ci-lean-test and ci-rust-test lineages never had a main snapshot: every new PR branch and every merge-queue entry started from an empty disk and rebuilt about 1,300 Lean modules, ten minutes more than a warm run. A push run after each merge keeps a main snapshot at most one merge old. --- .github/workflows/ci.yml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d5ec71862..b2968b562 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -3,6 +3,12 @@ name: CI Jobs on: pull_request: merge_group: + # Pushes to main run the same jobs so their sticky disks get a `main` + # snapshot: RunsOn files each run's snapshot under its own ref, and a ref + # with none falls back to the default branch's. Without this run every + # new PR branch and every merge-queue entry starts from an empty disk. + push: + branches: [main] workflow_dispatch: permissions: From 5eceb2478ff82e4251cbfae46826eb0be27cbb2b Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Tue, 29 Sep 2026 13:59:47 -0400 Subject: [PATCH 2/8] merge-tests: share lean-test's sticky disk; dispatch !merge-tests on the PR branch The five matrix partitions used their own sticky lineage, which had no main snapshot either, so every merge-queue run was five cold builds. They now use ci.yml's lean-test lineage, which the push-to-main runs keep warm; the toolchain, codegen target and cached paths are the same. A comment event runs under the default branch's ref, so an issue_comment-triggered run would snapshot a PR's build as main's. The comment now only relays: a small job dispatches this workflow on the PR's head branch with the PR number as input, and the dispatched run does what the comment run did, under the branch's own ref. Fork branches and branches without the dispatch trigger get a comment explaining why nothing ran. --- .github/workflows/merge-tests.yml | 86 ++++++++++++++++++++++--------- 1 file changed, 63 insertions(+), 23 deletions(-) diff --git a/.github/workflows/merge-tests.yml b/.github/workflows/merge-tests.yml index 461fd8626..04db66ecc 100644 --- a/.github/workflows/merge-tests.yml +++ b/.github/workflows/merge-tests.yml @@ -2,10 +2,20 @@ name: Merge tests on: merge_group: + # `!merge-tests` on a PR: the relay job dispatches this workflow on the + # PR's branch, so the run carries the branch's ref. RunsOn files the + # sticky-disk snapshot under the run's ref, and a comment event's ref is + # the default branch; dispatching keeps a PR's build out of `main`'s + # cache while still reading from it. issue_comment: types: [created] + workflow_dispatch: + inputs: + pr: + description: PR number whose test merge commit to run + required: true -run-name: "${{ github.event_name == 'issue_comment' && format('Merge tests for PR #{0}', github.event.issue.number) || 'Merge tests' }}" +run-name: "${{ github.event_name == 'workflow_dispatch' && format('Merge tests for PR #{0}', inputs.pr) || (github.event_name == 'issue_comment' && 'Relay merge-tests comment' || 'Merge tests') }}" permissions: contents: read @@ -14,17 +24,44 @@ permissions: # cannot satisfy the required check, so runs are never superseded here. jobs: + relay: + name: Relay !merge-tests comment + if: >- + github.event_name == 'issue_comment' && + github.event.issue.pull_request && + github.event.issue.state == 'open' && + github.event.comment.user.type != 'Bot' && + contains(github.event.comment.body, '!merge-tests') && + (github.event.comment.author_association == 'MEMBER' || + github.event.comment.author_association == 'OWNER') + runs-on: ubuntu-latest + permissions: + actions: write + pull-requests: write + steps: + - name: Dispatch on the PR branch + env: + GH_TOKEN: ${{ github.token }} + PR_NUMBER: ${{ github.event.issue.number }} + run: | + [[ "$PR_NUMBER" =~ ^[1-9][0-9]*$ ]] \ + || { echo "::error::PR number must be a positive integer"; exit 1; } + read -r head_ref head_repo < <(gh api "repos/$GITHUB_REPOSITORY/pulls/$PR_NUMBER" \ + --jq '"\(.head.ref) \(.head.repo.full_name)"') + fail() { + printf '%s\n' "$1" > comment-body.md + gh pr comment "$PR_NUMBER" --body-file comment-body.md + echo "::error::$1" + exit 1 + } + [ "$head_repo" = "$GITHUB_REPOSITORY" ] \ + || fail "Merge tests run on branches of this repository only; \`$head_repo\` is a fork." + gh workflow run merge-tests.yml --ref "$head_ref" -f pr="$PR_NUMBER" 2> dispatch-error.txt \ + || fail "Could not dispatch merge tests on \`$head_ref\`: $(cat dispatch-error.txt). The branch needs this workflow's \`workflow_dispatch\` trigger; merge \`main\` into it and comment again." + prepare: name: Prepare merge tests - if: >- - github.event_name == 'merge_group' || - (github.event_name == 'issue_comment' && - github.event.issue.pull_request && - github.event.issue.state == 'open' && - github.event.comment.user.type != 'Bot' && - contains(github.event.comment.body, '!merge-tests') && - (github.event.comment.author_association == 'MEMBER' || - github.event.comment.author_association == 'OWNER')) + if: ${{ github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' }} runs-on: ubuntu-latest permissions: issues: write @@ -40,9 +77,9 @@ jobs: EVENT_NAME: ${{ github.event_name }} EVENT_SHA: ${{ github.sha }} GH_TOKEN: ${{ github.token }} - PR_NUMBER: ${{ github.event.issue.number }} + PR_NUMBER: ${{ inputs.pr }} run: | - if [ "$EVENT_NAME" = issue_comment ]; then + if [ "$EVENT_NAME" = workflow_dispatch ]; then [[ "$PR_NUMBER" =~ ^[1-9][0-9]*$ ]] \ || { echo "::error::PR number must be a positive integer"; exit 1; } revision=$(gh api "repos/$GITHUB_REPOSITORY/pulls/$PR_NUMBER" \ @@ -57,7 +94,7 @@ jobs: echo "revision=$revision" >> "$GITHUB_OUTPUT" - name: Compose initial comment - if: github.event_name == 'issue_comment' + if: github.event_name == 'workflow_dispatch' env: MERGE_SHA: ${{ steps.target.outputs.revision }} PR_NUMBER: ${{ steps.target.outputs.pr }} @@ -71,7 +108,7 @@ jobs: } > comment-body.md - name: Post initial comment - if: github.event_name == 'issue_comment' + if: github.event_name == 'workflow_dispatch' id: post uses: peter-evans/create-or-update-comment@v5 with: @@ -82,7 +119,7 @@ jobs: merge-tests: name: ${{ matrix.name }} needs: prepare - if: ${{ github.event_name == 'merge_group' || github.event_name == 'issue_comment' }} + if: ${{ github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' }} strategy: fail-fast: false matrix: @@ -117,7 +154,12 @@ jobs: # only after the whole attempt finishes, and the longest partitions # already run close to the merge queue's status-check timeout, so one # reclaim is enough to dequeue the PR. - runs-on: runs-on=${{ github.run_id }}-merge-tests-${{ github.run_attempt }}-${{ strategy.job-index }}/cpu=32/family=r7i+r8i+r7a+r8a/spot=false/image=ubuntu26-full-x64/volume=100gb/sticky=merge-tests-x86-64-v4:50gb/extras=s3-cache + # + # The sticky disk is ci.yml's lean-test lineage: same toolchain, same + # portable codegen, same cached paths, and that job's push-to-main runs + # are what keep the lineage's `main` snapshot fresh. A merge-queue ref + # has no snapshot of its own and falls back to that one. + runs-on: runs-on=${{ github.run_id }}-merge-tests-${{ github.run_attempt }}-${{ strategy.job-index }}/cpu=32/family=r7i+r8i+r7a+r8a/spot=false/image=ubuntu26-full-x64/volume=100gb/sticky=ci-lean-test-x86-64-v4:50gb/extras=s3-cache steps: - name: Validate merge-test variant env: @@ -130,7 +172,7 @@ jobs: - uses: actions/checkout@v7 with: - ref: ${{ github.event_name == 'issue_comment' && format('refs/pull/{0}/merge', needs.prepare.outputs.pr) || needs.prepare.outputs.revision }} + ref: ${{ github.event_name == 'workflow_dispatch' && format('refs/pull/{0}/merge', needs.prepare.outputs.pr) || needs.prepare.outputs.revision }} persist-credentials: false - name: Verify test revision @@ -174,7 +216,7 @@ jobs: valgrind: name: Valgrind FFI needs: prepare - if: ${{ github.event_name == 'merge_group' || github.event_name == 'issue_comment' }} + if: ${{ github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' }} # Valgrind cannot decode AVX-512, so this job builds generic artifacts and # keeps them in the S3-backed actions cache under their own key rather # than sharing a sticky disk with the x86-64-v4 partitions. @@ -182,7 +224,7 @@ jobs: steps: - uses: actions/checkout@v7 with: - ref: ${{ github.event_name == 'issue_comment' && format('refs/pull/{0}/merge', needs.prepare.outputs.pr) || needs.prepare.outputs.revision }} + ref: ${{ github.event_name == 'workflow_dispatch' && format('refs/pull/{0}/merge', needs.prepare.outputs.pr) || needs.prepare.outputs.revision }} persist-credentials: false - name: Verify test revision @@ -231,9 +273,7 @@ jobs: .lake/build/bin/IxTests ffi merge-gate: - if: >- - always() && - (github.event_name != 'issue_comment' || needs.prepare.result != 'skipped') + if: ${{ always() && github.event_name != 'issue_comment' }} needs: [prepare, merge-tests, valgrind] permissions: actions: read @@ -246,7 +286,7 @@ jobs: name: Report merge tests if: >- always() && - github.event_name == 'issue_comment' && + github.event_name == 'workflow_dispatch' && needs.prepare.result == 'success' needs: [prepare, merge-tests, valgrind, merge-gate] runs-on: ubuntu-latest From 4390b65c0d246c860decda6d692092879fafe081 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Tue, 29 Sep 2026 14:00:57 -0400 Subject: [PATCH 3/8] nix: run the Nix CI job on pushes to main to warm its sticky disk Same reasoning as ci.yml: the nix-x86-64-v4 lineage never had a main snapshot, so every new ref started from an empty disk. --- .github/workflows/nix.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml index a5e5df0c1..e7dd6da29 100644 --- a/.github/workflows/nix.yml +++ b/.github/workflows/nix.yml @@ -3,6 +3,10 @@ name: Nix CI on: pull_request: merge_group: + # Pushes to main keep the sticky disk's `main` snapshot fresh, which every + # new PR branch and merge-queue ref falls back to (see ci.yml). + push: + branches: [main] workflow_dispatch: permissions: From 23fb1358ce712ebcd48040ea457adaefb4116689 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Tue, 29 Sep 2026 14:15:07 -0400 Subject: [PATCH 4/8] ci: build only on pushes to main The push run exists to snapshot build products the merge queue already tested. lean-test keeps the all-targets build and IxTcVerify and skips the codegen check, the toolchain diff and the test tiers; rust-test keeps clippy and check and builds the test binaries without running them, skipping rustfmt and cargo-deny. cuda-compile is all build steps and its main-keyed cache entry is what a new branch's restore-keys prefix can see, so it runs unchanged. --- .github/workflows/ci.yml | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b2968b562..ad0ffd9f2 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -47,17 +47,24 @@ jobs: run: lake lint -- --wfail -v - name: Build Ix.Tc formal verification run: lake build IxTcVerify + # A push to main already passed these checks in the merge queue; that + # run only exists to snapshot the build products above. - name: Check codegen'd IxVM kernel is up to date + if: github.event_name != 'push' run: lake exe ix codegen --check - name: Check Lean versions match for Ix and compiler bench + if: github.event_name != 'push' run: diff lean-toolchain Benchmarks/Compile/lean-toolchain # The primary test tier runs over the targets the lint step just built, # so the tests add no compilation of their own. - name: Run primary tests + if: github.event_name != 'push' run: lake test --wfail - name: Test Ix CLI + if: github.event_name != 'push' run: lake test --wfail -- cli - name: Test Ixon v3 contracts and consumers + if: github.event_name != 'push' run: | lake exe ixon-v3-primitives lake exe ixon-v3-tests --primitives @@ -81,18 +88,24 @@ jobs: with: auto-config: false use-github-cache: false + # A push to main already passed the lints and tests in the merge + # queue; that run only builds, so the sticky disk holds the check, + # clippy and test-binary artifacts the next PR run will fingerprint. - name: Check Rustfmt code style + if: github.event_name != 'push' uses: actions-rust-lang/rustfmt@v1 - name: Check clippy warnings run: cargo clippy --release --workspace --all-targets --features ix-ffi/parallel,ix-ffi/net,ix-ffi/test-ffi -- -D warnings - name: Check *everything* compiles run: cargo check --release --workspace --all-targets --features ix-ffi/parallel,ix-ffi/net,ix-ffi/test-ffi - name: Tests - run: cargo nextest run --release --profile ci --workspace + run: cargo nextest run --release --profile ci --workspace ${{ github.event_name == 'push' && '--no-run' || '' }} - name: Get Rust version + if: github.event_name != 'push' run: | echo "RUST_VERSION=$(awk -F '"' '/^channel/ {print $2}' rust-toolchain.toml)" | tee -a $GITHUB_ENV - name: Cargo-deny + if: github.event_name != 'push' uses: EmbarkStudios/cargo-deny-action@v2 with: rust-version: ${{ env.RUST_VERSION }} From e98ff512c772793c349227da6cc629ca59f0b8d9 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Tue, 29 Sep 2026 14:28:19 -0400 Subject: [PATCH 5/8] ci: cache rustc outputs with sccache on the Rust jobs Cargo judges a workspace crate fresh by source mtimes, and a fresh checkout renews every mtime, so the restored target directory never spares the repo's own crates: a warm rust-test run still spent about five and a half minutes recompiling them, and lean-test rebuilds ix_rs for two minutes every run. sccache keys rustc outputs by content, so unchanged crates return as cache hits; linking and build scripts still run, so thin-LTO link time remains. cuda-compile is left out with a note on wiring both rustc and nvcc when the GPU benchmark lands after #644; the container's S3 credentials and multi-stark's single --lib nvcc call both need attention first. --- .github/workflows/ci.yml | 18 ++++++++++++++++++ .github/workflows/merge-tests.yml | 5 +++++ 2 files changed, 23 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ad0ffd9f2..f64bab6dd 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -26,11 +26,17 @@ jobs: runs-on: runs-on=${{ github.run_id }}-lean-test-${{ github.run_attempt }}/cpu=16/family=r7i+r8i+r7a+r8a/image=ubuntu26-full-x64/volume=100gb/sticky=ci-lean-test-x86-64-v4:50gb/extras=s3-cache steps: - uses: actions/checkout@v7 + # sccache keys rustc outputs by content, so the workspace crates, which + # cargo rebuilds after every fresh checkout because their mtimes moved, + # come back as cache hits. RunsOn configures it before anything can + # start an sccache server. - uses: runs-on/action@v2 with: + sccache: s3 sticky_cache: | rust custom,path=.lake,path=target + - uses: mozilla-actions/sccache-action@v0.0.11 - uses: ./.github/actions/setup-rust-toolchain with: codegen: portable @@ -73,11 +79,17 @@ jobs: runs-on: runs-on=${{ github.run_id }}-rust-test-${{ github.run_attempt }}/cpu=8/family=r7i+r8i+r7a+r8a/image=ubuntu26-full-x64/volume=100gb/sticky=ci-rust-test-x86-64-v4:50gb/extras=s3-cache steps: - uses: actions/checkout@v7 + # sccache keys rustc outputs by content, so the workspace crates, which + # cargo rebuilds after every fresh checkout because their mtimes moved, + # come back as cache hits. RunsOn configures it before anything can + # start an sccache server. - uses: runs-on/action@v2 with: + sccache: s3 sticky_cache: | rust custom,path=.lake,path=target + - uses: mozilla-actions/sccache-action@v0.0.11 - uses: ./.github/actions/setup-rust-toolchain with: codegen: portable @@ -123,6 +135,12 @@ jobs: # sufficient for this downstream integration gate. MULTI_STARK_CUDA_ARCHS: "80" steps: + # No sccache here yet. Once the GPU benchmark lands after #644, wire + # it for both compilers: `sccache: s3` plus the sccache action for + # rustc (this job runs in a container, so its S3 credentials via the + # instance role need checking first), and an `NVCC` wrapper running + # `sccache nvcc` for the kernels, which multi-stark's build script + # must compile with `-c` per source for sccache to cache them. - uses: runs-on/action@v2 - uses: actions/checkout@v7 - name: Install toolchain bootstrap dependencies diff --git a/.github/workflows/merge-tests.yml b/.github/workflows/merge-tests.yml index 04db66ecc..9f06ebe3d 100644 --- a/.github/workflows/merge-tests.yml +++ b/.github/workflows/merge-tests.yml @@ -185,11 +185,16 @@ jobs: exit 1 fi + # sccache keys rustc outputs by content, so the workspace crates, which + # cargo rebuilds after every fresh checkout because their mtimes moved, + # come back as cache hits (see ci.yml). - uses: runs-on/action@v2 with: + sccache: s3 sticky_cache: | rust custom,path=.lake,path=target + - uses: mozilla-actions/sccache-action@v0.0.11 - uses: ./.github/actions/setup-rust-toolchain with: codegen: portable From b161266db96c13292365b7cf979748196de68052 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Tue, 29 Sep 2026 14:30:56 -0400 Subject: [PATCH 6/8] nix: cache rustc outputs with sccache in the dev-shell build Only the `nix develop` step can use it: the sandboxed `nix build` and `nix flake check` see neither the wrapper nor the network and stay on Cachix. The dev shell inherits RUSTC_WRAPPER and keeps the outer PATH, so nothing in the flake changes. --- .github/workflows/nix.yml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml index e7dd6da29..d92f37d72 100644 --- a/.github/workflows/nix.yml +++ b/.github/workflows/nix.yml @@ -30,11 +30,18 @@ jobs: 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 steps: - uses: actions/checkout@v7 + # 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 + # binary the sccache action installs resolves there (see ci.yml). - uses: runs-on/action@v2 with: + sccache: s3 sticky_cache: | rust custom,path=.lake,path=target + - uses: mozilla-actions/sccache-action@v0.0.11 - uses: cachix/install-nix-action@v31 with: nix_path: nixpkgs=channel:nixos-unstable From 7cca29dbeebd6697caa13c9887644067dd26f97b Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Tue, 29 Sep 2026 15:10:13 -0400 Subject: [PATCH 7/8] bench: sticky disks and sccache for the benchmark builds; dispatch !benchmark on the PR branch The build jobs of bench-main and bench-pr share one native-r8i sticky lineage in place of the tarballed Lake cache and rust-cache: bench-main's push-to-main run leaves the lineage's main snapshot, and a !benchmark run, dispatched on its PR branch, restores that snapshot and writes its own to the branch. Each compile env gets its own lineage holding the compile workspace's .lake, since concurrent jobs on one lineage keep only the last clean completion; the FLT package cache and its matrix key go with it. sccache covers the workspace-crate rebuilds in both build jobs and in bench-pr's from-scratch base builds. The relay dispatched on the default branch, which made every !benchmark run a main job to RunsOn; it now dispatches on the PR's head branch and refuses forks with a comment, since a fork branch cannot be dispatched and would otherwise snapshot into main's lineage. --- .github/workflows/bench-main.yml | 45 ++++++++++++++++------------ .github/workflows/bench-pr.yml | 51 ++++++++++++++++++++++++++------ 2 files changed, 68 insertions(+), 28 deletions(-) diff --git a/.github/workflows/bench-main.yml b/.github/workflows/bench-main.yml index ff66ce452..8366cb406 100644 --- a/.github/workflows/bench-main.yml +++ b/.github/workflows/bench-main.yml @@ -46,25 +46,29 @@ jobs: # with native code generation for r8i, with caches and measured results # isolated from other hardware and compiler flags. build: - runs-on: runs-on=${{ github.run_id }}-build-${{ github.run_attempt }}/cpu=32/family=r8i.8xlarge/spot=false/image=ubuntu26-full-x64/volume=100gb/extras=s3-cache + # The sticky disk is the native-r8i lineage bench-pr's build job shares: + # this push run leaves the lineage's `main` snapshot, which a + # `!benchmark` run dispatched on its PR branch reads without writing. + runs-on: runs-on=${{ github.run_id }}-build-${{ github.run_attempt }}/cpu=32/family=r8i.8xlarge/spot=false/image=ubuntu26-full-x64/volume=100gb/sticky=bench-build-r8i-native:50gb/extras=s3-cache steps: - - uses: runs-on/action@v2 - uses: actions/checkout@v7 - - name: Mount Lake build cache - uses: actions/cache@v6 + # Lake and cargo artifacts live on the sticky disk; sccache serves the + # workspace crates cargo rebuilds after every fresh checkout (see + # ci.yml), under entries the native codegen flags keep apart from CI's. + - uses: runs-on/action@v2 with: - path: .lake - key: ${{ env.BENCH_CACHE }}-lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} - restore-keys: ${{ env.BENCH_CACHE }}-lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}- + sccache: s3 + sticky_cache: | + rust + custom,path=.lake,path=target + - uses: mozilla-actions/sccache-action@v0.0.11 - name: Log build CPU uses: ./.github/actions/log-cpu with: label: Benchmark binary build CPU - # Rust toolchain + cargo cache, so the cargo step inside `lake build` - # does not recompile the Plonky3/multi-stark dependencies every run. - uses: ./.github/actions/setup-rust-toolchain with: - cache-key: ${{ env.BENCH_CACHE }} + use-github-cache: "false" - uses: leanprover/lean-action@v1 with: auto-config: false @@ -126,7 +130,10 @@ jobs: # job title. name: compile-${{ matrix.env }} needs: build - runs-on: runs-on=${{ github.run_id }}-compile-${{ github.run_attempt }}-${{ strategy.job-index }}/cpu=32/family=r8i.8xlarge/spot=false/image=ubuntu26-full-x64/volume=100gb/extras=s3-cache + # One sticky lineage per env: concurrent jobs on one lineage keep only + # the last clean completion, so a shared disk would drop every other + # env's Lake packages and oleans each run. + runs-on: runs-on=${{ github.run_id }}-compile-${{ github.run_attempt }}-${{ strategy.job-index }}/cpu=32/family=r8i.8xlarge/spot=false/image=ubuntu26-full-x64/volume=100gb/sticky=bench-compile-${{ matrix.env }}-r8i-native:100gb/extras=s3-cache permissions: contents: read checks: write @@ -148,10 +155,16 @@ jobs: # shared Compile package; no mathlib cache needed. - { env: ISLB } - { env: Mathlib, mathlib: true } - - { env: FLT, cache_pkg: flt, mathlib: true } + - { env: FLT, mathlib: true } steps: - - uses: runs-on/action@v2 - uses: actions/checkout@v7 + # The compile workspace's `.lake` persists on the sticky disk: its + # Lake packages, the Mathlib oleans `cache get` fetched, and the env's + # own build, so later runs replay instead of refetching and rebuilding. + - uses: runs-on/action@v2 + with: + sticky_cache: | + custom,path=${{ env.COMPILE_DIR }}/.lake # `lake build` below clones this package's Lake dependencies. - uses: ./.github/actions/authenticate-github-fetches - uses: actions/cache/restore@v6 @@ -174,12 +187,6 @@ jobs: auto-config: false use-github-cache: false use-mathlib-cache: ${{ matrix.mathlib && 'true' || 'false' }} - # FLT takes a few minutes to rebuild, so cache its build artifacts. - - if: matrix.cache_pkg - uses: actions/cache@v6 - with: - path: ${{ env.COMPILE_DIR }}/.lake/packages/${{ matrix.cache_pkg }}/.lake/build - key: ${{ env.BENCH_CACHE }}-${{ matrix.cache_pkg }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', env.COMPILE_DIR)) }}-${{ hashFiles(format('{0}/lake-manifest.json', env.COMPILE_DIR)) }} - run: lake build Compile${{ matrix.env }} working-directory: ${{ env.COMPILE_DIR }} # The measured compile: serializes the env to `.ixe` at the diff --git a/.github/workflows/bench-pr.yml b/.github/workflows/bench-pr.yml index 55e4b4c25..76fdb5faa 100644 --- a/.github/workflows/bench-pr.yml +++ b/.github/workflows/bench-pr.yml @@ -114,21 +114,32 @@ jobs: runs-on: ubuntu-latest permissions: actions: write - pull-requests: read + pull-requests: write steps: # issue_comment doesn't carry the PR's base/head; this action looks # them up. - uses: xt0rted/pull-request-comment-branch@v3 id: comment-branch - - name: Dispatch the trusted run + # Dispatched on the PR's branch, not the default branch: RunsOn files + # each run's sticky-disk snapshot under its ref, so the build lands on + # the branch and only reads `main`'s (bench-main's) snapshot. A fork + # branch cannot be dispatched, and would write `main`'s otherwise. + - name: Dispatch on the PR branch env: GH_TOKEN: ${{ github.token }} COMMENT_BODY: ${{ github.event.comment.body }} PR_NUMBER: ${{ github.event.issue.number }} + HEAD_REF: ${{ steps.comment-branch.outputs.head_ref }} run: | + head_repo=$(gh api "repos/$GITHUB_REPOSITORY/pulls/$PR_NUMBER" --jq '.head.repo.full_name') + if [ "$head_repo" != "$GITHUB_REPOSITORY" ]; then + printf '%s\n' "Benchmarks run on branches of this repository only; \`$head_repo\` is a fork." > comment-body.md + gh pr comment "$PR_NUMBER" --body-file comment-body.md + exit 1 + fi gh workflow run bench-pr.yml \ --repo "$GITHUB_REPOSITORY" \ - --ref "${{ github.event.repository.default_branch }}" \ + --ref "$HEAD_REF" \ -f pr="$PR_NUMBER" \ -f base-sha="${{ steps.comment-branch.outputs.base_sha }}" \ -f base-ref="${{ steps.comment-branch.outputs.base_ref }}" \ @@ -147,7 +158,10 @@ jobs: # available. build: if: github.event_name == 'workflow_dispatch' - runs-on: runs-on=${{ github.run_id }}-build-${{ github.run_attempt }}/cpu=32/family=r8i.8xlarge/spot=false/image=ubuntu26-full-x64/volume=100gb/extras=s3-cache + # bench-main's build lineage: its push-to-main runs leave the `main` + # snapshot this run falls back to; this run's own snapshot goes to + # the PR branch the relay dispatched on. + runs-on: runs-on=${{ github.run_id }}-build-${{ github.run_attempt }}/cpu=32/family=r8i.8xlarge/spot=false/image=ubuntu26-full-x64/volume=100gb/sticky=bench-build-r8i-native:50gb/extras=s3-cache outputs: revision: ${{ steps.target.outputs.revision }} matrix: ${{ steps.parse.outputs.matrix }} @@ -159,7 +173,6 @@ jobs: # rejected; the failure comment quotes it. parse-error: ${{ steps.parse.outputs.parse-error }} steps: - - uses: runs-on/action@v2 # Comment dispatch requires an org MEMBER/OWNER; manual dispatch requires # repo write access. Emit the validated full SHA once for every checkout. - name: Validate SHAs @@ -176,6 +189,16 @@ jobs: ref: ${{ steps.target.outputs.revision }} # The job builds and runs PR code; never leave the token in .git. persist-credentials: false + # Lake and cargo artifacts live on the sticky disk; sccache serves the + # workspace crates cargo rebuilds after every fresh checkout (see + # ci.yml), under entries the native codegen flags keep apart from CI's. + - uses: runs-on/action@v2 + with: + sccache: s3 + sticky_cache: | + rust + custom,path=.lake,path=target + - uses: mozilla-actions/sccache-action@v0.0.11 - id: bins uses: actions/cache/restore@v6 with: @@ -186,7 +209,7 @@ jobs: - if: steps.bins.outputs.cache-hit != 'true' uses: ./.github/actions/setup-rust-toolchain with: - cache-key: ${{ env.BENCH_CACHE }} + use-github-cache: "false" # A persistent hit still needs the matching toolchain for libleanshared. - uses: leanprover/lean-action@v1 with: @@ -212,7 +235,7 @@ jobs: - if: steps.parse.outputs.fresh == '1' && steps.bins.outputs.cache-hit == 'true' uses: ./.github/actions/setup-rust-toolchain with: - cache-key: ${{ env.BENCH_CACHE }} + use-github-cache: "false" - name: Log build CPU uses: ./.github/actions/log-cpu with: @@ -310,20 +333,25 @@ jobs: name: compile-${{ matrix.env }} needs: build if: needs.build.outputs.envs != '[]' - runs-on: runs-on=${{ github.run_id }}-compile-${{ github.run_attempt }}-${{ strategy.job-index }}/cpu=32/family=r8i.8xlarge/spot=false/image=ubuntu26-full-x64/volume=100gb/extras=s3-cache + # bench-main's per-env compile lineage (see there): this run reads the + # env's `main` snapshot and leaves its own on the PR branch. + runs-on: runs-on=${{ github.run_id }}-compile-${{ github.run_attempt }}-${{ strategy.job-index }}/cpu=32/family=r8i.8xlarge/spot=false/image=ubuntu26-full-x64/volume=100gb/sticky=bench-compile-${{ matrix.env }}-r8i-native:100gb/extras=s3-cache timeout-minutes: 60 strategy: fail-fast: false matrix: env: ${{ fromJSON(needs.build.outputs.envs) }} steps: - - uses: runs-on/action@v2 - name: Checkout PR uses: actions/checkout@v7 with: ref: ${{ needs.build.outputs.revision }} # The job runs PR code; never leave the token in .git. persist-credentials: false + - uses: runs-on/action@v2 + with: + sticky_cache: | + custom,path=Benchmarks/Compile/.lake # `lake build` below clones this package's Lake dependencies. - uses: ./.github/actions/authenticate-github-fetches # Apply the allowlisted KEY=VALUE lines from the !benchmark comment, @@ -469,7 +497,12 @@ jobs: HEAD_SHA: ${{ needs.build.outputs.revision }} FRESH: ${{ needs.build.outputs.fresh }} steps: + # sccache for the from-scratch base build below: its workspace crates + # are what the base's own bench-main run compiled (see ci.yml). - uses: runs-on/action@v2 + with: + sccache: s3 + - uses: mozilla-actions/sccache-action@v0.0.11 # The PR is checked out at the workspace root (the local composite # actions resolve from there); the base checkout, when needed, goes # under base/. From e997138ae233a8f432df0790fe6af678e5a57514 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Tue, 29 Sep 2026 15:14:11 -0400 Subject: [PATCH 8/8] ci: clear RUSTC_WRAPPER for the cargo-deny container cargo-deny-action runs in Docker and inherits the job's RUSTC_WRAPPER=sccache, but the container has no sccache, so cargo failed on `sccache rustc -vV` before deny could fetch the crate graph. Deny never compiles; an empty wrapper is one cargo ignores. --- .github/workflows/ci.yml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f64bab6dd..3f8ceefd2 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -116,9 +116,14 @@ jobs: if: github.event_name != 'push' run: | echo "RUST_VERSION=$(awk -F '"' '/^channel/ {print $2}' rust-toolchain.toml)" | tee -a $GITHUB_ENV + # A Docker action: the job's RUSTC_WRAPPER reaches its container, where + # sccache is not installed, and cargo fails before deny runs. Deny only + # reads metadata, and cargo treats an empty wrapper as none. - name: Cargo-deny if: github.event_name != 'push' uses: EmbarkStudios/cargo-deny-action@v2 + env: + RUSTC_WRAPPER: "" with: rust-version: ${{ env.RUST_VERSION }}