From a4712ffb1bd055d763c899658975e7ffe0c5951f Mon Sep 17 00:00:00 2001 From: Tianshu Huang Date: Fri, 23 Oct 2026 11:36:46 -0700 Subject: [PATCH 1/4] Run autoharness CI jobs only in merge queue or on dispatch (#730) --- .github/workflows/kani.yml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 8673ecfa2e220..3f72aa0431554 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -67,6 +67,10 @@ jobs: kani_autoharness: name: Verify std library using autoharness + # Autoharness, Metrics, List, Analyzer and Build JSON run only in the merge queue or on + # request (#730): they cost about 5 runner-hours per run and decide how long a PR waits. + # A job skipped by its `if:` counts as successful, so PRs are not blocked during review. + if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' runs-on: ${{ matrix.os }} strategy: matrix: @@ -229,6 +233,7 @@ jobs: run_kani_metrics: name: Kani Metrics + if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' runs-on: ${{ matrix.os }} strategy: matrix: @@ -299,6 +304,7 @@ jobs: run-log-analysis: name: Build JSON from logs + if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' needs: [run_kani_metrics, kani_autoharness] runs-on: ${{ matrix.os }} strategy: @@ -351,6 +357,7 @@ jobs: run-kani-list: name: Kani List + if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' runs-on: ubuntu-latest steps: - name: Remove unnecessary software to free up disk space @@ -396,6 +403,7 @@ jobs: run-autoharness-analyzer: name: Kani Autoharness Analyzer + if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' runs-on: ubuntu-latest steps: # Step 1: Check out the repository From d0c8abaa1cf592c749bcb120958c2deed7ad9a5c Mon Sep 17 00:00:00 2001 From: Tianshu Huang Date: Fri, 23 Oct 2026 14:19:18 -0700 Subject: [PATCH 2/4] Gate autoharness steps, not the job, so the required check stays green --- .github/workflows/kani.yml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 3f72aa0431554..34ce46fe1e28f 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -69,8 +69,9 @@ jobs: name: Verify std library using autoharness # Autoharness, Metrics, List, Analyzer and Build JSON run only in the merge queue or on # request (#730): they cost about 5 runner-hours per run and decide how long a PR waits. - # A job skipped by its `if:` counts as successful, so PRs are not blocked during review. - if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' + # This job is a required check under its matrix name, and a job skipped by a job-level + # `if:` reports without the "(os)" suffix, which would leave PRs pending. So the gate is + # on each step instead: on a PR the job starts, skips every step and passes in seconds. runs-on: ${{ matrix.os }} strategy: matrix: @@ -84,7 +85,7 @@ jobs: steps: - name: Remove unnecessary software to free up disk space - if: matrix.os == 'ubuntu-latest' + if: matrix.os == 'ubuntu-latest' && (github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch') run: | # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml df -h @@ -93,6 +94,7 @@ jobs: # Step 1: Check out the repository - name: Checkout Repository + if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' uses: actions/checkout@v4 with: submodules: true @@ -111,6 +113,7 @@ jobs: # Unicode tables were regenerated (nightly-2026-09-25) they exceed the 10m # timeout on macOS and the ubuntu runner died while verifying them. - name: Run Kani Verification + if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' run: | scripts/run-kani.sh --run autoharness --kani-args \ --include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::disjoint_bitor" \ @@ -223,6 +226,7 @@ jobs: gzip autoharness-verification.log - name: Upload Autoharness Verification Log + if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' uses: actions/upload-artifact@v4 with: name: ${{ matrix.os }}-autoharness-verification.log.gz From c939eedc98f69e4a7de60fd8be28bf68215d0f8a Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 30 Oct 2026 23:30:19 +0000 Subject: [PATCH 3/4] Let maintainers request autoharness on a PR with a label Running autoharness only in the merge queue means a contributor's first autoharness result arrives after the PR is queued, and a failure ejects it hours later. workflow_dispatch does not help contributors: it needs write access and runs on a branch of this repo, not on a fork's PR. Add the run-autoharness label as a third way to run the autoharness and metrics jobs: while it is on a PR they run on every push. Adding any label now triggers the workflow, so the partitions skip label events (they already ran for that commit) and the autoharness jobs ignore labels other than run-autoharness. --- .github/workflows/kani.yml | 26 ++++++++++++++++---------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 34ce46fe1e28f..d2d3e3691e421 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -5,6 +5,8 @@ on: merge_group: pull_request: branches: [ main ] + # `labeled` lets a maintainer request autoharness on a PR with the run-autoharness label. + types: [opened, synchronize, reopened, labeled] push: paths: - 'library/**' @@ -18,6 +20,8 @@ defaults: jobs: check-kani-on-std: name: Verify std library (partition ${{ matrix.partition }}) + # Adding a label must not re-run the partitions; they already ran for this commit. + if: github.event.action != 'labeled' runs-on: ${{ matrix.os }} strategy: matrix: @@ -67,8 +71,10 @@ jobs: kani_autoharness: name: Verify std library using autoharness - # Autoharness, Metrics, List, Analyzer and Build JSON run only in the merge queue or on - # request (#730): they cost about 5 runner-hours per run and decide how long a PR waits. + if: github.event.action != 'labeled' || github.event.label.name == 'run-autoharness' + # Autoharness, Metrics, List, Analyzer and Build JSON run only in the merge queue, on + # workflow_dispatch, or on PRs with the run-autoharness label (#730): they cost about 5 + # runner-hours per run and decide how long a PR waits. # This job is a required check under its matrix name, and a job skipped by a job-level # `if:` reports without the "(os)" suffix, which would leave PRs pending. So the gate is # on each step instead: on a PR the job starts, skips every step and passes in seconds. @@ -85,7 +91,7 @@ jobs: steps: - name: Remove unnecessary software to free up disk space - if: matrix.os == 'ubuntu-latest' && (github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch') + if: matrix.os == 'ubuntu-latest' && (github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'run-autoharness')) run: | # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml df -h @@ -94,7 +100,7 @@ jobs: # Step 1: Check out the repository - name: Checkout Repository - if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' + if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'run-autoharness') uses: actions/checkout@v4 with: submodules: true @@ -113,7 +119,7 @@ jobs: # Unicode tables were regenerated (nightly-2026-09-25) they exceed the 10m # timeout on macOS and the ubuntu runner died while verifying them. - name: Run Kani Verification - if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' + if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'run-autoharness') run: | scripts/run-kani.sh --run autoharness --kani-args \ --include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::disjoint_bitor" \ @@ -226,7 +232,7 @@ jobs: gzip autoharness-verification.log - name: Upload Autoharness Verification Log - if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' + if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'run-autoharness') uses: actions/upload-artifact@v4 with: name: ${{ matrix.os }}-autoharness-verification.log.gz @@ -237,7 +243,7 @@ jobs: run_kani_metrics: name: Kani Metrics - if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' + if: (github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'run-autoharness')) && (github.event.action != 'labeled' || github.event.label.name == 'run-autoharness') runs-on: ${{ matrix.os }} strategy: matrix: @@ -308,7 +314,7 @@ jobs: run-log-analysis: name: Build JSON from logs - if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' + if: (github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'run-autoharness')) && (github.event.action != 'labeled' || github.event.label.name == 'run-autoharness') needs: [run_kani_metrics, kani_autoharness] runs-on: ${{ matrix.os }} strategy: @@ -361,7 +367,7 @@ jobs: run-kani-list: name: Kani List - if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' + if: (github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'run-autoharness')) && (github.event.action != 'labeled' || github.event.label.name == 'run-autoharness') runs-on: ubuntu-latest steps: - name: Remove unnecessary software to free up disk space @@ -407,7 +413,7 @@ jobs: run-autoharness-analyzer: name: Kani Autoharness Analyzer - if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' + if: (github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'run-autoharness')) && (github.event.action != 'labeled' || github.event.label.name == 'run-autoharness') runs-on: ubuntu-latest steps: # Step 1: Check out the repository From e51a2bcefed38d954e3634f82c067fabd818a9e6 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 30 Oct 2026 23:30:38 +0000 Subject: [PATCH 4/4] Explain why the label-only job-level skip is safe for the required check --- .github/workflows/kani.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index d2d3e3691e421..9c99dfa15cb86 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -78,6 +78,8 @@ jobs: # This job is a required check under its matrix name, and a job skipped by a job-level # `if:` reports without the "(os)" suffix, which would leave PRs pending. So the gate is # on each step instead: on a PR the job starts, skips every step and passes in seconds. + # The job-level `if:` above only skips events for other labels; the required check has + # already reported for that commit by then. runs-on: ${{ matrix.os }} strategy: matrix: