Skip to content

Run autoharness jobs only in the merge queue #738

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Tianshu-Huang wants to merge 4 commits into
base: main
Choose a base branch
from
Open

Run autoharness jobs only in the merge queue #738

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
a4712ff
Run autoharness CI jobs only in merge queue or on dispatch (#730)
Tianshu-Huang Oct 23, 2026
d0c8aba
Gate autoharness steps, not the job, so the required check stays green
Tianshu-Huang Oct 23, 2026
c939eed
Let maintainers request autoharness on a PR with a label
feliperodri Oct 30, 2026
e51a2bc
Explain why the label-only job-level skip is safe for the required check
feliperodri Oct 30, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 21 additions & 1 deletion .github/workflows/kani.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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/**'
Expand All @@ -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:
Expand Down Expand Up @@ -67,6 +71,15 @@ 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
# 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:
Expand All @@ -80,7 +93,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' || 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
Expand All @@ -89,6 +102,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')
uses: actions/checkout@v4
with:
submodules: true
Expand All @@ -107,6 +121,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')
run: |
scripts/run-kani.sh --run autoharness --kani-args \
--include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::disjoint_bitor" \
Expand Down Expand Up @@ -219,6 +234,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')
uses: actions/upload-artifact@v4
with:
name: ${{ matrix.os }}-autoharness-verification.log.gz
Expand All @@ -229,6 +245,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')
runs-on: ${{ matrix.os }}
strategy:
matrix:
Expand Down Expand Up @@ -299,6 +316,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')
needs: [run_kani_metrics, kani_autoharness]
runs-on: ${{ matrix.os }}
strategy:
Expand Down Expand Up @@ -351,6 +369,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')
runs-on: ubuntu-latest
steps:
- name: Remove unnecessary software to free up disk space
Expand Down Expand Up @@ -396,6 +415,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')
runs-on: ubuntu-latest
steps:
# Step 1: Check out the repository
Expand Down
Loading