From a4712ffb1bd055d763c899658975e7ffe0c5951f Mon Sep 17 00:00:00 2001 From: Tianshu Huang Date: Fri, 23 Oct 2026 11:36:46 -0700 Subject: [PATCH 1/5] 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/5] 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/5] 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/5] 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: From a6df330eeb156bf38c4523ecfb95056e5246bf04 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Mon, 2 Nov 2026 00:53:42 +0000 Subject: [PATCH 5/5] Trigger label-requested autoharness from a separate workflow Adding a label started a new run of kani.yml on the same commit, and GitHub reads required checks from the latest run. That run skipped the partitions (and, for other labels, the autoharness jobs), so the required checks went back to "expected" and the PR could not enter the merge queue. kani.yml no longer reacts to labels. kani-autoharness-request.yml runs on labeled/synchronize/reopened and, when the PR has run-autoharness, calls kani.yml with autoharness: true, which runs only the autoharness and metrics jobs. Its checks are prefixed with the caller job name, so they never collide with the required ones. --- .../workflows/kani-autoharness-request.yml | 19 ++++++++++ .github/workflows/kani.yml | 35 ++++++++++--------- 2 files changed, 38 insertions(+), 16 deletions(-) create mode 100644 .github/workflows/kani-autoharness-request.yml diff --git a/.github/workflows/kani-autoharness-request.yml b/.github/workflows/kani-autoharness-request.yml new file mode 100644 index 0000000000000..aa94b48babe4b --- /dev/null +++ b/.github/workflows/kani-autoharness-request.yml @@ -0,0 +1,19 @@ +# Runs the autoharness and Kani metrics jobs on a PR that has the run-autoharness label, so a +# contributor can see those results before the merge queue (#730). This is a separate workflow +# so that adding a label never starts a new run of kani.yml: GitHub reads required checks from +# the latest run, and a label-only run would leave the partitions "expected". +name: Kani autoharness on request + +on: + pull_request: + branches: [ main ] + types: [labeled, synchronize, reopened] + +jobs: + autoharness: + if: >- + contains(github.event.pull_request.labels.*.name, 'run-autoharness') && + (github.event.action != 'labeled' || github.event.label.name == 'run-autoharness') + uses: ./.github/workflows/kani.yml + with: + autoharness: true diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 9c99dfa15cb86..21eb1e2a2d490 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -2,11 +2,16 @@ name: Kani on: workflow_dispatch: + # Called by kani-autoharness-request.yml when a PR has the run-autoharness label. + workflow_call: + inputs: + autoharness: + description: Run only the autoharness and metrics jobs + type: boolean + default: false 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/**' @@ -20,8 +25,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' + # When called for autoharness only, the partitions already ran for this commit. + if: ${{ !inputs.autoharness }} runs-on: ${{ matrix.os }} strategy: matrix: @@ -71,15 +76,13 @@ jobs: kani_autoharness: name: Verify std library using autoharness - 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 + # workflow_dispatch, or on PRs with the run-autoharness label, through + # kani-autoharness-request.yml (#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. - # 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: @@ -93,7 +96,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' || contains(github.event.pull_request.labels.*.name, 'run-autoharness')) + if: matrix.os == 'ubuntu-latest' && (github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || inputs.autoharness) run: | # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml df -h @@ -102,7 +105,7 @@ jobs: # Step 1: Check out the repository - name: Checkout Repository - if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'run-autoharness') + if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || inputs.autoharness uses: actions/checkout@v4 with: submodules: true @@ -121,7 +124,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' || contains(github.event.pull_request.labels.*.name, 'run-autoharness') + if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || inputs.autoharness run: | scripts/run-kani.sh --run autoharness --kani-args \ --include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::disjoint_bitor" \ @@ -234,7 +237,7 @@ jobs: gzip autoharness-verification.log - name: Upload Autoharness Verification Log - if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'run-autoharness') + if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || inputs.autoharness uses: actions/upload-artifact@v4 with: name: ${{ matrix.os }}-autoharness-verification.log.gz @@ -245,7 +248,7 @@ jobs: run_kani_metrics: name: Kani Metrics - 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') + if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || inputs.autoharness runs-on: ${{ matrix.os }} strategy: matrix: @@ -316,7 +319,7 @@ jobs: run-log-analysis: name: Build JSON from logs - 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') + if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || inputs.autoharness needs: [run_kani_metrics, kani_autoharness] runs-on: ${{ matrix.os }} strategy: @@ -369,7 +372,7 @@ jobs: run-kani-list: name: Kani List - 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') + if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || inputs.autoharness runs-on: ubuntu-latest steps: - name: Remove unnecessary software to free up disk space @@ -415,7 +418,7 @@ jobs: run-autoharness-analyzer: name: Kani Autoharness Analyzer - 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') + if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || inputs.autoharness runs-on: ubuntu-latest steps: # Step 1: Check out the repository