From a4712ffb1bd055d763c899658975e7ffe0c5951f Mon Sep 17 00:00:00 2001
From: Tianshu Huang <tianshu.huang.g@gmail.com>
Date: Fri, 23 Oct 2026 11:36:46 -0700
Subject: [PATCH 1/2] 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 <tianshu.huang.g@gmail.com>
Date: Fri, 23 Oct 2026 14:19:18 -0700
Subject: [PATCH 2/2] 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