From a3bf0d20ed747a88e6b6fa1eda4587fb2b64a91f Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 3 Sep 2026 22:26:54 -0400 Subject: [PATCH 1/9] ci: add on-demand merge tests and shared runner caches --- .github/actions/install-zisk/action.yml | 6 +- .github/actions/log-cpu/action.yml | 154 +++------- .github/actions/setup-lake-cache/action.yml | 32 +++ .../actions/setup-rust-toolchain/action.yml | 41 +-- .github/workflows/bench-main.yml | 107 ++----- .github/workflows/bench-pr.yml | 175 ++++------- .github/workflows/bencher-plots.yml | 2 +- .github/workflows/ci.yml | 134 ++++++--- .github/workflows/codeql.yml | 5 +- .github/workflows/merge-tests.yml | 271 ++++++++++++------ .github/workflows/nix.yml | 29 +- .github/workflows/update.yml | 12 +- Ix/Cli/BenchCmd.lean | 3 +- Ix/Cli/BenchReport.lean | 18 +- Ix/Tc/Verify/Audit/Basic.lean | 63 ++-- Tests/Ix/Tc/Roundtrip.lean | 149 ++++------ docs/benchmarking.md | 47 ++- 17 files changed, 600 insertions(+), 648 deletions(-) create mode 100644 .github/actions/setup-lake-cache/action.yml diff --git a/.github/actions/install-zisk/action.yml b/.github/actions/install-zisk/action.yml index 857fcb356..40ef7b4be 100644 --- a/.github/actions/install-zisk/action.yml +++ b/.github/actions/install-zisk/action.yml @@ -117,9 +117,9 @@ runs: # reuse a stale key. `aws s3 cp` (multipart, no creds — public bucket) # holds throughput steady where a single-stream `curl` swings by an # order of magnitude; `curl` is the fallback for hosts without the AWS - # CLI. Deliberately NOT actions/cache'd: the runner fleet is AWS-hosted, - # so multipart S3 outruns the Actions cache service — and the tarball - # would crowd the repo's cache quota besides. + # CLI. Deliberately NOT actions/cache'd: the multi-GB tarball would crowd + # the repo's cache quota, while its public S3 source supports multipart + # downloads directly. - name: Fetch proving key from S3, extract, regenerate const-trees if: inputs.proving-key == 'true' shell: bash diff --git a/.github/actions/log-cpu/action.yml b/.github/actions/log-cpu/action.yml index b47cea486..ada8c9f16 100644 --- a/.github/actions/log-cpu/action.yml +++ b/.github/actions/log-cpu/action.yml @@ -1,140 +1,52 @@ name: Log CPU information -description: >- - Log a benchmark host's CPU and effective cgroup allocation, optionally - recording the report, printing native-binary build provenance, and warning - when the build and measurement CPUs differ. +description: Log the current host's CPU and effective cgroup allocation inputs: label: - description: Heading and context stored in a newly recorded CPU report + description: Heading and context for the CPU report required: false default: CPU information - output-file: - description: Optional path at which to record the current host report - required: false - provenance-file: - description: Optional native-binary build-host report to print - required: false - provenance-label: - description: Subject named in provenance mismatch warnings - required: false - default: Native benchmark binaries - warning-file: - description: Optional Markdown file to which provenance warnings are appended - required: false - log-current: - description: Whether to log the current host - required: false - default: "true" + +outputs: + summary: + description: CPU model, effective vCPU count, and total RAM + value: ${{ steps.report.outputs.summary }} runs: using: composite steps: - # PR benchmarks execute trusted workflow YAML from the default branch but - # load this action from the PR checkout. Ensure a freshly checked-out base - # has its pinned Rust toolchain before Lake invokes Cargo. - - name: Bootstrap base Rust toolchain - if: inputs.label == 'Base benchmark binary build CPU' + - id: report shell: bash - run: | - set -euo pipefail - - toolchain_file=base/rust-toolchain.toml - [ -f "$toolchain_file" ] || { echo "::error::$toolchain_file is missing"; exit 1; } - channel=$(awk -F '"' '/^[[:space:]]*channel[[:space:]]*=/ { print $2; exit }' "$toolchain_file") - profile=$(awk -F '"' '/^[[:space:]]*profile[[:space:]]*=/ { print $2; exit }' "$toolchain_file") - if [[ ! "$channel" =~ ^[A-Za-z0-9._+-]+$ ]]; then - echo "::error::$toolchain_file has an invalid Rust channel" - exit 1 - fi - case "${profile:-default}" in - minimal|default|complete) ;; - *) echo "::error::$toolchain_file has an invalid Rust profile"; exit 1 ;; - esac - - rustup run "$channel" rustc --version >/dev/null 2>&1 && exit 0 - echo "Installing Rust $channel (${profile:-default} profile) for the fresh base build" - rustup toolchain install "$channel" --profile "${profile:-default}" --no-self-update - - - shell: bash env: CPU_LABEL: ${{ inputs.label }} - CPU_OUTPUT_FILE: ${{ inputs.output-file }} - CPU_PROVENANCE_FILE: ${{ inputs.provenance-file }} - CPU_PROVENANCE_LABEL: ${{ inputs.provenance-label }} - CPU_WARNING_FILE: ${{ inputs.warning-file }} - LOG_CURRENT_CPU: ${{ inputs.log-current }} run: | set -euo pipefail export LC_ALL=C - resolve_path() { - if [[ "$1" == \~/* ]]; then - printf '%s/%s\n' "$HOME" "${1:2}" - else - printf '%s\n' "$1" - fi - } - - model_name() { - awk -F ': *' '/^Model name:/ { print $2; exit }' "$@" - } - - current_cpu_model=$(lscpu | model_name) - - cpu_report() { - echo "Context: $CPU_LABEL" - echo "Runner: ${RUNNER_NAME:-unknown} (${RUNNER_OS:-unknown}/${RUNNER_ARCH:-unknown})" - echo "Kernel: $(uname -srvm)" - echo "nproc: $(nproc)" - if [ -r /sys/fs/cgroup/cpu.max ]; then - echo "cgroup cpu.max: $(< /sys/fs/cgroup/cpu.max)" - fi - if [ -r /sys/fs/cgroup/cpuset.cpus.effective ]; then - echo "cgroup cpuset.cpus.effective: $(< /sys/fs/cgroup/cpuset.cpus.effective)" - fi - grep -m1 '^Cpus_allowed_list:' /proc/self/status || true - lscpu - flags=$({ grep -m1 -oE 'avx2|avx512[a-z0-9_]*' /proc/cpuinfo || true; } \ - | sort -u | tr '\n' ' ') - echo "AVX flags: ${flags:-absent}" - } - - if [ "$LOG_CURRENT_CPU" = true ]; then - echo "::group::$CPU_LABEL" - if [ -n "$CPU_OUTPUT_FILE" ]; then - output_file=$(resolve_path "$CPU_OUTPUT_FILE") - mkdir -p "$(dirname "$output_file")" - cpu_report | tee "$output_file" - else - cpu_report - fi - echo "::endgroup::" + cpu_info=$(lscpu) + cpu_model=$(printf '%s\n' "$cpu_info" | awk -F ': *' '/^Model name:/ { print $2; exit }') + vcpus=$(nproc) + ram_kib=$(awk '/^MemTotal:/ { print $2; exit }' /proc/meminfo) + ram=$(awk -v kib="$ram_kib" 'BEGIN { printf "%.1f GiB", kib / 1048576 }') + + echo "::group::$CPU_LABEL" + echo "Context: $CPU_LABEL" + echo "Runner: ${RUNNER_NAME:-unknown} (${RUNNER_OS:-unknown}/${RUNNER_ARCH:-unknown})" + echo "Kernel: $(uname -srvm)" + echo "nproc: $vcpus" + echo "RAM: $ram" + if [ -r /sys/fs/cgroup/cpu.max ]; then + echo "cgroup cpu.max: $(< /sys/fs/cgroup/cpu.max)" fi - - if [ -n "$CPU_PROVENANCE_FILE" ]; then - provenance_file=$(resolve_path "$CPU_PROVENANCE_FILE") - echo "::group::Native benchmark binary build CPU" - if [ -s "$provenance_file" ]; then - cat "$provenance_file" - else - echo "::warning::Binary build CPU provenance is unavailable (the cache may predate CPU reports)" - fi - echo "::endgroup::" - - provenance_model=$(model_name "$provenance_file" 2>/dev/null || true) - warning="" - if [ -z "$provenance_model" ] || [ -z "$current_cpu_model" ]; then - warning=$(printf '**CPU provenance unavailable for %s:** one report has no CPU model, so native-code compatibility cannot be checked.' "$CPU_PROVENANCE_LABEL") - elif [ "$provenance_model" != "$current_cpu_model" ]; then - warning=$(printf "**CPU model mismatch for %s:** built on \`%s\`; measured on \`%s\`. Native Rust code uses \`-Ctarget-cpu=native\`." "$CPU_PROVENANCE_LABEL" "$provenance_model" "$current_cpu_model") - fi - if [ -n "$warning" ]; then - echo "::warning::$warning" - if [ -n "$CPU_WARNING_FILE" ]; then - warning_file=$(resolve_path "$CPU_WARNING_FILE") - mkdir -p "$(dirname "$warning_file")" - printf '%s\n' "- $warning" >> "$warning_file" - fi - fi + if [ -r /sys/fs/cgroup/cpuset.cpus.effective ]; then + echo "cgroup cpuset.cpus.effective: $(< /sys/fs/cgroup/cpuset.cpus.effective)" fi + grep -m1 '^Cpus_allowed_list:' /proc/self/status || true + printf '%s\n' "$cpu_info" + flags=$({ grep -m1 -oE 'avx2|avx512[a-z0-9_]*' /proc/cpuinfo || true; } \ + | sort -u | tr '\n' ' ') + echo "AVX flags: ${flags:-absent}" + echo "::endgroup::" + + printf 'summary=CPU: `%s` · vCPUs: `%s` · RAM: `%s`\n' \ + "${cpu_model:-unknown}" "$vcpus" "$ram" >> "$GITHUB_OUTPUT" diff --git a/.github/actions/setup-lake-cache/action.yml b/.github/actions/setup-lake-cache/action.yml new file mode 100644 index 000000000..405aa846e --- /dev/null +++ b/.github/actions/setup-lake-cache/action.yml @@ -0,0 +1,32 @@ +name: Set up Namespace build cache +description: Mount the shared Namespace cache for Lake, Cargo, and optional tool caches + +inputs: + cache-modes: + description: Namespace cache modes to enable + required: false + default: rust + additional-paths: + description: Additional paths to mount on the Namespace cache volume + required: false + +outputs: + cache-hit: + description: Whether Namespace restored the build cache + value: ${{ steps.cache.outputs.cache-hit }} + +runs: + using: composite + steps: + - name: Create Lake build directory + shell: bash + run: mkdir -p "${{ github.workspace }}/.lake" + + - name: Mount Namespace build cache + id: cache + uses: namespacelabs/nscloud-cache-action@v1 + with: + cache: ${{ inputs.cache-modes }} + path: | + ${{ github.workspace }}/.lake + ${{ inputs.additional-paths }} diff --git a/.github/actions/setup-rust-toolchain/action.yml b/.github/actions/setup-rust-toolchain/action.yml index 6692caa65..0accaf5c4 100644 --- a/.github/actions/setup-rust-toolchain/action.yml +++ b/.github/actions/setup-rust-toolchain/action.yml @@ -1,29 +1,38 @@ name: Set up Rust toolchain description: >- - Install Rust on Warp Linux x64, configure compiler flags, and cache Cargo - artifacts. + Install Rust on supported Linux x64 runners, configure compiler flags, and + optionally cache Cargo artifacts. inputs: cache-workspaces: description: Cargo workspaces to cache required: false + use-github-cache: + description: Enable the setup action's Cargo cache + required: false + default: "true" + cache-provider: + description: Cache provider used by the Rust setup action + required: false + default: github avx512-codegen: - description: Enable AVX-512 code generation for the Warp x64 fleet's common ISA + description: Enable portable AVX-512 code generation for supported x64 runners required: false default: "true" runs: using: composite steps: - - name: Require Warp Linux x64 runner + - name: Require supported Linux x64 runner shell: bash env: IX_RUNNER_NAME: ${{ runner.name }} IX_RUNNER_OS: ${{ runner.os }} IX_RUNNER_ARCH: ${{ runner.arch }} run: | - if [[ "$IX_RUNNER_NAME" != warp-* || "$IX_RUNNER_OS" != Linux || "$IX_RUNNER_ARCH" != X64 ]]; then - echo "::error::setup-rust-toolchain requires a Warp Linux x64 runner; got name=$IX_RUNNER_NAME os=$IX_RUNNER_OS arch=$IX_RUNNER_ARCH" + if [[ "$IX_RUNNER_OS" != Linux || "$IX_RUNNER_ARCH" != X64 || \ + ("$IX_RUNNER_NAME" != warp-* && "$IX_RUNNER_NAME" != nsc-runner-*) ]]; then + echo "::error::setup-rust-toolchain requires a Warp or Namespace Linux x64 runner; got name=$IX_RUNNER_NAME os=$IX_RUNNER_OS arch=$IX_RUNNER_ARCH" exit 1 fi @@ -40,12 +49,12 @@ runs: echo "CARGO_NET_GIT_FETCH_WITH_CLI=true" >> "$GITHUB_ENV" fi - # The fleet mixes Intel Granite Rapids and AMD Zen 5, and a binary may be - # built on one and measured on another. Neither vendor's feature set - # contains the other's, so `-Ctarget-cpu=native` is not portable across - # the fleet: Zen 5 enables SSE4A, which LLVM emits (as INSERTQ, in - # witness generation) and Intel traps on with #UD. Pin the measured - # intersection instead. x86-64-v4 covers every AVX-512 subset Plonky3 + # The supported fleets mix Intel and AMD hosts, and cached artifacts may + # be built on one CPU model and consumed on another. Neither vendor's + # feature set contains the other's, so `-Ctarget-cpu=native` is not + # portable across the fleet: Zen 5 enables SSE4A, which LLVM emits (as + # INSERTQ, in witness generation) and Intel traps on with #UD. Pin the + # measured intersection instead. x86-64-v4 covers every AVX-512 subset Plonky3 # uses; +avx512vbmi2 keeps its VPSHRDQ interleave and +gfni keeps LLVM's # byte-shift lowering. blake3 selects its kernels via CPUID at runtime # and is unaffected. Pinning also makes codegen host-independent, so the @@ -59,14 +68,14 @@ runs: grep -qw "$f" /proc/cpuinfo || missing+=("$f") done if [ ${#missing[@]} -gt 0 ]; then - echo "::error::Runner CPU lacks required feature(s): ${missing[*]}. Benchmark binaries are built for x86-64-v4 +avx512vbmi2,+gfni." + echo "::error::Runner CPU lacks required feature(s): ${missing[*]}. Binaries are built for x86-64-v4 +avx512vbmi2,+gfni." exit 1 fi - uses: actions-rust-lang/setup-rust-toolchain@v1 with: rustflags: ${{ inputs.avx512-codegen == 'true' && '-Ctarget-cpu=x86-64-v4 -Ctarget-feature=+avx512vbmi2,+gfni -Dwarnings' || '-Dwarnings' }} - # Codegen is pinned above, so `target/` artifacts are interchangeable - # across every Warp x64 host. - cache-key: warp-x64 + cache: ${{ inputs.use-github-cache }} + cache-provider: ${{ inputs.cache-provider }} + cache-key: ${{ inputs.avx512-codegen == 'true' && 'x64-avx512' || 'x64-portable' }} cache-workspaces: ${{ inputs.cache-workspaces }} diff --git a/.github/workflows/bench-main.yml b/.github/workflows/bench-main.yml index d97e9a2e6..c24afecbc 100644 --- a/.github/workflows/bench-main.yml +++ b/.github/workflows/bench-main.yml @@ -13,8 +13,7 @@ name: Benchmark main # 2. compile — compiles each Lean env to a `.ixe` file (this IS the # compile benchmark) and caches the file for stage 3. # 3. benchmark — one job per remaining entry: restore the `.ixe` and -# run the entry's backend over it (aiur, zisk, ooc, -# decompile). +# run the entry's backend over it (aiur, ooc, decompile). # # Each entry uploads to its own bencher testbed/workload, so a threshold # reset for one workload never touches another. When the kernel REJECTS a @@ -40,36 +39,40 @@ env: jobs: # Build the `ix` and `bench-typecheck` binaries once and cache them; # every later job restores them instead of rebuilding. They are built - # with -Ctarget-cpu=native, so every job that runs them must use the - # same warp runner class. + # for the fleet's fixed AVX-512 baseline. Measured jobs stay on Warp so + # the benchmark testbed remains consistent. build: runs-on: warp-ubuntu-latest-x64-32x steps: - uses: actions/checkout@v7 - # Native codegen fixes the available instructions at build time. Carry - # this report with the binaries so every later measurement records both - # the build host and its own run host. + - name: Mount Lake build cache + uses: WarpBuilds/cache@v2 + with: + path: .lake + key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} + restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}- - name: Log build CPU uses: ./.github/actions/log-cpu with: label: Benchmark binary build CPU - output-file: ${{ runner.temp }}/benchmark-build-cpu.txt # 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-provider: warpbuild - uses: leanprover/lean-action@v1 with: auto-config: false build: true build-args: "ix --wfail -v" + use-github-cache: false - run: | mkdir -p ~/.local/bin echo | lake run install # copies ix -> ~/.local/bin/ix lake build bench-typecheck cp .lake/build/bin/bench-typecheck ~/.local/bin/ - cp "${{ runner.temp }}/benchmark-build-cpu.txt" ~/.local/bin/ chmod +x ~/.local/bin/bench-typecheck - - uses: actions/cache/save@v6 + - uses: WarpBuilds/cache/save@v2 with: path: ~/.local/bin key: bench-bins-${{ github.sha }} @@ -88,7 +91,7 @@ jobs: matrix: ${{ steps.matrix.outputs.matrix }} steps: - uses: actions/checkout@v7 - - uses: actions/cache/restore@v6 + - uses: WarpBuilds/cache/restore@v2 with: path: ~/.local/bin key: bench-bins-${{ github.sha }} @@ -142,7 +145,7 @@ jobs: - uses: actions/checkout@v7 # `lake build` below clones this package's Lake dependencies. - uses: ./.github/actions/authenticate-github-fetches - - uses: actions/cache/restore@v6 + - uses: WarpBuilds/cache/restore@v2 with: path: ~/.local/bin key: bench-bins-${{ github.sha }} @@ -150,7 +153,6 @@ jobs: uses: ./.github/actions/log-cpu with: label: Compile measurement CPU - provenance-file: ~/.local/bin/benchmark-build-cpu.txt - run: echo "$HOME/.local/bin" >> $GITHUB_PATH # Install the Lean toolchain. The mathlib olean cache is fetched only # for envs that import Mathlib (Mathlib, FLT) — the shared @@ -164,7 +166,7 @@ jobs: 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 + uses: WarpBuilds/cache@v2 with: path: ${{ env.COMPILE_DIR }}/.lake/packages/${{ matrix.cache_pkg }}/.lake/build key: ${{ matrix.cache_pkg }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', env.COMPILE_DIR)) }}-${{ hashFiles(format('{0}/lake-manifest.json', env.COMPILE_DIR)) }} @@ -180,12 +182,10 @@ jobs: ix bench run --backend compile --env ${{ matrix.env }} --out bench.json ix bench bmf --in bench.json --out benchmark.json cat benchmark.json - # Ask the registry three things about this env (instead of keeping + # Ask the registry for this env's metadata (instead of keeping # hand-written env lists here): # consumed — does any benchmark entry restore this env's `.ixe`? # If yes, cache it below. - # zkvm — does a zkVM entry execute this env? If yes, pre-cut - # its closure shards below. # testbed / workload / thresholds — the upload metadata for this # env's own compile benchmark. - id: gates @@ -194,39 +194,21 @@ jobs: ix bench ci matrix > matrix.json gate() { jq --arg env "${{ matrix.env }}" "[.[] | select($1).env] | index(\$env) >= 0" matrix.json; } echo "consumed=$(gate '.backend == "compile" | not')" >> "$GITHUB_OUTPUT" - echo "zkvm=$(gate '.backend == "zisk" or .backend == "sp1"')" >> "$GITHUB_OUTPUT" meta() { jq -r --arg env "${{ matrix.env }}" "first(.[] | select(.backend == \"compile\" and .env == \$env)).$1" matrix.json; } echo "testbed=$(meta testbed)" >> "$GITHUB_OUTPUT" echo "workload=$(meta workload)" >> "$GITHUB_OUTPUT" { echo "thresholds<> "$GITHUB_OUTPUT" - # Pre-cut the closure-shard artifacts for this env's zisk constants - # (extract → profile → shard; the planner's RAM budget decides each - # constant's shard count). The zisk runs can cut these lazily - # themselves, but doing it here — right next to the fresh `.ixe`, - # with the toolchain already installed — means they just restore a - # directory. - - if: steps.gates.outputs.zkvm == 'true' - name: Cut closure shards for zisk constants - run: ix bench shard --env ${{ matrix.env }} --ixe ${{ matrix.env }}.ixe # Cache the `.ixe` for the benchmark job. IMPORTANT: every restore of - # this key must list the same paths — actions/cache versions the + # this key must list the same paths — cache versions include the # entry by its path list, so a mismatched list is unreachable # whatever the key. Keeping this entry to one path lets bench-pr's # base-side restore fall back to that workflow's compile-job key (a # stacked PR's base is a PR head, which never passes through here). - if: steps.gates.outputs.consumed == 'true' - uses: actions/cache/save@v6 + uses: WarpBuilds/cache/save@v2 with: path: ${{ matrix.env }}.ixe key: bench-ixe-${{ github.sha }}-${{ matrix.env }} - # Shards get their own entry rather than riding the `.ixe`: only the - # zkVM envs have any, so bundling them would put a directory that - # usually doesn't exist into every `.ixe` restore's path list. - - if: steps.gates.outputs.zkvm == 'true' - uses: actions/cache/save@v6 - with: - path: zkshards-${{ matrix.env }} - key: bench-shards-${{ github.sha }}-${{ matrix.env }} # Upload the compile metrics. Testbed, workload, and threshold flags # all come from the registry (the reasoning behind each bound lives # next to `thresholds` in Ix/Cli/BenchCmd.lean). @@ -241,9 +223,8 @@ jobs: # One job per remaining matrix entry, all sharing this one step list # (same shape as bench-pr.yml's benchmark job). Each entry brings its - # own label, testbed, workload, and threshold flags, so the only - # backend-specific steps are the zkVM toolchain installs. Every entry - # restores the compile job's cached `.ixe` — nothing recompiles here. + # own label, testbed, workload, and threshold flags. Every entry restores + # the compile job's cached `.ixe` — nothing recompiles here. # # What each backend measures: # - aiur: the proof pipeline — per constant, every stage plus the @@ -252,11 +233,6 @@ jobs: # (stage 2); the KZG stages will fold in as they land. One # subprocess per constant under the RAM watchdog; a too-large # prove is killed and recorded as a `status: oom` row. - # - zisk: executes the same constants in the zkVM (deterministic - # cycle counts; proving would need a GPU, so execute-only). Each - # constant runs as the shard partition the planner's RAM budget - # sized for it (one shard when it fits), reusing the pre-cut - # zkshards-/ dirs; builds its Rust host in-job. # - ooc: the same kernel run out-of-circuit and in parallel (much # faster). One whole-env row plus one row per constant. # - decompile: the inverse of compile. Roundtrip correctness is @@ -276,7 +252,7 @@ jobs: params: ${{ fromJson(needs.plan.outputs.matrix) }} steps: - uses: actions/checkout@v7 - - uses: actions/cache/restore@v6 + - uses: WarpBuilds/cache/restore@v2 with: path: ~/.local/bin key: bench-bins-${{ github.sha }} @@ -284,19 +260,6 @@ jobs: uses: ./.github/actions/log-cpu with: label: Benchmark measurement CPU - provenance-file: ~/.local/bin/benchmark-build-cpu.txt - # The zkVM runs build their Rust host in-run; the rest run staged - # binaries only. (Restore an install-sp1 step here when sp1 is - # re-enabled in the registry.) - - if: matrix.params.backend == 'zisk' || matrix.params.backend == 'sp1' - uses: ./.github/actions/setup-rust-toolchain - with: - cache-workspaces: ${{ matrix.params.backend }} - - name: Install Zisk - if: matrix.params.backend == 'zisk' - uses: ./.github/actions/install-zisk - with: - proving-key: false - run: echo "$HOME/.local/bin" >> $GITHUB_PATH # Provision the toolchain so the staged binaries find libleanshared # (no package build). use-github-cache off: nothing to cache here, and @@ -308,33 +271,19 @@ jobs: use-github-cache: false # Pull the `.ixe` the compile job built — do NOT recompile here. # (The path list must match the compile job's save exactly.) - - uses: actions/cache/restore@v6 + - uses: WarpBuilds/cache/restore@v2 with: path: ${{ matrix.params.env }}.ixe key: bench-ixe-${{ github.sha }}-${{ matrix.params.env }} fail-on-cache-miss: true - # The pre-cut closure shards, for the backends that have any. Not - # fail-on-cache-miss: cutting them in the compile job is an - # optimisation, and `ix bench run` still cuts lazily without them. - - if: matrix.params.backend == 'zisk' || matrix.params.backend == 'sp1' - uses: actions/cache/restore@v6 - with: - path: zkshards-${{ matrix.params.env }} - key: bench-shards-${{ github.sha }}-${{ matrix.params.env }} # If the kernel rejects a constant, `ix bench run` exits 3 and this # step fails — that is a correctness regression, not a benchmark # blip. The completed rows are already on disk for the upload below. - name: Run ${{ matrix.params.label }} benchmark - run: | - # ZisK's ASM microservices mmap with MAP_LOCKED: raise the memlock - # hard limit in this shell so the tools `ix bench run` spawns - # inherit it. - if [ "${{ matrix.params.backend }}" = zisk ]; then - sudo prlimit --pid $$ --memlock=unlimited:unlimited - fi - ix bench run --backend ${{ matrix.params.backend }} \ - --env ${{ matrix.params.env }} --mode ${{ matrix.params.mode }} \ - --ixe ${{ matrix.params.env }}.ixe --out bench.json + run: >- + ix bench run --backend ${{ matrix.params.backend }} + --env ${{ matrix.params.env }} --mode ${{ matrix.params.mode }} + --ixe ${{ matrix.params.env }}.ixe --out bench.json # The ooc run writes a per-constant attribution CSV next to its # results file. Bencher stores metric rows only, so cache the CSV by # (SHA, cell) — bench-pr restores it to render the per-constant @@ -344,7 +293,7 @@ jobs: - name: Cache per-constant attribution CSV if: ${{ !cancelled() && matrix.params.backend == 'ooc' }} continue-on-error: true - uses: actions/cache/save@v6 + uses: WarpBuilds/cache/save@v2 with: path: bench.json.perconst.csv key: bench-perconst-${{ github.sha }}-${{ matrix.params.backend }}-${{ matrix.params.env }}-${{ matrix.params.mode }} diff --git a/.github/workflows/bench-pr.yml b/.github/workflows/bench-pr.yml index bd5cb24b1..64e6b84db 100644 --- a/.github/workflows/bench-pr.yml +++ b/.github/workflows/bench-pr.yml @@ -3,9 +3,7 @@ # The base is the PR's own base branch — main for an unstacked PR, the # parent PR's head for a stacked one — and the report is labelled with it. # -# !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] | all) [execute] -# (sp1 is disabled in the registry (Ix/Cli/BenchCmd.lean) — the parser skips it -# with a note in the config summary) +# !benchmark ([aiur] [ooc] [compile] [decompile] | all) [execute] # BENCH_ENVS=InitStd,Mathlib # which compiled envs (case-insensitive, any registry env; # # defaults to every env for compile/decompile, InitStd # # for the rest) @@ -41,7 +39,7 @@ # token switches it to the fast Phase-1-only mode (witness # generation; no bencher baseline exists for that, so the base side # comes from a base-SHA run). -# - zisk / sp1 / ooc: `execute`. +# - ooc: `execute`. # - compile: `ix compile .lean` → `.ixe`. # - decompile: `ix decompile` over the compile run's fresh `.ixe`. # The bare `fresh` token skips the bencher fetch and prevents persistent @@ -64,10 +62,10 @@ # access (anti-poisoning; no token permission can override it), so cache # saves would all fail. The issue_comment run therefore only checks the # commenter is an org MEMBER/OWNER and re-dispatches this same file as -# workflow_dispatch, which is allowed to save caches. The relay rejects fork -# PRs before dispatch so only repository writers can supply code to that cache -# scope. Manual dispatch already requires repo write access and may -# intentionally compare loose commits. +# workflow_dispatch, which is allowed to save caches. The MEMBER/OWNER command +# explicitly authorizes that PR head to run in the cache-writing context. +# Manual dispatch already requires repo write access and may intentionally +# compare loose commits. name: Benchmark pull requests on: @@ -126,11 +124,6 @@ jobs: COMMENT_BODY: ${{ github.event.comment.body }} PR_NUMBER: ${{ github.event.issue.number }} run: | - head_repo=$(gh api "repos/$GITHUB_REPOSITORY/pulls/$PR_NUMBER" --jq '.head.repo.full_name') - if [ "$head_repo" != "$GITHUB_REPOSITORY" ]; then - echo "::error::Comment-triggered benchmarks require a same-repository PR head" - exit 1 - fi gh workflow run bench-pr.yml \ --repo "$GITHUB_REPOSITORY" \ --ref "${{ github.event.repository.default_branch }}" \ @@ -145,12 +138,11 @@ jobs: # artifact for every later job. Normal runs may select a persistent # head-SHA cache. A cached `ix` may bootstrap command parsing, but `fresh` # replaces the full bundle before it is published to benchmark jobs. - # Built on a warp runner like bench-main's binaries, so both sides share - # the same instruction set (AVX-512) — and every job that runs these - # binaries must be a warp host too, or a plain GitHub host crashes with - # an illegal instruction. The job ends by parsing the !benchmark command - # with the selected `ix bench ci parse`: the registry lives in Lean, so - # the matrix can only be computed after a binary is available. + # Built on a Warp runner like bench-main's binaries, so both sides use the + # same fixed AVX-512 baseline and benchmark testbed. The job ends by parsing + # the !benchmark command with the selected `ix bench ci parse`: the registry + # lives in Lean, so the matrix can only be computed after a binary is + # available. build: if: github.event_name == 'workflow_dispatch' runs-on: warp-ubuntu-latest-x64-32x @@ -161,11 +153,12 @@ jobs: fresh: ${{ steps.parse.outputs.fresh }} passthrough-env: ${{ steps.parse.outputs.passthrough-env }} config-summary: ${{ steps.parse.outputs.config-summary }} + hardware-summary: ${{ steps.cpu.outputs.summary }} # Set (with the step failing) when the !benchmark command was # rejected; the failure comment quotes it. parse-error: ${{ steps.parse.outputs.parse-error }} steps: - # The relay admits only same-repository heads; manual dispatch requires + # 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 id: target @@ -182,7 +175,7 @@ jobs: # The job builds and runs PR code; never leave the token in .git. persist-credentials: false - id: bins - uses: actions/cache/restore@v6 + uses: WarpBuilds/cache/restore@v2 with: path: ~/.local/bin key: bench-bins-${{ steps.target.outputs.revision }} @@ -190,6 +183,8 @@ jobs: # remaining binaries are built after parsing, when `fresh` is known. - if: steps.bins.outputs.cache-hit != 'true' uses: ./.github/actions/setup-rust-toolchain + with: + cache-provider: warpbuild # A persistent hit still needs the matching toolchain for libleanshared. - uses: leanprover/lean-action@v1 with: @@ -214,40 +209,28 @@ jobs: # run replaces it before the bundle can reach any measured job. - if: steps.parse.outputs.fresh == '1' && steps.bins.outputs.cache-hit == 'true' uses: ./.github/actions/setup-rust-toolchain - # `.cargo/config.toml` sets `-Ctarget-cpu=native`; log the build CPU so a - # benchmark shift can be traced to the host that selected the native - # instruction set. The report travels with the binaries below. - - name: Log build CPU - if: steps.parse.outputs.fresh == '1' || steps.bins.outputs.cache-hit != 'true' + with: + cache-provider: warpbuild + - name: Log benchmark runner CPU + id: cpu uses: ./.github/actions/log-cpu with: - label: Benchmark binary build CPU - output-file: ${{ runner.temp }}/benchmark-build-cpu.txt + label: Benchmark runner CPU - name: Build benchmark binaries if: steps.parse.outputs.fresh == '1' || steps.bins.outputs.cache-hit != 'true' run: | lake build ix bench-typecheck cp .lake/build/bin/ix .lake/build/bin/bench-typecheck ~/.local/bin/ - cp "${{ runner.temp }}/benchmark-build-cpu.txt" ~/.local/bin/ chmod +x ~/.local/bin/ix ~/.local/bin/bench-typecheck - # Cache entries are immutable and may lack optional provenance. Keep the - # run artifact's shape stable and state explicitly when its build host is - # unknown. - - name: Ensure build CPU provenance - run: | - if [ ! -s "$HOME/.local/bin/benchmark-build-cpu.txt" ]; then - echo "Benchmark binary build CPU unavailable: cache predates CPU provenance." \ - > "$HOME/.local/bin/benchmark-build-cpu.txt" - fi - if: steps.parse.outputs.fresh != '1' && steps.bins.outputs.cache-hit != 'true' - uses: actions/cache/save@v6 + uses: WarpBuilds/cache/save@v2 with: path: ~/.local/bin key: bench-bins-${{ steps.target.outputs.revision }} - name: Package run binaries run: >- tar -C "$HOME/.local/bin" -cf benchmark-binaries.tar - ix bench-typecheck benchmark-build-cpu.txt + ix bench-typecheck - name: Upload run binaries uses: actions/upload-artifact@v7 with: @@ -280,6 +263,7 @@ jobs: BUILD_RESULT: ${{ needs.build.result }} PARSE_ERROR: ${{ needs.build.outputs.parse-error }} SUMMARY: ${{ needs.build.outputs.config-summary }} + HARDWARE: ${{ needs.build.outputs.hardware-summary }} HEAD_SHA: ${{ needs.build.outputs.revision }} run: | RUN_URL="${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" @@ -299,8 +283,11 @@ jobs: echo if [ -n "$SUMMARY" ]; then echo "> $SUMMARY" - echo fi + if [ -n "$HARDWARE" ]; then + echo "> $HARDWARE" + fi + echo echo "Benchmarking \`${HEAD_SHA:0:7}\` — this comment will be replaced with the results when the run finishes." echo echo "[Watch progress]($RUN_URL)" @@ -356,9 +343,9 @@ jobs: - name: Restore published .ixe if: needs.build.outputs.fresh != '1' id: pr-ixe - uses: actions/cache/restore@v6 + uses: WarpBuilds/cache/restore@v2 with: - # actions/cache derives an entry's version from its path list, so + # The cache derives an entry's version from its path list, so # the list is effectively part of the key: this one path matches # bench-main's compile-job save, which lets a stacked PR's base # run reach either producer's entry from one restore. @@ -367,11 +354,9 @@ jobs: - name: Restore published compile row if: needs.build.outputs.fresh != '1' id: pr-row - uses: actions/cache/restore@v6 + uses: WarpBuilds/cache/restore@v2 with: - path: | - compile.json - compile-cpu-warnings.md + path: compile.json key: bench-pr-row-${{ needs.build.outputs.revision }}-${{ matrix.env }} - name: Select compile source id: compile-source @@ -390,7 +375,6 @@ jobs: - name: Unpack run binaries if: steps.compile-source.outputs.rebuild == 'true' run: | - rm -f compile-cpu-warnings.md mkdir -p "$HOME/.local/bin" tar -C "$HOME/.local/bin" -xf benchmark-binaries.tar echo "$HOME/.local/bin" >> "$GITHUB_PATH" @@ -399,9 +383,6 @@ jobs: uses: ./.github/actions/log-cpu with: label: Compile measurement CPU - provenance-file: ~/.local/bin/benchmark-build-cpu.txt - provenance-label: PR benchmark binaries during compile - warning-file: compile-cpu-warnings.md # Pointed at the Benchmarks/Compile subpackage (same toolchain as # the root): mathlib is a dependency only there, so the mathlib # cache fetch has to run from that directory. @@ -426,7 +407,7 @@ jobs: run: ix bench run --backend compile --env ${{ matrix.env }} --out compile.json - name: Publish .ixe if: needs.build.outputs.fresh != '1' && steps.pr-ixe.outputs.cache-hit != 'true' - uses: actions/cache/save@v6 + uses: WarpBuilds/cache/save@v2 with: # Path lists are version-significant — keep this identical to the # restore above and to bench-main's save. @@ -436,11 +417,9 @@ jobs: # reuses it as its PR side (same runner class, binaries, command). - name: Publish compile row if: needs.build.outputs.fresh != '1' && steps.pr-row.outputs.cache-hit != 'true' - uses: actions/cache/save@v6 + uses: WarpBuilds/cache/save@v2 with: - path: | - compile.json - compile-cpu-warnings.md + path: compile.json key: bench-pr-row-${{ needs.build.outputs.revision }}-${{ matrix.env }} - name: Upload run environment uses: actions/upload-artifact@v7 @@ -449,7 +428,6 @@ jobs: path: | ${{ matrix.env }}.ixe compile.json - compile-cpu-warnings.md if-no-files-found: error retention-days: 1 overwrite: true @@ -517,9 +495,6 @@ jobs: uses: ./.github/actions/log-cpu with: label: Benchmark job CPU - provenance-file: .lake/build/bin/benchmark-build-cpu.txt - provenance-label: PR benchmark binaries in this job - warning-file: cpu-warnings.md # Toolchain only (no package build, no mathlib cache): the restored # binaries need the toolchain's libleanshared to run. This job never # compiles an env — the `.ixe` and compile row come from the compile @@ -535,24 +510,6 @@ jobs: uses: actions/download-artifact@v8 with: name: benchmark-env-${{ matrix.params.env }} - # zkVM runs additionally need the Rust toolchain + the backend's toolchain - # and system deps (the shared composite install actions). - - name: Set up zkVM Rust toolchain - if: matrix.params.backend == 'zisk' || matrix.params.backend == 'sp1' - uses: ./.github/actions/setup-rust-toolchain - with: - cache-workspaces: ${{ matrix.params.backend }} - # sp1 is disabled in the registry (execute too slow for CI); - # re-enable it there and uncomment this install step to restore it. - # - name: Install SP1 - # if: matrix.params.backend == 'sp1' - # uses: ./.github/actions/install-sp1 - - name: Install Zisk - if: matrix.params.backend == 'zisk' - uses: ./.github/actions/install-zisk - with: - proving-key: false - # ---------- PR side ---------- # The PR side runs first: `ix bench run` selects its constants from # the shared set (Ix/BenchConstants.lean), and pr.json's row names @@ -566,11 +523,6 @@ jobs: # the job, after the table upload. continue-on-error: true run: | - if [ "$BACKEND" = zisk ]; then - # ZisK's ASM microservices mmap with MAP_LOCKED: raise the memlock - # hard limit in this shell so the spawned tools inherit it. - sudo prlimit --pid $$ --memlock=unlimited:unlimited - fi if [ "$BACKEND" = compile ]; then # The compile job already measured this env's compile (same # runner class, binaries, and command) — reuse its row instead @@ -638,7 +590,7 @@ jobs: id: perconst if: matrix.params.backend == 'ooc' && env.FRESH != '1' continue-on-error: true - uses: actions/cache/restore@v6 + uses: WarpBuilds/cache/restore@v2 with: path: bench.json.perconst.csv key: bench-perconst-${{ env.BASE_SHA }}-${{ matrix.params.backend }}-${{ matrix.params.env }}-${{ matrix.params.mode }} @@ -675,35 +627,25 @@ jobs: - name: Restore base binaries (bench-bins cache) if: steps.decide.outputs.run-base == 'true' && env.FRESH != '1' id: base-bins - uses: actions/cache/restore@v6 + uses: WarpBuilds/cache/restore@v2 with: path: ~/.local/bin key: bench-bins-${{ env.BASE_SHA }} # Two producers compile the env at a given SHA: bench-main for main # commits, this workflow's compile job for PR heads. A stacked PR's # base is the latter, so both keys are tried from one step. This works - # because both producers save the same single path; actions/cache - # versions an entry by its paths. restore-keys matches by prefix, so + # because both producers save the same single path; the cache versions + # an entry by its paths. restore-keys matches by prefix, so # no registry env name may be a prefix of another. - name: Restore base .ixe (bench-main or bench-pr compile cache) if: steps.decide.outputs.run-base == 'true' && env.FRESH != '1' id: base-ixe - uses: actions/cache/restore@v6 + uses: WarpBuilds/cache/restore@v2 with: path: ${{ matrix.params.env }}.ixe key: bench-ixe-${{ env.BASE_SHA }}-${{ matrix.params.env }} restore-keys: | bench-pr-ixe-${{ env.BASE_SHA }}-${{ matrix.params.env }} - # Shards live in their own entry and only exist for the zkVM - # backends; without them `ix bench run` cuts them itself. - - name: Restore base closure shards - if: >- - steps.decide.outputs.run-base == 'true' && env.FRESH != '1' && - (matrix.params.backend == 'zisk' || matrix.params.backend == 'sp1') - uses: actions/cache/restore@v6 - with: - path: zkshards-${{ matrix.params.env }} - key: bench-shards-${{ env.BASE_SHA }}-${{ matrix.params.env }} # Cached base binaries are only usable when both `lean-toolchain` # files match, and — for Mathlib — only when the `.ixe` also # restored (otherwise the base side would need mathlib oleans that @@ -727,7 +669,6 @@ jobs: if [ "$BENV" != Mathlib ] || [ "$ixe" = true ]; then mkdir -p base/.lake/build/bin mv ~/.local/bin/ix ~/.local/bin/bench-typecheck base/.lake/build/bin/ 2>/dev/null || true - mv ~/.local/bin/benchmark-build-cpu.txt base/.lake/build/bin/ 2>/dev/null || true [ -x base/.lake/build/bin/ix ] && [ -x base/.lake/build/bin/bench-typecheck ] \ && cached=true fi @@ -735,20 +676,18 @@ jobs: echo "cached=$cached" >> "$GITHUB_OUTPUT" echo "base .ixe: $([ "$ixe" = true ] && echo restored from cache || echo compiling in the base run)" echo "base binaries: $([ "$cached" = true ] && echo restored from cache || echo building from source)" - - name: Log cached base binary build CPU - if: steps.decide.outputs.run-base == 'true' && steps.base-src.outputs.cached == 'true' - uses: ./.github/actions/log-cpu - with: - log-current: "false" - provenance-file: base/.lake/build/bin/benchmark-build-cpu.txt - provenance-label: Cached base benchmark binaries - warning-file: cpu-warnings.md + - name: Set up changed base Rust toolchain + if: steps.decide.outputs.run-base == 'true' && steps.base-src.outputs.cached != 'true' + working-directory: base + run: | + if ! cmp -s rust-toolchain.toml ../rust-toolchain.toml; then + rustup show active-toolchain || rustup toolchain install + fi - name: Log base build CPU if: steps.decide.outputs.run-base == 'true' && steps.base-src.outputs.cached != 'true' uses: ./.github/actions/log-cpu with: label: Base benchmark binary build CPU - output-file: base/.lake/build/bin/benchmark-build-cpu.txt - name: Build base (ix, bench-typecheck) if: steps.decide.outputs.run-base == 'true' && steps.base-src.outputs.cached != 'true' uses: leanprover/lean-action@v1 @@ -789,12 +728,6 @@ jobs: run: | if [ "${{ steps.base-src.outputs.ixe }}" = true ]; then mv "${{ matrix.params.env }}.ixe" "base/${{ matrix.params.env }}.ixe" - # Shards, when restored above: in place, `ix bench run` skips - # re-cutting them for the base tree. - mv "zkshards-${{ matrix.params.env }}" "base/zkshards-${{ matrix.params.env }}" 2>/dev/null || true - fi - if [ "$BACKEND" = zisk ]; then - sudo prlimit --pid $$ --memlock=unlimited:unlimited fi flags="" if [ -n "$CONSTS" ]; then @@ -848,15 +781,11 @@ jobs: - name: Build comparison table run: | mkdir -p out - if [ "$BACKEND" = compile ] && [ -s compile-cpu-warnings.md ]; then - cat compile-cpu-warnings.md >> cpu-warnings.md - fi ix bench compare \ --backend "$BACKEND" --env "$BENV" --mode "$MODE" \ --base "$GITHUB_WORKSPACE/main.json" --pr "$GITHUB_WORKSPACE/pr.json" \ --base-source "${{ steps.decide.outputs.source }}" \ --base-label "${BASE_REF:-${BASE_SHA::7}}" \ - --warning-file "$GITHUB_WORKSPACE/cpu-warnings.md" \ --out "out/table-$LABEL.md" cat "out/table-$LABEL.md" @@ -919,13 +848,21 @@ jobs: - name: Build comment body env: SUMMARY: ${{ needs.build.outputs.config-summary }} + HARDWARE: ${{ needs.build.outputs.hardware-summary }} HEAD_SHA: ${{ needs.build.outputs.revision }} BASE_SHA: ${{ inputs.base-sha }} BASE_REF: ${{ inputs.base-ref }} run: | mkdir -p tables # absent when no run uploaded a table + summary="$SUMMARY" + if [ -n "$HARDWARE" ]; then + if [ -n "$summary" ]; then + summary="$summary"$'\n\n' + fi + summary="$summary$HARDWARE" + fi ix bench report \ - --tables tables --summary "$SUMMARY" \ + --tables tables --summary "$summary" \ --head "$HEAD_SHA" \ --base-label "${BASE_REF:-${BASE_SHA::7}}" \ --repo-url "${{ github.server_url }}/${{ github.repository }}" \ diff --git a/.github/workflows/bencher-plots.yml b/.github/workflows/bencher-plots.yml index 2db968c67..870776146 100644 --- a/.github/workflows/bencher-plots.yml +++ b/.github/workflows/bencher-plots.yml @@ -33,7 +33,7 @@ jobs: # exact cache when bench-main has finished its build, else the newest # available (prefix match) — whose compiled-in registry may then lag # the checkout. - - uses: actions/cache/restore@v6 + - uses: WarpBuilds/cache/restore@v2 with: path: ~/.local/bin key: bench-bins-${{ github.sha }} diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 267f0b62e..dbb252c3f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -13,29 +13,41 @@ concurrency: cancel-in-progress: true jobs: - # Build Ix once and cache `.lake` under lean-action's per-sha key. That cache - # holds the base Ix build — lean-action saves it right after building the - # default lib, before the all-targets lint below — and the parallel lean-test - # job and merge-tests.yml's Lake jobs restore it instead of recompiling the - # base. `test: false` keeps this job build-only; those jobs run the tests. It - # also compiles and publishes the small `nataddcomm.ixe` fixture the zkVM - # execution gates (sp1-build/zisk-build) run their guests over: they need this - # exact `ix` build, so they consume it as an artifact and gate on this job - # succeeding. + merge-tests: + name: Merge tests + if: github.event_name == 'pull_request' + runs-on: ubuntu-latest + steps: + - name: Defer tests to merge queue + run: echo "Merge tests run against the merge group's synthetic commit." + + # Build every regular Lake target before the test fan-out. The Namespace + # volume is committed only after this job succeeds, so every saved build + # cache contains the complete build rather than one parallel job's subset. + # The small `nataddcomm.ixe` fixture is passed separately to the zkVM jobs. build: - runs-on: warp-ubuntu-latest-x64-16x + runs-on: + - nscloud-ubuntu-26.04-amd64-16x32-with-cache + - nscloud-cache-size-50gb + - nscloud-cache-tag-argumentcomputer-ix steps: - uses: actions/checkout@v7 - uses: ./.github/actions/setup-rust-toolchain + with: + use-github-cache: "false" + - uses: ./.github/actions/setup-lake-cache - uses: leanprover/lean-action@v1 with: build-args: "--wfail -v" test: false + use-github-cache: false # build-all lint driver compiles every lib/exe target with --wfail, so a # warning in any target (exes, benchmarks, Apps) — not just the default lib # lean-action builds above — fails CI. - name: Build all targets run: lake lint -- --wfail -v + - name: Build Ix.Tc formal verification + run: lake build IxTcVerify - name: Check codegen'd IxVM kernel is up to date run: lake exe ix codegen --check - name: Check Lean versions match for Ix and compiler bench @@ -54,31 +66,21 @@ jobs: if-no-files-found: error retention-days: 1 - # The primary test tier, plus the two extras, over the base build the - # `build` job cached. Restores `.lake` read-only (exact per-sha key the - # `build` job wrote, prefix fallback otherwise); lean-action runs the whole - # primary tier as a bare `lake test` against that restored build (no - # build/cache of its own). No `--wfail` there: `test-args` is declared but - # unwired in the released `v1`, so it would be silently ignored, and the - # `build` job already compiles every lib and exe -- `Tests` and `IxTests` - # included -- under `lake lint -- --wfail -v`. The CLI step covers the one - # primary runner that is special-cased ahead of suite dispatch in - # `Tests/Main.lean`; ignored suites run only in `merge-tests.yml`. + # The primary test tier consumes the complete cache but cannot commit its + # local changes. The build job remains the sole shared-cache writer. lean-test: needs: build - runs-on: warp-ubuntu-latest-x64-16x + runs-on: + - nscloud-ubuntu-26.04-amd64-16x32-with-cache + - nscloud-cache-size-50gb + - nscloud-cache-tag-argumentcomputer-ix + - nscloud-cache-exp-do-not-commit steps: - uses: actions/checkout@v7 - uses: ./.github/actions/setup-rust-toolchain - # `./.lake`, not `.lake`: the cache path is hashed into the entry's - # version, and lean-action saves under `./.lake`, so a bare `.lake` here - # computes a different version and the restore misses despite the key - # matching. - - uses: actions/cache/restore@v6 - with: - path: ./.lake - key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} - restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}- + with: + use-github-cache: "false" + - uses: ./.github/actions/setup-lake-cache - uses: leanprover/lean-action@v1 with: auto-config: false @@ -87,11 +89,24 @@ jobs: - name: Test Ix CLI run: lake test --wfail -- cli + # Lake and root Cargo builds both use the repository's target directory, so + # these two writers share a volume in dependency order. Namespace volumes + # are last-write-wins; parallel zkVM writers use dedicated tags, while CUDA + # consumes the primary cache without committing its feature-specific output. + # Namespace's remote sccache could share compatible compilation units across + # the zkVM volumes without serializing the jobs. rust-test: - runs-on: warp-ubuntu-latest-x64-8x + needs: build + runs-on: + - nscloud-ubuntu-26.04-amd64-8x16-with-cache + - nscloud-cache-size-50gb + - nscloud-cache-tag-argumentcomputer-ix steps: - uses: actions/checkout@v7 - uses: ./.github/actions/setup-rust-toolchain + with: + use-github-cache: "false" + - uses: ./.github/actions/setup-lake-cache - uses: taiki-e/install-action@nextest # Install Lean for rust-bindgen step - uses: leanprover/lean-action@v1 @@ -117,8 +132,19 @@ jobs: # Compile and link the opt-in backend without requiring a GPU. Runtime and # proof-byte equivalence are covered by multi-stark's NVIDIA smoke suite. cuda-compile: - runs-on: warp-ubuntu-latest-x64-8x - container: nvidia/cuda:12.8.1-devel-ubuntu24.04 + needs: build + runs-on: + - nscloud-ubuntu-26.04-amd64-8x16-with-cache + - nscloud-cache-size-50gb + - nscloud-cache-tag-argumentcomputer-ix + - nscloud-cache-exp-do-not-commit + container: + image: nvidia/cuda:13.3.1-devel-ubuntu26.04 + env: + NSC_CACHE_PATH: ${{ env.NSC_CACHE_PATH }} + volumes: + - /cache:/cache + options: --cap-add=SYS_ADMIN env: # This job validates feature plumbing and the Rust-staticlib-to-Lean # link without paying for a GPU runner. Multi-stark CI compiles the @@ -131,8 +157,11 @@ jobs: run: | apt-get update apt-get install --yes --no-install-recommends \ - build-essential ca-certificates curl git libclang-dev + build-essential ca-certificates curl git libclang-dev sudo - uses: ./.github/actions/setup-rust-toolchain + with: + use-github-cache: "false" + - uses: ./.github/actions/setup-lake-cache - uses: leanprover/lean-action@v1 with: auto-config: false @@ -144,13 +173,11 @@ jobs: # zkVM host build + execute gate: do the Zisk/SP1 hosts (and their guest # ELFs, via each workspace's build.rs) still compile AND run? rust-test - # doesn't build these workspaces (special toolchains), and bench-main.yml's - # zkVM runs — which also run real executions — tolerate per-constant - # failures by design (dropped rows, OOM sentinels), so they never turn red - # on a breakage. These jobs are the red-X signal: each builds its host, then - # runs the guest in the VM over `nataddcomm.ixe` (a ~40-constant closure the - # `build` job publishes as an artifact). They run in parallel with the test - # jobs and with each other after `build` succeeds. Both hosts exit + # doesn't build these workspaces because they need special toolchains. These + # jobs are the red-X signal: each builds its host, then runs the guest in the + # VM over `nataddcomm.ixe` (a ~40-constant closure the `build` job publishes + # as an artifact). They run in parallel with the test jobs and with each + # other after `build` succeeds. Both hosts exit # non-zero when the kernel rejects a constant (sp1: EXIT_REJECTED; zisk: # `reject_failures`), so a guest that compiles but panics / faults / rejects # fails the job. Both execute paths are keyless: Zisk uses its SDK's @@ -160,12 +187,20 @@ jobs: sp1-build: name: SP1 host build needs: build - runs-on: warp-ubuntu-latest-x64-16x + runs-on: + - nscloud-ubuntu-26.04-amd64-8x16-with-cache + - nscloud-cache-size-50gb + - nscloud-cache-tag-argumentcomputer-ix-sp1 steps: - uses: actions/checkout@v7 - uses: ./.github/actions/setup-rust-toolchain with: - cache-workspaces: sp1 + use-github-cache: "false" + - uses: ./.github/actions/setup-lake-cache + with: + additional-paths: | + ${{ github.workspace }}/sp1/target + ${{ github.workspace }}/sp1/guest/target - uses: ./.github/actions/install-sp1 # The precompile-aware SP1 runner-binary is auto-built from the fork git # dep by `sp1-core-executor-runner`'s build script — no manual override. @@ -199,12 +234,21 @@ jobs: zisk-build: name: Zisk host build needs: build - runs-on: warp-ubuntu-latest-x64-16x + runs-on: + - nscloud-ubuntu-26.04-amd64-8x16-with-cache + - nscloud-cache-size-50gb + - nscloud-cache-tag-argumentcomputer-ix-zisk steps: - uses: actions/checkout@v7 - uses: ./.github/actions/setup-rust-toolchain with: - cache-workspaces: zisk + use-github-cache: "false" + - uses: ./.github/actions/setup-lake-cache + with: + additional-paths: | + ${{ github.workspace }}/zisk/target + ${{ github.workspace }}/zisk/guest/target + ${{ github.workspace }}/zisk/agg-guest/target - uses: ./.github/actions/install-zisk with: proving-key: false diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index ab4d1c4c2..4963e986e 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -8,9 +8,8 @@ # The gates are job-level `if`s rather than workflow-level `on.paths` # (or a dynamically-built matrix) deliberately: a required check that # never triggers sticks at "Expected", while a skipped job satisfies it. -# When the rust analysis does run, it runs on a warp host (CodeQL scales -# with cores; default setup pins it to a stock 4-core runner) with the -# dependency extraction cached between runs. +# Rust analysis runs only when Rust inputs change, with dependency extraction +# cached between runs. name: CodeQL on: diff --git a/.github/workflows/merge-tests.yml b/.github/workflows/merge-tests.yml index dccdf83cd..b293c7996 100644 --- a/.github/workflows/merge-tests.yml +++ b/.github/workflows/merge-tests.yml @@ -1,9 +1,11 @@ name: Merge tests on: - pull_request: - branches: [main] merge_group: + issue_comment: + types: [created] + +run-name: "${{ github.event_name == 'issue_comment' && format('Merge tests for PR #{0}', github.event.issue.number) || 'Merge tests' }}" permissions: contents: read @@ -12,16 +14,80 @@ permissions: # cannot satisfy the required check, so runs are never superseded here. jobs: + prepare: + name: Prepare merge tests + 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: + issues: write + pull-requests: write + outputs: + comment-id: ${{ steps.post.outputs.comment-id }} + pr: ${{ steps.target.outputs.pr }} + revision: ${{ steps.target.outputs.revision }} + steps: + - name: Resolve test revision + id: target + env: + EVENT_NAME: ${{ github.event_name }} + EVENT_SHA: ${{ github.sha }} + GH_TOKEN: ${{ github.token }} + PR_NUMBER: ${{ github.event.issue.number }} + run: | + if [ "$EVENT_NAME" = issue_comment ]; 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" \ + --jq '.merge_commit_sha // empty') + echo "pr=$PR_NUMBER" >> "$GITHUB_OUTPUT" + else + revision=$EVENT_SHA + fi + + [[ "$revision" =~ ^[0-9a-f]{40}$ ]] \ + || { echo "::error::PR does not currently have a test merge commit"; exit 1; } + echo "revision=$revision" >> "$GITHUB_OUTPUT" + + - name: Compose initial comment + if: github.event_name == 'issue_comment' + env: + MERGE_SHA: ${{ steps.target.outputs.revision }} + PR_NUMBER: ${{ steps.target.outputs.pr }} + run: | + { + echo "## ⏳ Merge tests running…" + echo + echo "Running the ignored test suite for PR #$PR_NUMBER at \`${MERGE_SHA:0:7}\`." + echo + echo "[In-progress logs](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})" + } > comment-body.md + + - name: Post initial comment + if: github.event_name == 'issue_comment' + id: post + uses: peter-evans/create-or-update-comment@v5 + with: + token: ${{ github.token }} + issue-number: ${{ steps.target.outputs.pr }} + body-path: comment-body.md + merge-tests: name: ${{ matrix.name }} - if: ${{ github.event_name == 'merge_group' }} + needs: prepare + if: ${{ github.event_name == 'merge_group' || github.event_name == 'issue_comment' }} strategy: fail-fast: true matrix: include: - name: Lake ignored tests (compile pipeline) kind: lake - runner: warp-ubuntu-latest-x64-32x test_args: >- --ignored rust-canon-roundtrip serial-canon-roundtrip parallel-canon-roundtrip @@ -29,114 +95,121 @@ jobs: rust-decompile validate-aux aux-gen-diff decompile-diff - name: Lake ignored tests (compile) kind: lake - runner: warp-ubuntu-latest-x64-32x test_args: --ignored compile - name: Lake ignored tests (decompile) kind: lake - runner: warp-ubuntu-latest-x64-32x test_args: --ignored decompile - name: Lake ignored tests (misc) kind: lake - runner: warp-ubuntu-latest-x64-32x test_args: >- --ignored shard-map catalog-dedup commit-io fidelity-initstd kernel-ixon-roundtrip kernel-tutorial kernel-check-env kernel-check-const rust-kernel-build-primitives rust-kernel-build-prim-origs ixvm zk_voting: true - - name: Valgrind FFI - kind: valgrind - runner: warp-ubuntu-latest-x64-8x - - name: Ix.Tc verification and parity + - name: Ix.Tc unit and parity tests kind: tc - runner: warp-ubuntu-latest-x64-16x test_args: >- - --ignored tc-anon-diff tc-init tc-tutorial tc-roundtrip tc-ingress-meta tc-pins tc-accel-diff lean4lean - runs-on: ${{ matrix.runner }} + runs-on: + - nscloud-ubuntu-26.04-amd64-32x64-with-cache + - nscloud-cache-size-50gb + - nscloud-cache-tag-argumentcomputer-ix + - nscloud-cache-exp-do-not-commit steps: - name: Validate merge-test variant env: TEST_KIND: ${{ matrix.kind }} run: | case "$TEST_KIND" in - lake|valgrind|tc) ;; + lake|tc) ;; *) echo "::error::Unknown merge-test variant: $TEST_KIND"; exit 1 ;; esac - uses: actions/checkout@v7 - - uses: ./.github/actions/setup-rust-toolchain with: - # Valgrind cannot decode the AVX-512 the fleet baseline emits. - avx512-codegen: ${{ matrix.kind != 'valgrind' }} + ref: ${{ github.event_name == 'issue_comment' && format('refs/pull/{0}/merge', needs.prepare.outputs.pr) || needs.prepare.outputs.revision }} + persist-credentials: false - # A merge group has its own SHA, so restore the nearest compatible build - # produced by ordinary CI and let Lake rebuild anything that changed. - - if: ${{ matrix.kind == 'lake' }} - uses: actions/cache/restore@v6 - with: - path: ./.lake - key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} - restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}- - - # Valgrind cannot decode AVX-512, so its portable artifacts must not - # share `.lake` with native builds. - - if: ${{ matrix.kind == 'valgrind' }} - uses: actions/cache@v6 - with: - path: ./.lake - key: lake-valgrind-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} - restore-keys: lake-valgrind-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}- - - # A generic cache on the merge-queue ref can shadow a complete `lake-tc` - # cache from main, so this deliberately has no base-cache fallback. - - if: ${{ matrix.kind == 'tc' }} - uses: actions/cache@v6 - with: - path: ./.lake - key: lake-tc-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} - restore-keys: lake-tc-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}- + - name: Verify test revision + env: + TEST_REVISION: ${{ needs.prepare.outputs.revision }} + run: | + checked_out=$(git rev-parse HEAD) + if [ "$checked_out" != "$TEST_REVISION" ]; then + echo "::error::PR merge ref changed before the run started; comment !merge-tests again" + exit 1 + fi - # The Rust FFI bindgen build also needs the Lean toolchain and headers. - - if: ${{ matrix.kind != 'valgrind' }} - uses: leanprover/lean-action@v1 + - uses: ./.github/actions/setup-rust-toolchain with: - auto-config: false - use-github-cache: false - - if: ${{ matrix.kind == 'valgrind' }} - uses: leanprover/lean-action@v1 + use-github-cache: "false" + - uses: ./.github/actions/setup-lake-cache + - uses: leanprover/lean-action@v1 with: auto-config: false - build: true - build-args: "IxTests" use-github-cache: false - # The misc partition drives `.lake/build/bin/ix` in subprocesses. The - # prefix cache can contain an executable from an older SHA because the - # ordinary CI cache is saved before its all-targets lint builds `ix`. - # Rebuild it explicitly so the CLI and the checked-out tests agree. - - name: Build current ix CLI for subprocess tests - if: ${{ matrix.kind == 'lake' && matrix.zk_voting }} - run: lake build ix - - name: Run ignored Lake test partition if: ${{ matrix.kind == 'lake' }} run: lake test --wfail -- ${{ matrix.test_args }} + - name: Run ZK voting prover if: ${{ matrix.kind == 'lake' && matrix.zk_voting }} run: lake exe Apps.ZKVoting.Prover + - name: Run Ix.Tc unit, parity, and regression tests + if: ${{ matrix.kind == 'tc' }} + run: | + lake test --wfail -- tc-unit + lake test --wfail -- --ignored ${{ matrix.test_args }} + + valgrind: + name: Valgrind FFI + needs: prepare + if: ${{ github.event_name == 'merge_group' || github.event_name == 'issue_comment' }} + # Valgrind cannot decode the shared baseline's AVX-512, so its portable + # build artifacts must not share a cache volume with the other test jobs. + runs-on: + - nscloud-ubuntu-26.04-amd64-8x16-with-cache + - nscloud-cache-size-50gb + - nscloud-cache-tag-argumentcomputer-ix-valgrind + 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 }} + persist-credentials: false + + - name: Verify test revision + env: + TEST_REVISION: ${{ needs.prepare.outputs.revision }} + run: | + checked_out=$(git rev-parse HEAD) + if [ "$checked_out" != "$TEST_REVISION" ]; then + echo "::error::PR merge ref changed before the run started; comment !merge-tests again" + exit 1 + fi + + - uses: ./.github/actions/setup-rust-toolchain + with: + avx512-codegen: "false" + use-github-cache: "false" + - uses: ./.github/actions/setup-lake-cache + - uses: leanprover/lean-action@v1 + with: + auto-config: false + use-github-cache: false + + - name: Run FFI tests normally + run: lake test --wfail -- ffi + - name: Install valgrind - if: ${{ matrix.kind == 'valgrind' }} run: | - # Some warpbuild images ship a mirrorlist with an unreachable - # azure.archive.ubuntu.com entry, causing apt-get update to stall indefinitely. - sudo sed -i '/azure\.archive\.ubuntu\.com/d' /etc/apt/apt-mirrors.txt 2>/dev/null || true sudo apt-get update sudo apt-get install -y valgrind + - name: Run tests under valgrind - if: ${{ matrix.kind == 'valgrind' }} run: | valgrind \ --leak-check=full \ @@ -147,30 +220,56 @@ jobs: --suppressions=.github/valgrind.supp \ .lake/build/bin/IxTests ffi - - name: Check Ix.Tc exported theorem trust manifest - if: ${{ matrix.kind == 'tc' }} - run: lake build Ix.Tc.Verify.Audit.Completed Ix.Tc.Verify.Audit.Conditional Ix.Tc.Verify.Audit.Statements - - name: Build Ix.Tc formal verification - if: ${{ matrix.kind == 'tc' }} - run: lake build IxTcVerify - - name: Check Ix.Tc verification sorry frontier - if: ${{ matrix.kind == 'tc' }} - run: lake build Ix.Tc.Verify.Audit.SorryFrontier - - name: Test Ix.Tc unit and adversarial fixtures - if: ${{ matrix.kind == 'tc' }} - run: lake test --wfail -- tc-unit - - name: Run Ix.Tc ignored tests - if: ${{ matrix.kind == 'tc' }} - run: lake test --wfail -- ${{ matrix.test_args }} - merge-tests-result: name: Merge tests - if: ${{ always() }} - needs: merge-tests + if: >- + always() && + (github.event_name != 'issue_comment' || needs.prepare.result != 'skipped') + needs: [prepare, merge-tests, valgrind] runs-on: ubuntu-latest + permissions: + issues: write + pull-requests: write steps: + - name: Compose final comment + if: github.event_name == 'issue_comment' && needs.prepare.result == 'success' + env: + MERGE_SHA: ${{ needs.prepare.outputs.revision }} + PR_NUMBER: ${{ needs.prepare.outputs.pr }} + TEST_RESULT: ${{ needs.merge-tests.result }} + VALGRIND_RESULT: ${{ needs.valgrind.result }} + run: | + if [ "$TEST_RESULT" = success ] && [ "$VALGRIND_RESULT" = success ]; then + heading="## ✅ Merge tests passed" + summary="All ignored test partitions passed" + elif [ "$TEST_RESULT" = cancelled ] || [ "$VALGRIND_RESULT" = cancelled ]; then + heading="## ⚪ Merge tests cancelled" + summary="The ignored test run was cancelled" + else + heading="## ❌ Merge tests failed" + summary="At least one ignored test partition failed" + fi + { + echo "$heading" + echo + echo "$summary for PR #$PR_NUMBER at \`${MERGE_SHA:0:7}\`." + echo + echo "[Workflow logs](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})" + } > comment-body.md + + - name: Update result comment + if: github.event_name == 'issue_comment' && needs.prepare.result == 'success' + uses: peter-evans/create-or-update-comment@v5 + with: + token: ${{ github.token }} + issue-number: ${{ needs.prepare.outputs.pr }} + comment-id: ${{ needs.prepare.outputs.comment-id }} + edit-mode: replace + body-path: comment-body.md + - name: Propagate merge-test failure if: >- - github.event_name == 'merge_group' && - needs.merge-tests.result != 'success' + needs.prepare.result != 'success' || + needs.merge-tests.result != 'success' || + needs.valgrind.result != 'success' run: exit 1 diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml index 51b38c363..c6f291789 100644 --- a/.github/workflows/nix.yml +++ b/.github/workflows/nix.yml @@ -13,12 +13,19 @@ concurrency: cancel-in-progress: true jobs: - # Runs Lean tests via Nix nix-test: name: Nix Tests - runs-on: warp-ubuntu-latest-x64-16x + runs-on: + - nscloud-ubuntu-26.04-amd64-16x32-with-cache + - nscloud-cache-size-100gb + - nscloud-cache-tag-argumentcomputer-ix-nix steps: - uses: actions/checkout@v7 + - uses: ./.github/actions/setup-lake-cache + with: + cache-modes: | + nix + rust - uses: cachix/install-nix-action@v31 with: nix_path: nixpkgs=channel:nixos-unstable @@ -37,23 +44,7 @@ jobs: - run: nix run .#ix -- --help # A single invocation lets Nix schedule independent checks concurrently. - run: nix flake check --print-build-logs --accept-flake-config - - # Tests Nix devShell support on Ubuntu - nix-devshell: - name: Nix devShell Tests - runs-on: warp-ubuntu-latest-x64-8x - steps: - - uses: actions/checkout@v7 - - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixos-unstable - github_access_token: ${{ secrets.GITHUB_TOKEN }} - - uses: cachix/cachix-action@v17 - with: - name: argumentcomputer - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - - uses: ./.github/actions/authenticate-github-fetches - # Builds and runs tests using Lake as a Nix package + # Run the real build and test commands inside the development environment. - run: nix develop --accept-flake-config --command bash -c "lake build && lake test" # Realize the zkVM shells so they're verified and pushed to the cache, # and smoke-test each shell's toolchain entrypoint. diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml index f2d50dc64..57dea131f 100644 --- a/.github/workflows/update.yml +++ b/.github/workflows/update.yml @@ -14,15 +14,7 @@ jobs: update: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v6 - - # Mint a token from the GitHub App so the opened PR triggers CI; pushes - # made with GITHUB_TOKEN do not. Same App as the org repo-sync workflows. - - uses: actions/create-github-app-token@v3 - id: app-token - with: - client-id: ${{ secrets.TOKEN_APP_ID }} - private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }} + - uses: actions/checkout@v7 # `dev` carries the fork's bump_mode/release_channel support; `main` only # mirrors upstream, which silently ignores these inputs. A PR is opened @@ -39,4 +31,4 @@ jobs: lake_package_directory: ". Benchmarks/**" bump_mode: pinned-tags pr: true - token: ${{ steps.app-token.outputs.token }} + token: ${{ secrets.GITHUB_TOKEN }} diff --git a/Ix/Cli/BenchCmd.lean b/Ix/Cli/BenchCmd.lean index 139154378..ac40b52b2 100644 --- a/Ix/Cli/BenchCmd.lean +++ b/Ix/Cli/BenchCmd.lean @@ -312,6 +312,7 @@ def backendSpecs : List BackendSpec := [ ("check-time", "0.10", "_"), ("throughput", "_", "0.10"), ("peak-rss", "0.10", "_")] }, { name := "zisk", defaultMode := "execute", inputs := .perConstant, + disabled := some "CI benchmarks disabled; covered by build/execute integration jobs", testbeds := [("execute", "zisk-check-execute-x64-32x")], metrics := [("execute", ["execute-time", "throughput", "peak-rss", "cycles", "constants", "shards"])], @@ -323,7 +324,7 @@ def backendSpecs : List BackendSpec := [ ("execute-time", "0.10", "_"), ("peak-rss", "0.10", "_"), ("throughput", "_", "0.10")] }, { name := "sp1", defaultMode := "execute", inputs := .perConstant, - disabled := some "execute run too slow for per-push CI; re-enable here once trimmed", + disabled := some "CI benchmarks disabled; covered by build/execute integration jobs", testbeds := [("execute", "sp1-check-execute-x64-32x")], metrics := [("execute", ["execute-time", "throughput", "peak-rss", "cycles"])], diff --git a/Ix/Cli/BenchReport.lean b/Ix/Cli/BenchReport.lean index f9a2aa3dd..e6c9ec7ed 100644 --- a/Ix/Cli/BenchReport.lean +++ b/Ix/Cli/BenchReport.lean @@ -652,12 +652,6 @@ def runCompareCmd (p : Cli.Parsed) : IO UInt32 := do && (← System.FilePath.pathExists ⟨prAttrib⟩) then table := table ++ "\n\n" ++ (← renderPerConstMovers mainAttrib prAttrib baseLabel) - if let some path := (p.flag? "warning-file").map (·.as! String) then - if ← System.FilePath.pathExists ⟨path⟩ then - let warning := (← IO.FS.readFile path).trimAscii.toString - if !warning.isEmpty then - let lines := (warning.splitOn "\n").map fun line => "> " ++ line - table := "> [!WARNING]\n" ++ "\n".intercalate lines ++ "\n\n" ++ table match p.flag? "out" with | some f => IO.FS.writeFile (f.as! String) (table ++ "\n") | none => IO.println table @@ -952,7 +946,7 @@ def parseError (msg : String) : IO UInt32 := do Grammar (an unknown command-line token, or an unknown env in BENCH_ENVS, rejects the command — exit 2 and a `parse-error` output): - !benchmark ([aiur] [zisk] [sp1] [ooc] [compile] | all) + !benchmark ([aiur] [ooc] [compile] [decompile] | all) [execute] [fresh] [KEY=VALUE …] BENCH_ENVS=InitStd,Mathlib (case-insensitive, any registry env; defaults to every env for the @@ -1026,7 +1020,7 @@ def runParseCmd (p : Cli.Parsed) : IO UInt32 := do freshFlag := true continue let requested := if t == "all" - then Ix.Cli.BenchCmd.backendSpecs + then Ix.Cli.BenchCmd.backendSpecs.filter (·.disabled.isNone) else (Ix.Cli.BenchCmd.findBackend t).toList -- Everything after `!benchmark` on the command line must parse: a -- typo'd backend silently running the default would report numbers @@ -1034,7 +1028,8 @@ def runParseCmd (p : Cli.Parsed) : IO UInt32 := do if requested.isEmpty then return ← parseError s!"unknown token `{t}` in the benchmark command \ (expected a backend — \ - {", ".intercalate (Ix.Cli.BenchCmd.backendSpecs.map (·.name))} — \ + {", ".intercalate ((Ix.Cli.BenchCmd.backendSpecs.filter + (·.disabled.isNone)).map (·.name))} — \ or `all` / `execute` / `fresh`)" for b in requested do if b.disabled.isSome then @@ -1042,6 +1037,10 @@ def runParseCmd (p : Cli.Parsed) : IO UInt32 := do else if backends.all (·.name != b.name) then backends := backends.push b if backends.isEmpty then + if !skipped.isEmpty then + let reasons := ", ".intercalate <| skipped.toList.map fun b => + s!"{b.name} ({b.disabled.getD "disabled in CI"})" + return ← parseError s!"no requested benchmark backend is enabled in CI: {reasons}" backends := (Ix.Cli.BenchCmd.findBackend "aiur").toList.toArray -- KEY=VALUE config: the inline command-line tokens (strict — an @@ -1253,7 +1252,6 @@ def benchCompareCmd : Cli.Cmd := `[Cli| title : String; "Table title (default: derived from the run)" "base-source" : String; "Where the base side came from, for the title" "base-label" : String; "Name the base side in headers (default: main)" - "warning-file" : String; "Markdown warning file to prepend when present" out : String; "Write the table here instead of stdout" ] diff --git a/Ix/Tc/Verify/Audit/Basic.lean b/Ix/Tc/Verify/Audit/Basic.lean index 54f1c2f61..177558f74 100644 --- a/Ix/Tc/Verify/Audit/Basic.lean +++ b/Ix/Tc/Verify/Audit/Basic.lean @@ -78,33 +78,48 @@ private def directConstants : ConstantInfo → Array Name namespace DependencyAudit +structure Cache where + dependencies : NameMap (Array Name) := {} + structure State where + cache : Cache := {} visited : NameSet := {} - names : Array Name := #[] origins : Array Name := #[] + pendingDependency? : Option Name := none abbrev M := ReaderT Environment (StateM State) +/-- Cache direct references across manifest roots, which commonly share large +proof subgraphs. -/ +private def dependencies (declName : Name) : M (Array Name) := do + let state ← get + if let some dependencies := state.cache.dependencies.find? declName then + return dependencies + let env ← read + let dependencies := match env.checked.get.find? declName with + | none => #[] + | some info => directConstants info + modify fun s => + { s with cache := { dependencies := s.cache.dependencies.insert declName dependencies } } + return dependencies + /-- Traverse the checked kernel environment and record each reachable declaration whose type or value directly mentions `sorryAx`. -/ partial def visit (declName : Name) : M Unit := do let state ← get unless state.visited.contains declName do - modify fun s => - { s with - visited := s.visited.insert declName - names := s.names.push declName } - let env ← read - match env.checked.get.find? declName with - | none => pure () - | some info => - let dependencies := directConstants info - if declName != ``sorryAx && dependencies.contains ``sorryAx then - modify fun s => { s with origins := s.origins.push declName } - dependencies.forM visit - -def collect (env : Environment) (root : Name) : State := - let (_, state) := ((visit root).run env).run {} + modify fun s => { s with visited := s.visited.insert declName } + if state.pendingDependency?.isNone && + declName.toString.startsWith "Ix.Tc.Upstream.Pending." then + modify fun s => { s with pendingDependency? := some declName } + let dependencies ← dependencies declName + if declName != ``sorryAx && dependencies.contains ``sorryAx then + modify fun s => { s with origins := s.origins.push declName } + dependencies.forM visit + +def collect (env : Environment) (root : Name) (cache : Cache) : State := + let initial : State := { cache := cache } + let (_, state) := ((visit root).run env).run initial state end DependencyAudit @@ -144,7 +159,8 @@ private def expectedAxioms (allowance : RootAllowance) : Array Lean.Name := sortNames <| if allowance.sorryOrigins.isEmpty then expected else expected.push ``sorryAx -private def checkOne (allowance : RootAllowance) : CommandElabM Unit := do +private def checkOne (dependencyCache : DependencyAudit.Cache) + (allowance : RootAllowance) : CommandElabM DependencyAudit.Cache := do validateCategories allowance let env ← getEnv unless env.contains allowance.root do @@ -164,7 +180,7 @@ private def checkOne (allowance : RootAllowance) : CommandElabM Unit := do -- Origin and architectural-quarantine checks consume the same transitive -- dependency graph. Keep one exact traversal per root: large generated -- recursor proofs make two independent walks unnecessarily expensive. - let dependencyAudit := DependencyAudit.collect env allowance.root + let dependencyAudit := DependencyAudit.collect env allowance.root dependencyCache let actualOrigins := sortNames dependencyAudit.origins let expectedOrigins := sortNames allowance.sorryOrigins unless actualOrigins == expectedOrigins do @@ -177,23 +193,24 @@ private def checkOne (allowance : RootAllowance) : CommandElabM Unit := do -- helper definitions from the quarantine module: otherwise replacing a -- pending witness could silently change the completed proof surface. if allowance.pendingAxioms.isEmpty then - for dependency in dependencyAudit.names do - if dependency.toString.startsWith "Ix.Tc.Upstream.Pending." then - throwError m!"{allowance.root}: unconditional root reaches quarantined dependency {dependency}" + if let some dependency := dependencyAudit.pendingDependency? then + throwError m!"{allowance.root}: unconditional root reaches quarantined dependency {dependency}" for forbidden in allowance.forbiddenDependencies do - if dependencyAudit.names.contains forbidden then + if dependencyAudit.visited.contains forbidden then throwError m!"{allowance.root}: forbidden transitive dependency {forbidden}" + return dependencyAudit.cache /-- Check a complete executable trust manifest. Duplicate roots are rejected instead of being silently audited twice. -/ def check (allowances : Array RootAllowance) : CommandElabM Unit := do let mut roots : NameSet := {} + let mut dependencyCache : DependencyAudit.Cache := {} for allowance in allowances do if roots.contains allowance.root then throwError m!"duplicate axiom-audit root: {allowance.root}" roots := roots.insert allowance.root - checkOne allowance + dependencyCache ← checkOne dependencyCache allowance logInfo m!"Ix.Tc verification trust audit passed for {allowances.size} theorem roots" end Ix.Tc.Verify.Audit diff --git a/Tests/Ix/Tc/Roundtrip.lean b/Tests/Ix/Tc/Roundtrip.lean index 44a990b5b..f46d9d92c 100644 --- a/Tests/Ix/Tc/Roundtrip.lean +++ b/Tests/Ix/Tc/Roundtrip.lean @@ -205,22 +205,6 @@ def unitTests : List TestSeq := [fixtureTests, negativeTests] /-! ### Rust-compiled closures (`tc-roundtrip`, ignored) -/ -/-- Compile a seed closure through the Rust compiler and roundtrip every - constant of the resulting env. -/ -def roundtripOnSeeds (leanEnv : Lean.Environment) (label : String) - (seeds : List Lean.Name) : IO (Nat × Option String) := do - let consts := Tests.Tc.AnonDiff.closureOf leanEnv seeds - if consts.isEmpty then - return (0, some s!"empty closure for {seeds}") - let dir ← IO.FS.createTempDir - let path := dir / s!"tc-roundtrip-{label}.ixe" - let _ ← Ix.CompileM.rsCompileEnvBytesFFI consts path.toString true - let bytes ← IO.FS.readBinFile path - IO.FS.removeDirAll dir - match Ixon.deEnvAnon bytes with - | .error e => return (0, some s!"deEnvAnon failed: {e}") - | .ok ixonEnv => return roundtripAll ixonEnv - def seedSets : List (String × List Lean.Name) := Tests.Tc.AnonDiff.seedSets ++ [ ("inductives-recursors", @@ -250,35 +234,6 @@ def seedSets : List (String × List Lean.Name) := `Tests.Ix.Compile.LevelSpellings.wfTwo, `Tests.Ix.Compile.LevelSpellings.wfTwoEqDef]) ] -def closureSuite : TestSeq := Id.run do - let mut ts : TestSeq := .done - for (label, seeds) in seedSets do - ts := ts ++ .individualIO s!"roundtrip closure: {label}" none (do - let env ← Tests.Tc.Roundtrip.fixtureEnv - let (rows, err?) ← roundtripOnSeeds env label seeds - return (err?.isNone, rows, 0, err?)) .done - return ts - -/-- Whole-environment roundtrip: compile the ENTIRE current Lean env through - the Rust compiler and roundtrip every constant of the result — the - direct analog of the Rust `kernel-ixon-roundtrip`'s input scope. For - external `.ixe` files (e.g. `compilemathlib.ixe`), use - `ix roundtrip-tc ` instead. -/ -def wholeEnvSuite : TestSeq := - .individualIO "roundtrip whole get_env environment" none (do - let leanEnv ← Tests.Tc.Roundtrip.fixtureEnv - let consts := leanEnv.constants.toList - let dir ← IO.FS.createTempDir - let path := dir / "tc-roundtrip-whole-env.ixe" - let _ ← Ix.CompileM.rsCompileEnvBytesFFI consts path.toString true - let bytes ← IO.FS.readBinFile path - IO.FS.removeDirAll dir - match Ixon.deEnvAnon bytes with - | .error e => return (false, 0, 0, some s!"deEnvAnon failed: {e}") - | .ok ixonEnv => - let (rows, err?) := roundtripAll ixonEnv - return (err?.isNone, rows, 0, err?)) .done - /-! ### Meta roundtrip (kernel → Lean, `compare_envs` semantics) The full-fidelity half: pure-parse the Rust-compiled env, meta-ingress the @@ -292,55 +247,77 @@ names are informational `notFound`; aux-rewritten entries (`original.isSome`) are skipped with a count (their anon-structural fidelity is covered by the anon roundtrip above). -/ -/-- Compile `consts` through the Rust compiler and run the shared meta - roundtrip driver (`Ix.Tc.metaRoundtripEnv`) against `leanEnv`. -/ -def metaRoundtripOn (leanEnv : Lean.Environment) (label : String) +/-- Run both roundtrip modes over one Rust compilation. Anon and meta parsing + consume the same immutable bytes, so compiling each fixture twice cannot + add coverage. -/ +def roundtripOn (leanEnv : Lean.Environment) (label : String) (consts : List (Lean.Name × Lean.ConstantInfo)) : - IO (Ix.Tc.MetaRoundtripReport × Option String) := do + IO (Nat × Ix.Tc.MetaRoundtripReport × Option String) := do + if consts.isEmpty then + return (0, {}, some "empty constant closure") let dir ← IO.FS.createTempDir - let path := dir / s!"tc-meta-roundtrip-{label}.ixe" + let path := dir / s!"tc-roundtrip-{label}.ixe" let _ ← Ix.CompileM.rsCompileEnvBytesFFI consts path.toString true let bytes ← IO.FS.readBinFile path IO.FS.removeDirAll dir - let ixonEnv ← match Ixon.deEnv bytes with - | .ok env => pure env - | .error e => return ({}, some s!"pure deEnv failed: {e}") - match metaRoundtripEnv leanEnv ixonEnv with - | .error e => return ({}, some e) - | .ok report => - if report.errorCount == 0 then - return (report, none) - else - let shown := report.errors.toSubarray 0 (min 5 report.errors.size) - |>.toArray - let msgs := shown.map fun (n, m) => s!"{n}: {m}" - return (report, - some s!"{report.errorCount} comparison error(s); first: \ - {String.intercalate " | " msgs.toList}") - -def metaClosureSuite : TestSeq := Id.run do - let mut ts : TestSeq := .done - for (label, seeds) in seedSets do - ts := ts ++ .individualIO s!"meta roundtrip closure: {label}" none (do - let env ← Tests.Tc.Roundtrip.fixtureEnv - let consts := Tests.Tc.AnonDiff.closureOf env seeds - let (report, err?) ← metaRoundtripOn env label consts - return (err?.isNone, report.checked, 0, err?)) .done - return ts - -/-- The centerpiece: meta roundtrip of the WHOLE current Lean env. -/ -def metaWholeEnvSuite : TestSeq := - .individualIO "meta roundtrip whole get_env environment" none (do + let (anonRows, anonErr?) := + match Ixon.deEnvAnon bytes with + | .error e => (0, some s!"deEnvAnon failed: {e}") + | .ok ixonEnv => roundtripAll ixonEnv + let (metaReport, metaErr?) := + match Ixon.deEnv bytes with + | .error e => (({} : Ix.Tc.MetaRoundtripReport), some s!"pure deEnv failed: {e}") + | .ok ixonEnv => + match metaRoundtripEnv leanEnv ixonEnv with + | .error e => (({} : Ix.Tc.MetaRoundtripReport), some e) + | .ok report => + if report.errorCount == 0 then + (report, none) + else + let shown : Array (Ix.Name × String) := + report.errors.toSubarray 0 (min 5 report.errors.size) |>.toArray + let msgs := shown.map fun (error : Ix.Name × String) => + s!"{error.1}: {error.2}" + (report, some s!"{report.errorCount} comparison error(s); first: \ + {String.intercalate " | " msgs.toList}") + let err? := match anonErr?, metaErr? with + | none, none => none + | some e, none => some s!"anon: {e}" + | none, some e => some s!"meta: {e}" + | some anon, some metaErr => some s!"anon: {anon}; meta: {metaErr}" + return (anonRows, metaReport, err?) + +/-- Load the fixture environment once, then check every focused closure and + the whole environment. Loading the same olean graph separately for each + closure is pure setup duplication. External `.ixe` files use + `ix roundtrip-tc `. -/ +def integrationSuite : TestSeq := + .individualIO "anon/meta roundtrip closures and whole environment" none (do let leanEnv ← Tests.Tc.Roundtrip.fixtureEnv - let (report, err?) ← - metaRoundtripOn leanEnv "whole-env" leanEnv.constants.toList - IO.println s!"[tc-meta-roundtrip] checked {report.checked}, \ - notFound {report.notFound}, skippedAux {report.skippedAux}, \ - skippedSurgery {report.skippedSurgery}" - return (err?.isNone, report.checked, 0, err?)) .done + let mut checked := 0 + let mut errors : Array String := #[] + for (label, seeds) in seedSets do + let consts := Tests.Tc.AnonDiff.closureOf leanEnv seeds + let (anonRows, metaReport, err?) ← roundtripOn leanEnv label consts + checked := checked + anonRows + metaReport.checked + match err? with + | some e => errors := errors.push s!"{label}: {e}" + | none => + IO.println s!"[tc-roundtrip] {label}: anon {anonRows}, meta {metaReport.checked}" + let (anonRows, metaReport, err?) ← + roundtripOn leanEnv "whole-env" leanEnv.constants.toList + checked := checked + anonRows + metaReport.checked + if let some e := err? then + errors := errors.push s!"whole-env: {e}" + IO.println s!"[tc-meta-roundtrip] checked {metaReport.checked}, \ + notFound {metaReport.notFound}, skippedAux {metaReport.skippedAux}, \ + skippedSurgery {metaReport.skippedSurgery}" + let msg := if errors.isEmpty then none + else some (String.intercalate "\n" errors.toList) + return (errors.isEmpty, checked, 0, msg)) .done public def suite : List TestSeq := - [closureSuite, wholeEnvSuite, metaClosureSuite, metaWholeEnvSuite] + [integrationSuite] end diff --git a/docs/benchmarking.md b/docs/benchmarking.md index e5a566412..a02cd2ca4 100644 --- a/docs/benchmarking.md +++ b/docs/benchmarking.md @@ -1,8 +1,8 @@ # Benchmarking One orchestrator — `ix bench` — runs every benchmark cell, locally and in CI. -A **cell** is `(backend, env, mode)`, e.g. `zisk-InitStd-execute`. CI is a -thin wrapper: the same `ix bench run` you type in a terminal is what both +A **cell** is `(backend, env, mode)`, e.g. `ooc-InitStd-execute`. For backends +scheduled in CI, the same `ix bench run` you type in a terminal is what both workflows execute, so every CI number is reproducible on your machine. - **`!benchmark` PR comment** (`.github/workflows/bench-pr.yml`) — on demand, @@ -101,8 +101,8 @@ a PR tree and compare them — exactly what the PR workflow does. | backend | what it measures | tool | |---|---|---| | `aiur` | the Aiur proof pipeline, per constant: the `ixvm` stage proves the IxVM typecheck, the `fri-verifier` stage executes and proves the in-circuit multi-stark verifier over that fresh proof (the KZG stages fold in as they land, each with its own measure prefix), closed by the pipeline ledger (total-time, pipeline-throughput, pipeline-peak-rss). Each stage's measures carry its prefix (`ixvm-prove-time`, `fri-verifier-fft-cost`, …). The whole system runs under the recursion-tuned FRI parameters. A second mode, execute, is the fast Phase-1-only signal (fft-cost, execute-time, throughput, peak-rss) — unscheduled, local/on-demand only (`!benchmark aiur execute`). The direct `--recursive --join` diagnostic takes exactly two constants as singleton `CheckEnv` shards and appends one pair row carrying `join-{execute-time,fft-cost,prove-time,peak-rss,proof-size,verify-time}`; it remains unscheduled until a runner can carry W0. | `bench-typecheck --recursive` | -| `zisk` | ZisK VM execute: cycles, execute-time, throughput, peak-rss, constants (pre-shard closure count, same universe as aiur's), shards (the runtime-planned partition size; 1 when the closure fits) | `zisk-host` | -| `sp1` | SP1 VM execute (currently disabled in the registry) | `sp1-host` | +| `zisk` | ZisK VM execute: cycles, execute-time, throughput, peak-rss, constants (pre-shard closure count, same universe as aiur's), shards (the runtime-planned partition size; 1 when the closure fits). Available locally; benchmark CI is disabled. | `zisk-host` | +| `sp1` | SP1 VM execute. Available locally; benchmark CI is disabled. | `sp1-host` | | `ooc` | out-of-circuit Rust kernel: whole-env row + one full-closure row per constant (`check-time` wraps only the check — the env loads once, outside every row's timed window) | `ix check-rs --json` | | `lean4lean` | the reference Lean4-in-Lean4 kernel ([digama0/lean4lean](https://github.com/digama0/lean4lean), required by the lakefile at a pinned rev) — the external yardstick for the Ix kernels on the same libraries. Olean-driven (no `.ixe`): the whole-library row replays every module in the env's import closure through lean4lean, module-parallel (check-time, constants, throughput, peak-rss; tune parallelism with `LEAN_NUM_THREADS`), plus one full-closure row per constant (the name's transitive closure into a fresh kernel env), mirroring ooc's row shape. Registry-disabled for CI (no bencher testbed yet); `ix bench run --backend lean4lean` works locally regardless | `bench-lean4lean` | | `compile` | `ix compile .lean → .ixe`: compile-time, file-size, constants, throughput | `ix compile --json` | @@ -174,14 +174,14 @@ approach the ceiling, and a kill there means missing rows and a red cell. There are **no per-constant timeouts**; the job-level `timeout-minutes` is the only clock. -Every zisk constant runs as a closure-shard partition sized at bench +Every local zisk benchmark constant runs as a closure-shard partition sized at runtime: `ix shard extract` → `ix profile` → `ix shard` cut a manifest whose shard count comes from the planner's RAM budget (a closure that fits gets a one-shard plan), and one `--shard-plan` host run executes the shards sequentially, emitting the constant's row with per-shard -breakdowns. bench-main's compile job pre-cuts these artifacts -(`ix bench shard`) and ships them via cache; a zisk run cuts lazily when -they're absent, and falls back to the whole closure if the cut fails. +breakdowns. `ix bench shard` can pre-cut these artifacts; a zisk run cuts +lazily when they're absent and falls back to the whole closure if the cut +fails. ## Registry and constant set @@ -208,7 +208,7 @@ they're absent, and falls back to the whole closure if the cut fails. ## `!benchmark` grammar ``` -!benchmark ([aiur] [zisk] [sp1] [ooc] [compile] [decompile] | all) +!benchmark ([aiur] [ooc] [compile] [decompile] | all) [execute] [fresh] [KEY=VALUE …] BENCH_ENVS=InitStd,Mathlib # default InitStd (case-insensitive); a # compile-only request may name any registry @@ -258,9 +258,8 @@ untouched. **bench-main.yml**: `build` (compile `ix` + `bench-typecheck` once, cache by SHA) → `plan` (`ix bench ci matrix` → job matrices) + `compile` (per env: -`ix bench run --backend compile`, cache the `.ixe` and pre-cut zisk shards -separately) → -one `benchmark` job per remaining cell — aiur / zisk / ooc / decompile — +`ix bench run --backend compile`, cache the `.ixe`) → +one `benchmark` job per remaining cell — aiur / ooc / decompile — (each: restore caches, one `ix bench run … --ixe`, `ix bench bmf`, upload via `.github/actions/bencher-track`). A kernel rejection exits 3 and reddens the @@ -290,18 +289,14 @@ non-`main` base, whose `.ixe` can be restored from its earlier PR run); the comment body, unprivileged) → `comment` (posts it — the only job with a write token, running no PR code). Normal runs may seed the run artifacts from persistent head/base-SHA caches. `fresh` bypasses those caches and rebuilds -the measured products while retaining dependency caches. +the measured products while retaining dependency caches. Benchmark runners use +WarpCache for both workflow products and Cargo build artifacts. Every job that creates a timing row logs its CPU model, instruction set, -effective CPU count, affinity, and cgroup allocation. Because the benchmark -binaries use native codegen, their build jobs also record the build CPU and -carry that report inside the binary cache or run artifact; measurement jobs -print it next to their own host report. A cache entry created before this -provenance was introduced remains usable and is reported as having an unknown -build CPU. The exact `lscpu` model name is compared; a difference (or missing -build provenance) is rendered as a warning in that cell's PR comment table. -This is diagnostic only: the CPU model does not participate in cache keys, and -only an explicit `fresh` request bypasses the measured-product caches. +effective CPU count, affinity, and cgroup allocation directly in the Actions +logs. The `!benchmark` comment also includes a compact CPU model, effective +vCPU count, and total RAM summary. This is diagnostic only: CPU information +does not participate in cache keys or benchmark results. ## Palomar compatibility corpus @@ -350,10 +345,10 @@ the same artifacts. ## Not yet covered -- **zkVM prove** — the hosts prove, but CI has no GPU runner; cells are - execute-only. -- **sp1** — disabled in the registry (execute too slow per push); - re-enable it there and it returns to the matrices and the parser. +- **Zisk and SP1 benchmark cells** — intentionally disabled in benchmark CI; + regular CI retains their build and keyless-execution integration jobs. +- **zkVM prove** — the hosts prove, but local proving requires suitable GPU + infrastructure. - **aiur prove numbers for the biggest closures** — every constant in the shared set runs the full pipeline, but the largest ones exceed the CI host's RAM ceiling and land as honest `oom` rows, which never upload From 8488a6f9e638131ad90b9c85a64ba2b06d2fd4b7 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 3 Sep 2026 22:49:36 -0400 Subject: [PATCH 2/9] ci: refresh workflow documentation --- .../authenticate-github-fetches/action.yml | 12 ++++----- .github/actions/bencher-track/action.yml | 2 +- .github/actions/install-sp1/action.yml | 4 +-- .github/actions/install-zisk/action.yml | 12 ++++----- .github/actions/setup-lake-cache/action.yml | 10 ++++--- .../actions/setup-rust-toolchain/action.yml | 12 ++++----- .github/workflows/bench-main.yml | 15 ++++++----- .github/workflows/bench-pr.yml | 6 ++--- .github/workflows/bencher-plots.yml | 4 +-- .github/workflows/ci.yml | 6 ++--- docs/benchmarking.md | 27 ++++++++++--------- 11 files changed, 58 insertions(+), 52 deletions(-) diff --git a/.github/actions/authenticate-github-fetches/action.yml b/.github/actions/authenticate-github-fetches/action.yml index 72d60e811..e9e6cbd17 100644 --- a/.github/actions/authenticate-github-fetches/action.yml +++ b/.github/actions/authenticate-github-fetches/action.yml @@ -1,12 +1,12 @@ name: Authenticate git fetches of GitHub repos description: >- Rewrite github.com URLs so git-CLI fetches carry the job's ephemeral token. - GitHub throttles anonymous git HTTPS traffic per source IP, and Warp runners - share egress IPs across tenants, so unauthenticated clones of public repos - can fail with a 401 ("could not read Username"). The rewrite covers every - fetch that goes through the git CLI: Lake dependency clones, Nix's eval-time - `builtins.fetchGit`, script clones, and cargo git dependencies when - CARGO_NET_GIT_FETCH_WITH_CLI is set. + GitHub throttles anonymous git HTTPS traffic per source IP, and managed + runner pools can share egress IPs across tenants, so unauthenticated clones + of public repos can fail with a 401 ("could not read Username"). The rewrite + covers every fetch that goes through the git CLI: Lake dependency clones, + Nix's eval-time `builtins.fetchGit`, script clones, and cargo git dependencies + when CARGO_NET_GIT_FETCH_WITH_CLI is set. runs: using: composite diff --git a/.github/actions/bencher-track/action.yml b/.github/actions/bencher-track/action.yml index 6de6c160d..85c6e9c36 100644 --- a/.github/actions/bencher-track/action.yml +++ b/.github/actions/bencher-track/action.yml @@ -13,7 +13,7 @@ inputs: description: Bencher testbed slug. required: true workload: - description: Workload key for the `refs/bencher/` anchor (the backend testbed minus its runner-arch suffix, e.g. zisk-check-execute). + description: Workload key for the `refs/bencher/` anchor (the backend testbed minus its runner-arch suffix, e.g. ooc-check). required: true file: description: Bencher Metric Format JSON file to upload. diff --git a/.github/actions/install-sp1/action.yml b/.github/actions/install-sp1/action.yml index 5f820cd03..0e386423d 100644 --- a/.github/actions/install-sp1/action.yml +++ b/.github/actions/install-sp1/action.yml @@ -13,11 +13,11 @@ runs: - name: Install system build deps shell: bash run: | - # Some warpbuild images ship an unreachable azure mirror that hangs + # Some runner images ship an unreachable Azure mirror that hangs # `apt-get update`; drop it first (no-op elsewhere). sudo sed -i '/azure\.archive\.ubuntu\.com/d' /etc/apt/apt-mirrors.txt 2>/dev/null || true export DEBIAN_FRONTEND=noninteractive - # The Ubuntu EC2 mirrors sporadically 502 / throttle on these large + # Ubuntu package mirrors sporadically 502 / throttle on these large # fetches (qemu-system alone pulls hundreds of MB), so retry the whole # update+install: `Acquire::Retries` absorbs single-download blips and # `--fix-missing` resumes a partially fetched set. diff --git a/.github/actions/install-zisk/action.yml b/.github/actions/install-zisk/action.yml index 40ef7b4be..35719d2f0 100644 --- a/.github/actions/install-zisk/action.yml +++ b/.github/actions/install-zisk/action.yml @@ -24,11 +24,11 @@ runs: - name: Install system build deps shell: bash run: | - # Some warpbuild images ship an unreachable azure mirror that hangs + # Some runner images ship an unreachable Azure mirror that hangs # `apt-get update`; drop it first (no-op elsewhere). sudo sed -i '/azure\.archive\.ubuntu\.com/d' /etc/apt/apt-mirrors.txt 2>/dev/null || true export DEBIAN_FRONTEND=noninteractive - # The Ubuntu EC2 mirrors sporadically 502 / throttle on these large + # Ubuntu package mirrors sporadically 502 / throttle on these large # fetches (qemu-system alone pulls hundreds of MB), so retry the whole # update+install: `Acquire::Retries` absorbs single-download blips and # `--fix-missing` resumes a partially fetched set. @@ -90,7 +90,7 @@ runs: "$HOME/.zisk/bin/cargo-zisk" toolchain install --toolchain-version zisk-0.5.1 echo "$HOME/.zisk/bin" >> "$GITHUB_PATH" # Pre-build the proofman C++ sys crate ALONE so its build script runs - # exactly once before any parallel zisk-host build. zisk-host pulls + # exactly once before zisk-host's parallel Cargo build. zisk-host pulls # zisk-sdk as both a dependency and a build-dependency, so cargo compiles # proofman-starks-lib-c as two units whose build scripts can run # CONCURRENTLY — and both run `make` inside the SHARED @@ -117,9 +117,9 @@ runs: # reuse a stale key. `aws s3 cp` (multipart, no creds — public bucket) # holds throughput steady where a single-stream `curl` swings by an # order of magnitude; `curl` is the fallback for hosts without the AWS - # CLI. Deliberately NOT actions/cache'd: the multi-GB tarball would crowd - # the repo's cache quota, while its public S3 source supports multipart - # downloads directly. + # CLI. Deliberately omitted from the shared runner cache: the multi-GB + # tarball would crowd build artifacts, while its public S3 source supports + # multipart downloads directly. - name: Fetch proving key from S3, extract, regenerate const-trees if: inputs.proving-key == 'true' shell: bash diff --git a/.github/actions/setup-lake-cache/action.yml b/.github/actions/setup-lake-cache/action.yml index 405aa846e..715259ff5 100644 --- a/.github/actions/setup-lake-cache/action.yml +++ b/.github/actions/setup-lake-cache/action.yml @@ -1,18 +1,20 @@ name: Set up Namespace build cache -description: Mount the shared Namespace cache for Lake, Cargo, and optional tool caches +description: >- + Mount .lake, Namespace's built-in cache presets, and optional build + directories on the shared cache volume. inputs: cache-modes: - description: Namespace cache modes to enable + description: Built-in Namespace cache presets to mount (for example, rust or nix) required: false default: rust additional-paths: - description: Additional paths to mount on the Namespace cache volume + description: Paths to mount in addition to the repository's .lake directory required: false outputs: cache-hit: - description: Whether Namespace restored the build cache + description: Whether Namespace restored a prior cache volume value: ${{ steps.cache.outputs.cache-hit }} runs: diff --git a/.github/actions/setup-rust-toolchain/action.yml b/.github/actions/setup-rust-toolchain/action.yml index 0accaf5c4..56bd63b64 100644 --- a/.github/actions/setup-rust-toolchain/action.yml +++ b/.github/actions/setup-rust-toolchain/action.yml @@ -8,7 +8,7 @@ inputs: description: Cargo workspaces to cache required: false use-github-cache: - description: Enable the setup action's Cargo cache + description: Enable Cargo artifact caching through the selected provider required: false default: "true" cache-provider: @@ -54,11 +54,11 @@ runs: # feature set contains the other's, so `-Ctarget-cpu=native` is not # portable across the fleet: Zen 5 enables SSE4A, which LLVM emits (as # INSERTQ, in witness generation) and Intel traps on with #UD. Pin the - # measured intersection instead. x86-64-v4 covers every AVX-512 subset Plonky3 - # uses; +avx512vbmi2 keeps its VPSHRDQ interleave and +gfni keeps LLVM's - # byte-shift lowering. blake3 selects its kernels via CPUID at runtime - # and is unaffected. Pinning also makes codegen host-independent, so the - # cache key below is sound and main-vs-PR timings stay comparable. + # measured intersection instead. x86-64-v4 covers every AVX-512 subset + # Plonky3 uses; +avx512vbmi2 keeps its VPSHRDQ interleave and +gfni keeps + # LLVM's byte-shift lowering. blake3 selects its kernels via CPUID at + # runtime and is unaffected. Pinning also makes codegen host-independent, + # so the cache key below is sound and main-vs-PR timings stay comparable. - name: Require the fleet's baseline CPU features if: inputs.avx512-codegen == 'true' shell: bash diff --git a/.github/workflows/bench-main.yml b/.github/workflows/bench-main.yml index c24afecbc..85dd183ff 100644 --- a/.github/workflows/bench-main.yml +++ b/.github/workflows/bench-main.yml @@ -3,16 +3,17 @@ name: Benchmark main # Benchmarks every push to main and uploads the results to bencher.dev. # Each measurement is one `ix bench run` with a (backend, env, mode) # parameter combination — the same command you can run locally, and the -# same one the !benchmark PR workflow uses. Three stages: +# same one the !benchmark PR workflow uses. Four job roles: # -# 1. plan — `ix bench ci matrix` prints the list of parameter +# 1. build — compiles and caches `ix` and `bench-typecheck` once. +# 2. plan — `ix bench ci matrix` prints the list of parameter # combinations to run. The list comes from the registry # (Ix/Cli/BenchCmd.lean) and each entry already carries # its bencher testbed, workload, and threshold flags, so # this file hardcodes none of that. -# 2. compile — compiles each Lean env to a `.ixe` file (this IS the -# compile benchmark) and caches the file for stage 3. -# 3. benchmark — one job per remaining entry: restore the `.ixe` and +# 3. compile — compiles each Lean env to a `.ixe` file (this IS the +# compile benchmark) and caches the file for `benchmark`. +# 4. benchmark — one job per remaining entry: restore the `.ixe` and # run the entry's backend over it (aiur, ooc, decompile). # # Each entry uploads to its own bencher testbed/workload, so a threshold @@ -84,8 +85,8 @@ jobs: # job; only the benchmark job waits on it. plan: needs: build - # Native target features may occur anywhere in `ix`, including this - # registry-only subcommand, so keep it on the Warp x64 runner fleet. + # The restored `ix` targets the fleet's fixed AVX-512 baseline, so keep + # even this registry-only invocation on compatible Warp x64 hardware. runs-on: warp-ubuntu-latest-x64-8x outputs: matrix: ${{ steps.matrix.outputs.matrix }} diff --git a/.github/workflows/bench-pr.yml b/.github/workflows/bench-pr.yml index 64e6b84db..c7eef5abe 100644 --- a/.github/workflows/bench-pr.yml +++ b/.github/workflows/bench-pr.yml @@ -651,7 +651,7 @@ jobs: # restored (otherwise the base side would need mathlib oleans that # only a full build fetches). Usable binaries go into # base/.lake/build/bin, where `ix bench run --repo base` finds them; - # a from-scratch base build puts them there natively. + # a from-scratch base build puts them there directly. - name: Resolve base binaries if: steps.decide.outputs.run-base == 'true' id: base-src @@ -814,8 +814,8 @@ jobs: # Assemble even when benchmark runs failed — the tables carry the ❌ # rows. Only the build job must have succeeded (it made the binaries). if: always() && needs.build.result == 'success' - # The report command uses the build job's native `ix`, so keep it on the - # Warp x64 runner fleet; report assembly does not need benchmark-scale RAM. + # The report command uses the build job's fixed-AVX-512 `ix`, so keep it on + # compatible Warp x64 hardware; report assembly needs little RAM. runs-on: warp-ubuntu-latest-x64-8x permissions: contents: read diff --git a/.github/workflows/bencher-plots.yml b/.github/workflows/bencher-plots.yml index 870776146..c63f4187f 100644 --- a/.github/workflows/bencher-plots.yml +++ b/.github/workflows/bencher-plots.yml @@ -24,8 +24,8 @@ permissions: jobs: sync-plots: - # The restored `ix` uses native target features selected on the benchmark - # build runner, even though this subcommand itself is pure Lean. + # The restored `ix` targets the benchmark fleet's fixed AVX-512 baseline, + # so even this pure-Lean subcommand needs compatible Warp x64 hardware. runs-on: warp-ubuntu-latest-x64-8x steps: - uses: actions/checkout@v7 diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index dbb252c3f..a6462edd1 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -66,8 +66,8 @@ jobs: if-no-files-found: error retention-days: 1 - # The primary test tier consumes the complete cache but cannot commit its - # local changes. The build job remains the sole shared-cache writer. + # The primary Lean test tier consumes the completed build cache read-only. + # Within this workflow, build and rust-test are the only ordered writers. lean-test: needs: build runs-on: @@ -90,7 +90,7 @@ jobs: run: lake test --wfail -- cli # Lake and root Cargo builds both use the repository's target directory, so - # these two writers share a volume in dependency order. Namespace volumes + # build and rust-test share a volume in dependency order. Namespace volumes # are last-write-wins; parallel zkVM writers use dedicated tags, while CUDA # consumes the primary cache without committing its feature-specific output. # Namespace's remote sccache could share compatible compilation units across diff --git a/docs/benchmarking.md b/docs/benchmarking.md index a02cd2ca4..1c6125e70 100644 --- a/docs/benchmarking.md +++ b/docs/benchmarking.md @@ -278,18 +278,21 @@ matching plots are kept, stale ones replaced, hand-pinned ones untouched. The sync also asserts every measure's canonical units (bencher auto-creates measures with placeholder units on first upload). -**bench-pr.yml**: `setup` (authorize the comment, resolve base/head SHAs) → -`build` (select or build the PR binaries, publish a run-scoped artifact, -then `ix bench ci parse`) → `compile` (one measured `ix compile` per env, -publishing a run-scoped `.ixe` + row artifact) → `benchmark` matrix (per cell: -download only those run artifacts; run the PR side; fetch main's numbers, -with a base-checkout run covering what bencher lacked (including every -non-`main` base, whose `.ixe` can be restored from its earlier PR run); -`ix bench compare` → table artifact) → `assemble` (`ix bench report` builds -the comment body, unprivileged) → `comment` (posts it — the only job with a -write token, running no PR code). Normal runs may seed the run artifacts from -persistent head/base-SHA caches. `fresh` bypasses those caches and rebuilds -the measured products while retaining dependency caches. Benchmark runners use +**bench-pr.yml**: `dispatch` (authorize the comment, resolve base/head SHAs, +then start the cache-writing run) → `build` (select or build the PR binaries, +publish a run-scoped artifact, then `ix bench ci parse`). `announce` posts the +initial running/error comment while `compile` runs one measured `ix compile` +per env and publishes a run-scoped `.ixe` + row artifact. The `benchmark` +matrix downloads only those run artifacts, runs the PR side, and fetches +main's numbers, with a base-checkout run covering what bencher lacked +(including every non-`main` +base, whose `.ixe` can be restored from its earlier PR run); `ix bench compare` +then publishes a table artifact. `assemble` runs `ix bench report` without +write privileges, and `comment` replaces the initial comment. Only `announce` +and `comment` hold write tokens, and neither checks out or runs PR code. Normal +runs may seed the run artifacts from persistent head/base-SHA caches. `fresh` +bypasses those caches and rebuilds the measured products while retaining +dependency caches. Benchmark runners use the fixed AVX-512 baseline and WarpCache for both workflow products and Cargo build artifacts. Every job that creates a timing row logs its CPU model, instruction set, From 002f7e57446a81fd580433f0ac71b4e963cf2cd7 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 3 Sep 2026 22:51:38 -0400 Subject: [PATCH 3/9] ci: bump Bencher action to v0.6.12 --- .github/workflows/bencher-plots.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/bencher-plots.yml b/.github/workflows/bencher-plots.yml index c63f4187f..25cf09b54 100644 --- a/.github/workflows/bencher-plots.yml +++ b/.github/workflows/bencher-plots.yml @@ -46,7 +46,7 @@ jobs: auto-config: false build: false use-github-cache: false - - uses: bencherdev/bencher@v0.6.11 + - uses: bencherdev/bencher@v0.6.12 # Plot create/delete needs those permissions on the ix project: a # user-scoped `bencher_user_*` key (the report-upload token the bench # workflows use may be run-scoped and unable to manage plots). From 288cfea79b59a9a92cf0562218574dde25a1954c Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 3 Sep 2026 22:55:32 -0400 Subject: [PATCH 4/9] ci: use GITHUB_TOKEN for repository writes --- .github/workflows/bench-main.yml | 11 ++++-- .github/workflows/bench-pr.yml | 36 +++++++------------ .../workflows/bencher-thresholds-reset.yml | 16 +++++---- .github/workflows/nix.yml | 2 +- .github/workflows/update.yml | 2 +- 5 files changed, 33 insertions(+), 34 deletions(-) diff --git a/.github/workflows/bench-main.yml b/.github/workflows/bench-main.yml index 85dd183ff..2d0c5ace2 100644 --- a/.github/workflows/bench-main.yml +++ b/.github/workflows/bench-main.yml @@ -29,7 +29,6 @@ on: permissions: contents: read - checks: write # No concurrency group on purpose: every merged commit gets benchmarked, # and a later merge must never cancel or queue behind an in-flight run. @@ -123,6 +122,9 @@ jobs: name: compile-${{ matrix.env }} needs: build runs-on: warp-ubuntu-latest-x64-32x + permissions: + contents: read + checks: write timeout-minutes: 60 strategy: fail-fast: false @@ -219,7 +221,7 @@ jobs: workload: ${{ steps.gates.outputs.workload }} file: benchmark.json key: ${{ secrets.BENCHER_API_KEY }} - github-token: ${{ secrets.GITHUB_TOKEN }} + github-token: ${{ github.token }} thresholds: ${{ steps.gates.outputs.thresholds }} # One job per remaining matrix entry, all sharing this one step list @@ -243,6 +245,9 @@ jobs: name: ${{ matrix.params.label }} needs: [compile, plan] runs-on: warp-ubuntu-latest-x64-32x + permissions: + contents: read + checks: write # `ix bench run` persists completed rows incrementally, so even a # job-level timeout keeps them on disk, but the bencher upload needs # the job alive. @@ -326,5 +331,5 @@ jobs: workload: ${{ matrix.params.workload }} file: bench-bmf.json key: ${{ secrets.BENCHER_API_KEY }} - github-token: ${{ secrets.GITHUB_TOKEN }} + github-token: ${{ github.token }} thresholds: ${{ matrix.params.thresholds }} diff --git a/.github/workflows/bench-pr.yml b/.github/workflows/bench-pr.yml index c7eef5abe..bf1be4b75 100644 --- a/.github/workflows/bench-pr.yml +++ b/.github/workflows/bench-pr.yml @@ -96,8 +96,6 @@ run-name: "${{ github.event_name == 'workflow_dispatch' && format('Benchmark PR permissions: contents: read - issues: read - pull-requests: read jobs: dispatch: @@ -244,13 +242,16 @@ jobs: # error message if the parse/build failed, otherwise a "running…" # placeholder so the commenter gets immediate feedback. The `comment` # job at the end edits this same comment in place with the results - # (this job's output is the comment id). Holds the App token, so — like - # `comment` — it never checks out or runs PR code; it only reads + # (this job's output is the comment id). This job has write permissions, + # so — like `comment` — it never checks out or runs PR code; it only reads # build's string outputs. announce: needs: build if: always() && github.event_name == 'workflow_dispatch' runs-on: ubuntu-latest + permissions: + issues: write + pull-requests: write outputs: comment-id: ${{ steps.post.outputs.comment-id }} steps: @@ -293,17 +294,11 @@ jobs: echo "[Watch progress]($RUN_URL)" } > comment-body.md fi - - name: Generate token to write PR comment - id: app-token - uses: actions/create-github-app-token@v3 - with: - client-id: ${{ secrets.TOKEN_APP_ID }} - private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }} - name: Post initial comment id: post uses: peter-evans/create-or-update-comment@v5 with: - token: ${{ steps.app-token.outputs.token }} + token: ${{ github.token }} issue-number: ${{ inputs.pr }} body-path: comment-body.md @@ -807,7 +802,7 @@ jobs: # Assemble the comment body from the per-run tables. Deliberately # UNPRIVILEGED: this job runs PR-built code (`ix bench report`), so it - # must never hold the App token. The posting job below only downloads + # must never receive write permissions. The posting job below only downloads # the finished body and never touches PR code. assemble: needs: [build, benchmark] @@ -875,12 +870,15 @@ jobs: # Replace the announce comment with the assembled results — or with an # error note when a stage failed: a rejected command or broken run must # never end in silence on the PR. This job and `announce` are the only - # two with the App token, and neither checks out or runs repo code — - # just an artifact download and two actions. + # two with write permissions, and neither checks out or runs repo code — + # just an artifact download and the comment action. comment: needs: [build, compile, benchmark, assemble, announce] if: always() && github.event_name == 'workflow_dispatch' runs-on: ubuntu-latest + permissions: + issues: write + pull-requests: write steps: - name: Download comment body if: needs.assemble.result == 'success' @@ -918,21 +916,13 @@ jobs: echo "[Workflow logs](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})" } > comment-body.md fi - - name: Generate token to write PR comment - id: app-token - uses: actions/create-github-app-token@v3 - with: - # `client-id` accepts the numeric App ID too (the JWT issuer claim - # takes either), so the existing secret works unchanged. - client-id: ${{ secrets.TOKEN_APP_ID }} - private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }} # `comment-id` targets the announce comment; if announce never # posted one (empty id), `issue-number` makes this create a fresh # comment instead. `replace` overwrites the "running…" placeholder. - name: Post / update comment uses: peter-evans/create-or-update-comment@v5 with: - token: ${{ steps.app-token.outputs.token }} + token: ${{ github.token }} issue-number: ${{ inputs.pr }} comment-id: ${{ needs.announce.outputs.comment-id }} edit-mode: replace diff --git a/.github/workflows/bencher-thresholds-reset.yml b/.github/workflows/bencher-thresholds-reset.yml index 90111bcde..f9958af04 100644 --- a/.github/workflows/bencher-thresholds-reset.yml +++ b/.github/workflows/bencher-thresholds-reset.yml @@ -53,17 +53,18 @@ on: issue_comment: types: [created] -permissions: - contents: write - pull-requests: write - issues: write # ack creates/applies the bencher-thresholds-reset: label +permissions: {} jobs: reset: if: github.event_name == 'workflow_dispatch' || github.event.pull_request.merged == true runs-on: ubuntu-latest + permissions: + contents: write + issues: write + pull-requests: write env: - GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} + GH_TOKEN: ${{ github.token }} REPO: ${{ github.repository }} EVENT: ${{ github.event_name }} INPUT_WORKLOAD: ${{ inputs.workload }} @@ -122,8 +123,11 @@ jobs: ack: 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, '!bencher-thresholds-reset') && (github.event.comment.author_association == 'OWNER' || github.event.comment.author_association == 'MEMBER' || github.event.comment.author_association == 'COLLABORATOR') runs-on: ubuntu-latest + permissions: + issues: write + pull-requests: write env: - GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} + GH_TOKEN: ${{ github.token }} REPO: ${{ github.repository }} PR: ${{ github.event.issue.number }} BODY: ${{ github.event.comment.body }} diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml index c6f291789..ca842e32a 100644 --- a/.github/workflows/nix.yml +++ b/.github/workflows/nix.yml @@ -29,7 +29,7 @@ jobs: - uses: cachix/install-nix-action@v31 with: nix_path: nixpkgs=channel:nixos-unstable - github_access_token: ${{ secrets.GITHUB_TOKEN }} + github_access_token: ${{ github.token }} - uses: cachix/cachix-action@v17 with: name: argumentcomputer diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml index 57dea131f..78e572470 100644 --- a/.github/workflows/update.yml +++ b/.github/workflows/update.yml @@ -31,4 +31,4 @@ jobs: lake_package_directory: ". Benchmarks/**" bump_mode: pinned-tags pr: true - token: ${{ secrets.GITHUB_TOKEN }} + token: ${{ github.token }} From b08d649346d29e56ef6b993360dc5f361311d94c Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 9 Sep 2026 16:56:35 -0400 Subject: [PATCH 5/9] ci: move the merge-tests stub to a pull_request-only workflow The "Merge tests" required check is satisfied on pull requests by a stub job and enforced in the merge queue by merge-tests.yml. Hosting the stub in ci.yml, which also runs on merge_group, left every merge-group commit with two check runs of that name: the skipped stub and the real result. GitHub documents same-named checks across workflows as ambiguous. A dedicated workflow that triggers only on pull_request emits exactly one "Merge tests" check per commit in either context, and produces no skipped jobs anywhere. --- .github/workflows/ci.yml | 8 -------- .github/workflows/merge-tests-stub.yml | 21 +++++++++++++++++++++ 2 files changed, 21 insertions(+), 8 deletions(-) create mode 100644 .github/workflows/merge-tests-stub.yml diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a6462edd1..88a9d5cc6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -13,14 +13,6 @@ concurrency: cancel-in-progress: true jobs: - merge-tests: - name: Merge tests - if: github.event_name == 'pull_request' - runs-on: ubuntu-latest - steps: - - name: Defer tests to merge queue - run: echo "Merge tests run against the merge group's synthetic commit." - # Build every regular Lake target before the test fan-out. The Namespace # volume is committed only after this job succeeds, so every saved build # cache contains the complete build rather than one parallel job's subset. diff --git a/.github/workflows/merge-tests-stub.yml b/.github/workflows/merge-tests-stub.yml new file mode 100644 index 000000000..1c829bc14 --- /dev/null +++ b/.github/workflows/merge-tests-stub.yml @@ -0,0 +1,21 @@ +name: Merge tests (pull request) + +# The "Merge tests" required check is enforced by merge-tests.yml, which runs +# the ignored suites only against the merge queue's synthetic commit. A pull +# request cannot enter the queue until every required check has passed on its +# own head, so this workflow reports the same check name there and does +# nothing else. It triggers only on pull_request so that a merge-group commit +# carries exactly one "Merge tests" check run — the real one — and no skipped +# stub alongside it. +on: + pull_request: + +permissions: {} + +jobs: + merge-tests: + name: Merge tests + runs-on: ubuntu-latest + steps: + - name: Defer tests to merge queue + run: echo "Merge tests run against the merge group's synthetic commit." From 749759af6d455c0f3d9251df335b372b9c406a7a Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 9 Sep 2026 16:56:58 -0400 Subject: [PATCH 6/9] bench: build the base side with the pinned codegen and toolchain A from-scratch base build in the PR benchmark job ran without the Rust setup action, so it took the tree's `.cargo/config.toml` and compiled for `-Ctarget-cpu=native` while the PR and main binaries were built for the fleet's fixed x86-64-v4 baseline. The base toolchain step also only installed when the two toolchain files differed, although nothing in the job had installed the PR's toolchain either. Run the shared setup action before the base build, caching the base workspace on WarpCache, and always ensure the base tree's own toolchain is present. --- .github/workflows/bench-pr.yml | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/.github/workflows/bench-pr.yml b/.github/workflows/bench-pr.yml index bf1be4b75..d96a44570 100644 --- a/.github/workflows/bench-pr.yml +++ b/.github/workflows/bench-pr.yml @@ -671,13 +671,21 @@ jobs: echo "cached=$cached" >> "$GITHUB_OUTPUT" echo "base .ixe: $([ "$ixe" = true ] && echo restored from cache || echo compiling in the base run)" echo "base binaries: $([ "$cached" = true ] && echo restored from cache || echo building from source)" - - name: Set up changed base Rust toolchain + # A from-scratch base build must match the PR and main binaries: the + # same pinned x86-64-v4 codegen (RUSTFLAGS overrides the tree's + # `.cargo/config.toml`, which selects `native`) and an installed + # toolchain. The action installs the PR checkout's toolchain; the base + # tree may pin a different channel, so ensure its own is present too. + - name: Set up Rust for the base build + if: steps.decide.outputs.run-base == 'true' && steps.base-src.outputs.cached != 'true' + uses: ./.github/actions/setup-rust-toolchain + with: + cache-provider: warpbuild + cache-workspaces: base + - name: Install the base tree's Rust toolchain if: steps.decide.outputs.run-base == 'true' && steps.base-src.outputs.cached != 'true' working-directory: base - run: | - if ! cmp -s rust-toolchain.toml ../rust-toolchain.toml; then - rustup show active-toolchain || rustup toolchain install - fi + run: rustup show active-toolchain || rustup toolchain install - name: Log base build CPU if: steps.decide.outputs.run-base == 'true' && steps.base-src.outputs.cached != 'true' uses: ./.github/actions/log-cpu From dfa9ca446c235e296fdbe20ac68d13e14f7ab5b5 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 9 Sep 2026 16:56:58 -0400 Subject: [PATCH 7/9] bench: label each table side with the host that measured it The comment header reported the build job's CPU as the run's hardware, but the fleet mixes CPU models and the measured rows come from other runners: the PR compile row from the compile job, and a bencher-sourced base side from bench-main at the base SHA. Each compare table now ends with one hardware line per side. The compile job carries its host with the row in the cache entry and run artifact; bench-main caches its measurement host by SHA and parameters, mirroring the attribution CSV, and the PR run restores it for a bencher-sourced base. A base run in the benchmark job is labelled with that job's runner. The build-host summary is dropped from the comment, since pinned codegen makes it irrelevant. --- .github/workflows/bench-main.yml | 33 +++++++++++++++ .github/workflows/bench-pr.yml | 70 +++++++++++++++++++++++--------- docs/benchmarking.md | 11 +++-- 3 files changed, 92 insertions(+), 22 deletions(-) diff --git a/.github/workflows/bench-main.yml b/.github/workflows/bench-main.yml index 2d0c5ace2..25f42ea2b 100644 --- a/.github/workflows/bench-main.yml +++ b/.github/workflows/bench-main.yml @@ -153,6 +153,7 @@ jobs: path: ~/.local/bin key: bench-bins-${{ github.sha }} - name: Log compile CPU + id: cpu uses: ./.github/actions/log-cpu with: label: Compile measurement CPU @@ -200,6 +201,7 @@ jobs: meta() { jq -r --arg env "${{ matrix.env }}" "first(.[] | select(.backend == \"compile\" and .env == \$env)).$1" matrix.json; } echo "testbed=$(meta testbed)" >> "$GITHUB_OUTPUT" echo "workload=$(meta workload)" >> "$GITHUB_OUTPUT" + echo "mode=$(meta mode)" >> "$GITHUB_OUTPUT" { echo "thresholds<> "$GITHUB_OUTPUT" # Cache the `.ixe` for the benchmark job. IMPORTANT: every restore of # this key must list the same paths — cache versions include the @@ -212,6 +214,22 @@ jobs: with: path: ${{ matrix.env }}.ixe key: bench-ixe-${{ github.sha }}-${{ matrix.env }} + # Record the host that measured this row. Bencher stores metric rows + # only, so bench-pr restores this note by (SHA, parameters) to label a + # bencher-sourced base side with its own hardware. Best-effort: a + # missing entry renders as "not recorded". + - name: Record measurement hardware + if: ${{ !cancelled() }} + env: + HARDWARE: ${{ steps.cpu.outputs.summary }} + run: printf '%s\n' "$HARDWARE" > bench-hardware.txt + - name: Cache measurement hardware + if: ${{ !cancelled() }} + continue-on-error: true + uses: WarpBuilds/cache/save@v2 + with: + path: bench-hardware.txt + key: bench-hardware-${{ github.sha }}-compile-${{ matrix.env }}-${{ steps.gates.outputs.mode }} # Upload the compile metrics. Testbed, workload, and threshold flags # all come from the registry (the reasoning behind each bound lives # next to `thresholds` in Ix/Cli/BenchCmd.lean). @@ -263,6 +281,7 @@ jobs: path: ~/.local/bin key: bench-bins-${{ github.sha }} - name: Log run CPU + id: cpu uses: ./.github/actions/log-cpu with: label: Benchmark measurement CPU @@ -303,6 +322,20 @@ jobs: with: path: bench.json.perconst.csv key: bench-perconst-${{ github.sha }}-${{ matrix.params.backend }}-${{ matrix.params.env }}-${{ matrix.params.mode }} + # The measurement host, by (SHA, parameters), for bench-pr to label a + # bencher-sourced base side — same best-effort contract as the CSV. + - name: Record measurement hardware + if: ${{ !cancelled() }} + env: + HARDWARE: ${{ steps.cpu.outputs.summary }} + run: printf '%s\n' "$HARDWARE" > bench-hardware.txt + - name: Cache measurement hardware + if: ${{ !cancelled() }} + continue-on-error: true + uses: WarpBuilds/cache/save@v2 + with: + path: bench-hardware.txt + key: bench-hardware-${{ github.sha }}-${{ matrix.params.backend }}-${{ matrix.params.env }}-${{ matrix.params.mode }} # Convert rows for upload even when the run step failed: bmf drops # every non-ok row (rejected or OOM), so only clean measurements # reach bencher. bmf exits nonzero when NO ok rows survive — the diff --git a/.github/workflows/bench-pr.yml b/.github/workflows/bench-pr.yml index d96a44570..4264f6b5f 100644 --- a/.github/workflows/bench-pr.yml +++ b/.github/workflows/bench-pr.yml @@ -151,7 +151,6 @@ jobs: fresh: ${{ steps.parse.outputs.fresh }} passthrough-env: ${{ steps.parse.outputs.passthrough-env }} config-summary: ${{ steps.parse.outputs.config-summary }} - hardware-summary: ${{ steps.cpu.outputs.summary }} # Set (with the step failing) when the !benchmark command was # rejected; the failure comment quotes it. parse-error: ${{ steps.parse.outputs.parse-error }} @@ -209,11 +208,10 @@ jobs: uses: ./.github/actions/setup-rust-toolchain with: cache-provider: warpbuild - - name: Log benchmark runner CPU - id: cpu + - name: Log build CPU uses: ./.github/actions/log-cpu with: - label: Benchmark runner CPU + label: Benchmark binary build CPU - name: Build benchmark binaries if: steps.parse.outputs.fresh == '1' || steps.bins.outputs.cache-hit != 'true' run: | @@ -264,7 +262,6 @@ jobs: BUILD_RESULT: ${{ needs.build.result }} PARSE_ERROR: ${{ needs.build.outputs.parse-error }} SUMMARY: ${{ needs.build.outputs.config-summary }} - HARDWARE: ${{ needs.build.outputs.hardware-summary }} HEAD_SHA: ${{ needs.build.outputs.revision }} run: | RUN_URL="${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" @@ -285,9 +282,6 @@ jobs: if [ -n "$SUMMARY" ]; then echo "> $SUMMARY" fi - if [ -n "$HARDWARE" ]; then - echo "> $HARDWARE" - fi echo echo "Benchmarking \`${HEAD_SHA:0:7}\` — this comment will be replaced with the results when the run finishes." echo @@ -351,7 +345,9 @@ jobs: id: pr-row uses: WarpBuilds/cache/restore@v2 with: - path: compile.json + path: | + compile.json + compile-hardware.txt key: bench-pr-row-${{ needs.build.outputs.revision }}-${{ matrix.env }} - name: Select compile source id: compile-source @@ -375,6 +371,7 @@ jobs: echo "$HOME/.local/bin" >> "$GITHUB_PATH" - name: Log compile CPU if: steps.compile-source.outputs.rebuild == 'true' + id: cpu uses: ./.github/actions/log-cpu with: label: Compile measurement CPU @@ -400,6 +397,14 @@ jobs: - name: Compile ${{ matrix.env }}.ixe if: steps.compile-source.outputs.rebuild == 'true' run: ix bench run --backend compile --env ${{ matrix.env }} --out compile.json + # The compile row is measured here, not in the benchmark job that + # renders it, so its host travels with the row: same cache entry and + # run artifact below. + - name: Record compile hardware + if: steps.compile-source.outputs.rebuild == 'true' + env: + HARDWARE: ${{ steps.cpu.outputs.summary }} + run: printf '%s\n' "$HARDWARE" > compile-hardware.txt - name: Publish .ixe if: needs.build.outputs.fresh != '1' && steps.pr-ixe.outputs.cache-hit != 'true' uses: WarpBuilds/cache/save@v2 @@ -414,7 +419,9 @@ jobs: if: needs.build.outputs.fresh != '1' && steps.pr-row.outputs.cache-hit != 'true' uses: WarpBuilds/cache/save@v2 with: - path: compile.json + path: | + compile.json + compile-hardware.txt key: bench-pr-row-${{ needs.build.outputs.revision }}-${{ matrix.env }} - name: Upload run environment uses: actions/upload-artifact@v7 @@ -423,6 +430,7 @@ jobs: path: | ${{ matrix.env }}.ixe compile.json + compile-hardware.txt if-no-files-found: error retention-days: 1 overwrite: true @@ -487,6 +495,7 @@ jobs: tar -C .lake/build/bin -xf benchmark-binaries.tar echo "$PWD/.lake/build/bin" >> "$GITHUB_PATH" - name: Log run CPU + id: cpu uses: ./.github/actions/log-cpu with: label: Benchmark job CPU @@ -589,6 +598,16 @@ jobs: with: path: bench.json.perconst.csv key: bench-perconst-${{ env.BASE_SHA }}-${{ matrix.params.backend }}-${{ matrix.params.env }}-${{ matrix.params.mode }} + # The host that measured the base SHA's rows on main, recorded by + # bench-main next to its bencher upload. Only a bencher-sourced base side + # uses it; a base run in this job is labelled with this runner instead. + - name: Restore base-side measurement hardware + if: env.FRESH != '1' + continue-on-error: true + uses: WarpBuilds/cache/restore@v2 + with: + path: bench-hardware.txt + key: bench-hardware-${{ env.BASE_SHA }}-${{ matrix.params.backend }}-${{ matrix.params.env }}-${{ matrix.params.mode }} # The final base-run decision — every base-side step gates on THIS # step. A base run, whatever triggered it (bencher miss or partial, # `fresh`, or an ooc attribution-CSV cache miss), is always a FULL @@ -782,6 +801,8 @@ jobs: mv bench.json.perconst.csv "$GITHUB_WORKSPACE/main.json.perconst.csv" fi - name: Build comparison table + env: + RUN_HARDWARE: ${{ steps.cpu.outputs.summary }} run: | mkdir -p out ix bench compare \ @@ -790,6 +811,25 @@ jobs: --base-source "${{ steps.decide.outputs.source }}" \ --base-label "${BASE_REF:-${BASE_SHA::7}}" \ --out "out/table-$LABEL.md" + # Label each side with the host that measured it. The fleet mixes + # CPU models, and the two sides need not share one: the PR compile + # row comes from the compile job, and a bencher-sourced base side + # from bench-main's run at the base SHA. Every other side ran here. + if [ "$BACKEND" = compile ]; then + pr_hw=$(cat compile-hardware.txt 2>/dev/null || true) + else + pr_hw="$RUN_HARDWARE" + fi + if [ "${{ steps.decide.outputs.run-base }}" = true ]; then + base_hw="$RUN_HARDWARE" + else + base_hw=$(cat bench-hardware.txt 2>/dev/null || true) + fi + { + echo + echo "- Base hardware (${{ steps.decide.outputs.source }}): ${base_hw:-not recorded}" + echo "- PR hardware: ${pr_hw:-not recorded}" + } >> "out/table-$LABEL.md" cat "out/table-$LABEL.md" - name: Upload table @@ -851,21 +891,13 @@ jobs: - name: Build comment body env: SUMMARY: ${{ needs.build.outputs.config-summary }} - HARDWARE: ${{ needs.build.outputs.hardware-summary }} HEAD_SHA: ${{ needs.build.outputs.revision }} BASE_SHA: ${{ inputs.base-sha }} BASE_REF: ${{ inputs.base-ref }} run: | mkdir -p tables # absent when no run uploaded a table - summary="$SUMMARY" - if [ -n "$HARDWARE" ]; then - if [ -n "$summary" ]; then - summary="$summary"$'\n\n' - fi - summary="$summary$HARDWARE" - fi ix bench report \ - --tables tables --summary "$summary" \ + --tables tables --summary "$SUMMARY" \ --head "$HEAD_SHA" \ --base-label "${BASE_REF:-${BASE_SHA::7}}" \ --repo-url "${{ github.server_url }}/${{ github.repository }}" \ diff --git a/docs/benchmarking.md b/docs/benchmarking.md index 1c6125e70..ca12a8f51 100644 --- a/docs/benchmarking.md +++ b/docs/benchmarking.md @@ -297,9 +297,14 @@ WarpCache for both workflow products and Cargo build artifacts. Every job that creates a timing row logs its CPU model, instruction set, effective CPU count, affinity, and cgroup allocation directly in the Actions -logs. The `!benchmark` comment also includes a compact CPU model, effective -vCPU count, and total RAM summary. This is diagnostic only: CPU information -does not participate in cache keys or benchmark results. +logs. Each table in the `!benchmark` comment ends with one hardware line per +side (CPU model, effective vCPUs, total RAM), because the two sides need not +share a host: the PR compile row is measured in the compile job, and a +bencher-sourced base side was measured by bench-main at the base SHA, which +caches that host next to its upload for the PR run to restore. A base run +performed in the benchmark job is labelled with that job's runner. This is +diagnostic only: CPU information does not participate in cache keys or +benchmark results, and a missing note renders as "not recorded". ## Palomar compatibility corpus From 682deb3824e0b33b3f1cfb0fae436641a932c278 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 9 Sep 2026 17:35:39 -0400 Subject: [PATCH 8/9] ci: pin bindgen to one LLVM install on multi-version runner images Lake's Rust build of the Blake3 package runs lean-ffi's bindgen over lean.h, which failed on the Namespace Ubuntu 26.04 image with every C11 atomic undeclared. bindgen collects include paths from the clang binary on PATH and passes them as -isystem, while clang-sys loads whichever libclang it finds; on an image shipping LLVM 20, 21 and 22 those differ, so clang's stdatomic.h include_nexts the other version's copy, whose identical include guard skips its body (rust-bindgen #2682, #3316). Export LIBCLANG_PATH and CLANG_PATH for the newest install that has both clang and libclang, leaving the defaults where none exists. --- .../actions/setup-rust-toolchain/action.yml | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/.github/actions/setup-rust-toolchain/action.yml b/.github/actions/setup-rust-toolchain/action.yml index 56bd63b64..4570a62f8 100644 --- a/.github/actions/setup-rust-toolchain/action.yml +++ b/.github/actions/setup-rust-toolchain/action.yml @@ -72,6 +72,25 @@ runs: exit 1 fi + # bindgen collects include paths from the `clang` binary on PATH and + # passes them as `-isystem`, while clang-sys loads whichever libclang it + # finds. On an image with several LLVM versions those differ: clang's + # `stdatomic.h` then `include_next`s the other version's copy, whose + # identical include guard skips its body, and every C11 atomic in + # `lean.h` comes out undeclared. Point both at one install. + - name: Pin bindgen to a single LLVM install + shell: bash + run: | + for llvm in $(printf '%s\n' /usr/lib/llvm-* | sort -V -r); do + if [ -x "$llvm/bin/clang" ] && ls "$llvm"/lib/libclang*.so* >/dev/null 2>&1; then + echo "LIBCLANG_PATH=$llvm/lib" >> "$GITHUB_ENV" + echo "CLANG_PATH=$llvm/bin/clang" >> "$GITHUB_ENV" + echo "bindgen pinned to $llvm" + exit 0 + fi + done + echo "no versioned LLVM install with both clang and libclang; leaving bindgen defaults" + - uses: actions-rust-lang/setup-rust-toolchain@v1 with: rustflags: ${{ inputs.avx512-codegen == 'true' && '-Ctarget-cpu=x86-64-v4 -Ctarget-feature=+avx512vbmi2,+gfni -Dwarnings' || '-Dwarnings' }} From 18463ff16ec7c6c2b4ed95bf1a4df3602cb7599e Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 9 Sep 2026 17:35:39 -0400 Subject: [PATCH 9/9] ci: trial the valgrind job on a GitHub-hosted runner Valgrind itself is single-threaded; the job's cost is the portable build of IxTests it needs, since the shared cache carries AVX-512 codegen the tool cannot decode. Run it on ubuntu-latest with its own actions/cache entry for .lake, and temporarily also on pull_request so the build and restore times can be measured before it takes that role in the merge queue. prepare and the result job stay gated off pull_request, so the stub workflow remains the only "Merge tests" check on a PR. The runner name guard in setup-rust-toolchain now applies only to AVX-512 builds. --- .../actions/setup-rust-toolchain/action.yml | 13 ++++-- .github/workflows/merge-tests.yml | 41 +++++++++++++------ 2 files changed, 39 insertions(+), 15 deletions(-) diff --git a/.github/actions/setup-rust-toolchain/action.yml b/.github/actions/setup-rust-toolchain/action.yml index 4570a62f8..5cdf6981f 100644 --- a/.github/actions/setup-rust-toolchain/action.yml +++ b/.github/actions/setup-rust-toolchain/action.yml @@ -23,16 +23,23 @@ inputs: runs: using: composite steps: + # The AVX-512 baseline below is a property of the Warp and Namespace + # fleets; a portable build may run on any Linux x64 host. - name: Require supported Linux x64 runner shell: bash env: IX_RUNNER_NAME: ${{ runner.name }} IX_RUNNER_OS: ${{ runner.os }} IX_RUNNER_ARCH: ${{ runner.arch }} + IX_AVX512_CODEGEN: ${{ inputs.avx512-codegen }} run: | - if [[ "$IX_RUNNER_OS" != Linux || "$IX_RUNNER_ARCH" != X64 || \ - ("$IX_RUNNER_NAME" != warp-* && "$IX_RUNNER_NAME" != nsc-runner-*) ]]; then - echo "::error::setup-rust-toolchain requires a Warp or Namespace Linux x64 runner; got name=$IX_RUNNER_NAME os=$IX_RUNNER_OS arch=$IX_RUNNER_ARCH" + if [[ "$IX_RUNNER_OS" != Linux || "$IX_RUNNER_ARCH" != X64 ]]; then + echo "::error::setup-rust-toolchain requires a Linux x64 runner; got os=$IX_RUNNER_OS arch=$IX_RUNNER_ARCH" + exit 1 + fi + if [[ "$IX_AVX512_CODEGEN" == true && \ + "$IX_RUNNER_NAME" != warp-* && "$IX_RUNNER_NAME" != nsc-runner-* ]]; then + echo "::error::AVX-512 builds require a Warp or Namespace runner; got name=$IX_RUNNER_NAME" exit 1 fi diff --git a/.github/workflows/merge-tests.yml b/.github/workflows/merge-tests.yml index b293c7996..0d6dad72c 100644 --- a/.github/workflows/merge-tests.yml +++ b/.github/workflows/merge-tests.yml @@ -4,6 +4,10 @@ on: merge_group: issue_comment: types: [created] + # Only the valgrind job runs on pull requests, as a trial of the + # GitHub-hosted runner's build and cache times before it takes that role + # in the queue permanently. + pull_request: run-name: "${{ github.event_name == 'issue_comment' && format('Merge tests for PR #{0}', github.event.issue.number) || 'Merge tests' }}" @@ -17,8 +21,9 @@ jobs: prepare: name: Prepare merge tests if: >- - github.event_name != 'issue_comment' || - (github.event.issue.pull_request && + 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') && @@ -168,20 +173,26 @@ jobs: valgrind: name: Valgrind FFI needs: prepare - if: ${{ github.event_name == 'merge_group' || github.event_name == 'issue_comment' }} - # Valgrind cannot decode the shared baseline's AVX-512, so its portable - # build artifacts must not share a cache volume with the other test jobs. - runs-on: - - nscloud-ubuntu-26.04-amd64-8x16-with-cache - - nscloud-cache-size-50gb - - nscloud-cache-tag-argumentcomputer-ix-valgrind + # `prepare` is skipped on pull_request, so `!cancelled()` keeps this job + # eligible there; the other events still require `prepare` to succeed. + if: >- + !cancelled() && + (github.event_name == 'pull_request' || + (needs.prepare.result == 'success' && + (github.event_name == 'merge_group' || github.event_name == 'issue_comment'))) + # Valgrind cannot decode the shared baseline's AVX-512, so this job builds + # portable artifacts under its own cache key. Valgrind itself is + # single-threaded, so a GitHub-hosted runner suffices once that build is + # cached. + runs-on: ubuntu-latest 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 == 'pull_request' && github.sha || (github.event_name == 'issue_comment' && format('refs/pull/{0}/merge', needs.prepare.outputs.pr) || needs.prepare.outputs.revision) }} persist-credentials: false - name: Verify test revision + if: github.event_name != 'pull_request' env: TEST_REVISION: ${{ needs.prepare.outputs.revision }} run: | @@ -194,8 +205,13 @@ jobs: - uses: ./.github/actions/setup-rust-toolchain with: avx512-codegen: "false" - use-github-cache: "false" - - uses: ./.github/actions/setup-lake-cache + # `./.lake`, not `.lake`: the path string is hashed into the cache + # entry's version, so the spelling must stay fixed for restores to hit. + - uses: actions/cache@v6 + with: + path: ./.lake + key: lake-valgrind-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} + restore-keys: lake-valgrind-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}- - uses: leanprover/lean-action@v1 with: auto-config: false @@ -224,6 +240,7 @@ jobs: name: Merge tests if: >- always() && + github.event_name != 'pull_request' && (github.event_name != 'issue_comment' || needs.prepare.result != 'skipped') needs: [prepare, merge-tests, valgrind] runs-on: ubuntu-latest