Run autoharness and Kani metrics jobs only in the merge queue #730

Why

Every push to a PR runs the whole Kani workflow, and the autoharness jobs decide how long a contributor waits for a result. In the last 30 PR runs, the two required "Verify std library using autoharness" jobs averaged 67 to 69 minutes (worst case 197). The four partitions averaged 34 to 47.

They also cost as much as the proofs themselves. Autoharness, Kani Metrics, Kani List, the Autoharness Analyzer and Build JSON take about 5 runner-hours per run, roughly the same as the eight partition jobs. From 2026-09-14 to 2026-10-14 the Kani workflow ran 183 times for PRs and pushes and only 17 times in the merge queue, so most of that cost goes to commits that never land as they are.

Proposal

Run these jobs only on merge_group and workflow_dispatch, not on pull_request or push:

• Verify std library using autoharness (ubuntu-latest, macos-latest)
• Kani Metrics (ubuntu-latest, macos-latest)
• Build JSON from logs
• Kani List
• Kani Autoharness Analyzer

if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch'

The two autoharness jobs stay required. GitHub reports a job skipped by its if: condition as successful, so a PR is not blocked during review, and the merge queue still runs autoharness before anything reaches main. Metrics, List, the Analyzer and Build JSON only report numbers, so nothing gates on them.

At last month's rate, these jobs would run about 17 times a month instead of about 200, and PR feedback would be bounded by the partitions instead of by autoharness.

Risk

• Autoharness failures surface later. On Merge subtree update for toolchain nightly-2026-09-25 #687 it found 21 contract failures that every partition passed: three Step contracts that a subtree merge had moved onto the wrong functions, and missing or weak contracts on the NonZero, AsciiChar and char step impls. Under this proposal a PR like that passes review and is removed from the queue a few hours later. For PRs that add or move contracts, the author or a reviewer can run the workflow on the branch with workflow_dispatch before queueing.
• The merge queue times out after 4 hours. The slowest autoharness run in the sample took 197 minutes, and macOS runners sometimes queue for a while before starting, so the timeout may need raising.
• The Kani List and Analyzer summaries stop appearing on PRs.

Where input is wanted

• Is finding autoharness failures at merge time acceptable, or should subtree sync PRs, which touch the whole library, keep running autoharness on the PR?
• Should we raise the merge queue timeout above 4 hours?