From be41a08e4fdffb23ef6cf685588c09786a5dec54 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Mon, 19 Oct 2026 00:09:14 +0700 Subject: [PATCH 1/4] ci: per-PR cancel groups on 9 uncancelled workflows, and a provable paths filter on dupe-ratchet (Closes #10552) Measured 2026-10-18 17:03Z: a PR push starts a median of 24 runs and 326 runs were queued. Ten workflows had no concurrency block; nine now get -. Where the workflow also runs on push it cancels only on pull_request events, so a master push run is never cancelled. Skipped: auto-merge-ready-prs (cancel-in-progress: false is deliberate), pr-budget (mutates PR state, listens to converted_to_draft) and t27b-native (already cancels per PR). dupe-ratchet gains a pull_request paths filter: specs/**, its script, its ledger and its own workflow, which is everything tools/dupe_scan.py reads (it walks specs/ for *.t27 and reads tools/duplicate_bodies_baseline.txt; its self-test builds a temp tree). No required check (validate, check-linked-issue, parse-ratchet, own-language) is touched. Foreign-line budget (diff net 0, 30 added / 30 deleted): the offset is the boilerplate copied into build-paper, catalog-count-gate and coq-kernel (branch-filter note) and into build-paper, coq-kernel and seal-staleness-warn (workflow_dispatch note). The rule they restate lives in scripts/ci/check_pr_branch_filters.py and `tri gates unmeasured`; no gate reads those comments. Co-Authored-By: Claude Sonnet 5.5 --- .github/workflows/build-paper.yml | 12 +++--------- .github/workflows/catalog-count-gate.yml | 8 +++----- .github/workflows/conformance-integrity-gate.yml | 3 +++ .github/workflows/coq-kernel.yml | 12 +++--------- .github/workflows/coq-proofs.yml | 3 +++ .github/workflows/dupe-ratchet.yml | 6 +++--- .github/workflows/gf-wide-conformance.yml | 3 +++ .github/workflows/gf16-conformance.yml | 3 +++ .github/workflows/pack-index-consistency-gate.yml | 3 +++ .github/workflows/seal-staleness-warn.yml | 7 +++---- 10 files changed, 30 insertions(+), 30 deletions(-) diff --git a/.github/workflows/build-paper.yml b/.github/workflows/build-paper.yml index 54b4b4ec7a..e3e6a4887a 100644 --- a/.github/workflows/build-paper.yml +++ b/.github/workflows/build-paper.yml @@ -6,19 +6,13 @@ on: paths: - 'docs/WHITEPAPER/**' pull_request: - # No `branches:` filter on pull_request, deliberately. A branch filter makes - # this gate silent on any PR whose base is not listed -- a stacked PR then - # shows a green check list that a master-based PR would not get. Enforced by - # scripts/ci/check_pr_branch_filters.py. The `push` filter below, where one - # exists, is left alone: restricting post-merge runs is a cost decision. paths: - 'docs/WHITEPAPER/**' - # Without this the missing reading cannot be taken on purpose: a gate with - # a `paths:` filter that nothing has matched in months is unmeasured, not - # passing, and there was no way to fire it at the default branch and find - # out. `tri gates unmeasured` reports the gap; this is what closes it. workflow_dispatch: +concurrency: + group: build-paper-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: ${{ github.event_name == 'pull_request' }} jobs: build-paper: runs-on: ubuntu-latest diff --git a/.github/workflows/catalog-count-gate.yml b/.github/workflows/catalog-count-gate.yml index adc7ac5a93..837606a1d5 100644 --- a/.github/workflows/catalog-count-gate.yml +++ b/.github/workflows/catalog-count-gate.yml @@ -19,11 +19,6 @@ name: Catalog Count Invariant (CI-01) on: pull_request: - # No `branches:` filter on pull_request, deliberately. A branch filter makes - # this gate silent on any PR whose base is not listed -- a stacked PR then - # shows a green check list that a master-based PR would not get. Enforced by - # scripts/ci/check_pr_branch_filters.py. The `push` filter below, where one - # exists, is left alone: restricting post-merge runs is a cost decision. paths: - "specs/numeric/formats_catalog.t27" - "tools/gen_formats_catalog.py" @@ -42,6 +37,9 @@ on: - ".github/workflows/catalog-count-gate.yml" workflow_dispatch: +concurrency: + group: catalog-count-gate-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: true jobs: count-invariant: runs-on: ubuntu-latest diff --git a/.github/workflows/conformance-integrity-gate.yml b/.github/workflows/conformance-integrity-gate.yml index 9275d987e8..634544dedc 100644 --- a/.github/workflows/conformance-integrity-gate.yml +++ b/.github/workflows/conformance-integrity-gate.yml @@ -31,6 +31,9 @@ on: permissions: contents: read +concurrency: + group: conformance-integrity-gate-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: ${{ github.event_name == 'pull_request' }} jobs: integrity-gate: runs-on: ubuntu-latest diff --git a/.github/workflows/coq-kernel.yml b/.github/workflows/coq-kernel.yml index 858a815387..490b40ec80 100644 --- a/.github/workflows/coq-kernel.yml +++ b/.github/workflows/coq-kernel.yml @@ -16,11 +16,6 @@ on: # no-op and no run would notice, because nothing under coq/ changed. - 'bootstrap/src/phi_f64_literals.rs' pull_request: - # No `branches:` filter on pull_request, deliberately. A branch filter makes - # this gate silent on any PR whose base is not listed -- a stacked PR then - # shows a green check list that a master-based PR would not get. Enforced by - # scripts/ci/check_pr_branch_filters.py. The `push` filter below, where one - # exists, is left alone: restricting post-merge runs is a cost decision. paths: - 'coq/**' - 'proofs/**' @@ -29,12 +24,11 @@ on: - 'tools/coq_outside_build_baseline.txt' - '.github/workflows/coq-kernel.yml' - 'bootstrap/src/phi_f64_literals.rs' - # Without this the missing reading cannot be taken on purpose: a gate with - # a `paths:` filter that nothing has matched in months is unmeasured, not - # passing, and there was no way to fire it at the default branch and find - # out. `tri gates unmeasured` reports the gap; this is what closes it. workflow_dispatch: +concurrency: + group: coq-kernel-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: ${{ github.event_name == 'pull_request' }} jobs: build: runs-on: ubuntu-latest diff --git a/.github/workflows/coq-proofs.yml b/.github/workflows/coq-proofs.yml index fe88a2a087..14181886a2 100644 --- a/.github/workflows/coq-proofs.yml +++ b/.github/workflows/coq-proofs.yml @@ -14,6 +14,9 @@ on: - '.github/workflows/coq-proofs.yml' workflow_dispatch: +concurrency: + group: coq-proofs-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: ${{ github.event_name == 'pull_request' }} jobs: compile-proofs: runs-on: ubuntu-latest diff --git a/.github/workflows/dupe-ratchet.yml b/.github/workflows/dupe-ratchet.yml index 6d5495b339..2e8db735b4 100644 --- a/.github/workflows/dupe-ratchet.yml +++ b/.github/workflows/dupe-ratchet.yml @@ -13,9 +13,9 @@ name: Duplicate Body Ratchet on: pull_request: - # No `branches:` filter, deliberately: a filter makes this gate silent on a - # stacked pull request, which then shows a green check list a master-based - # one would not get (scripts/ci/check_pr_branch_filters.py enforces this). + # No `branches:` filter (scripts/ci/check_pr_branch_filters.py): a stacked PR must + # not see a different check list. + paths: ["specs/**", "tools/dupe_scan.py", "tools/duplicate_bodies_baseline.txt", ".github/workflows/dupe-ratchet.yml"] push: branches: [master] workflow_dispatch: diff --git a/.github/workflows/gf-wide-conformance.yml b/.github/workflows/gf-wide-conformance.yml index 2596185e0e..9726602e87 100644 --- a/.github/workflows/gf-wide-conformance.yml +++ b/.github/workflows/gf-wide-conformance.yml @@ -40,6 +40,9 @@ on: permissions: contents: read +concurrency: + group: gf-wide-conformance-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: ${{ github.event_name == 'pull_request' }} jobs: gf-wide: runs-on: ubuntu-latest diff --git a/.github/workflows/gf16-conformance.yml b/.github/workflows/gf16-conformance.yml index 90b850ac0e..14643c913f 100644 --- a/.github/workflows/gf16-conformance.yml +++ b/.github/workflows/gf16-conformance.yml @@ -22,6 +22,9 @@ on: permissions: contents: read +concurrency: + group: gf16-conformance-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: ${{ github.event_name == 'pull_request' }} jobs: gf16-oracle: runs-on: ubuntu-latest diff --git a/.github/workflows/pack-index-consistency-gate.yml b/.github/workflows/pack-index-consistency-gate.yml index e5c6363bbc..452bf6e7f8 100644 --- a/.github/workflows/pack-index-consistency-gate.yml +++ b/.github/workflows/pack-index-consistency-gate.yml @@ -27,6 +27,9 @@ on: permissions: contents: read +concurrency: + group: pack-index-consistency-gate-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: ${{ github.event_name == 'pull_request' }} jobs: pack-index-consistency: runs-on: ubuntu-latest diff --git a/.github/workflows/seal-staleness-warn.yml b/.github/workflows/seal-staleness-warn.yml index dd2627cf3e..802a91e955 100644 --- a/.github/workflows/seal-staleness-warn.yml +++ b/.github/workflows/seal-staleness-warn.yml @@ -22,16 +22,15 @@ on: - 'bootstrap/src/compiler.rs' - 'bootstrap/stage0/FROZEN_HASH' - 'repro/numerics/nmse_manifest.json' - # Without this the missing reading cannot be taken on purpose: a gate with - # a `paths:` filter that nothing has matched in months is unmeasured, not - # passing, and there was no way to fire it at the default branch and find - # out. `tri gates unmeasured` reports the gap; this is what closes it. workflow_dispatch: # Least-privilege: this advisory job only needs to read the checked-out tree. permissions: contents: read +concurrency: + group: seal-staleness-warn-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: true jobs: warn-if-seal-stale: runs-on: ubuntu-latest From bd0cb652b4b64aede42f0a18698c569b53ffde2a Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Mon, 19 Oct 2026 10:21:35 +0700 Subject: [PATCH 2/4] census: re-bless quiet 'named a path but not quiet' 237 -> 246 (Closes #10552) The nine concurrency groups added by this PR each carry one line, group: -${{ github.event.pull_request.number || github.ref }}, which is a quiet candidate by is_quiet_candidate (it contains '||') and names a path-shaped token. Nine workflows gained one such line each, so the count moves by exactly nine and nothing else in the census moved (67 workflow files read, 33 steps in a quiet shape). No gate got quieter: the lines are workflow configuration, not run-steps. Co-Authored-By: Claude Sonnet 5.5 --- tools/census/quiet.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/census/quiet.txt b/tools/census/quiet.txt index 548b02aaa5..03f5129335 100644 --- a/tools/census/quiet.txt +++ b/tools/census/quiet.txt @@ -2,7 +2,7 @@ GATE STEPS WHOSE PASS SURVIVES THE SUBJECT GOING MISSING workflow files read 67 steps in a quiet shape 33 - named a path but not quiet 237 (--excluded prints them) + named a path but not quiet 246 (--excluded prints them) by shape: failure branch passes 14 `… 2>/dev/null … || echo PASSED` From 1fbe8fdd1f9e19af5a85453757e5e651b07e68d2 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Mon, 19 Oct 2026 14:35:22 +0700 Subject: [PATCH 3/4] census: re-bless quiet 'named a path but not quiet' 239 -> 248 (Closes #10552) Master pins 239. This branch adds nine workflow concurrency group lines, each containing '||' (github.event.pull_request.number || github.ref), so the count moves by exactly nine. No other census line moved. Co-Authored-By: Claude Sonnet 5.5 --- tools/census/quiet.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/census/quiet.txt b/tools/census/quiet.txt index d4d9b07958..4771f24a3a 100644 --- a/tools/census/quiet.txt +++ b/tools/census/quiet.txt @@ -2,7 +2,7 @@ GATE STEPS WHOSE PASS SURVIVES THE SUBJECT GOING MISSING workflow files read 67 steps in a quiet shape 33 - named a path but not quiet 239 (--excluded prints them) + named a path but not quiet 248 (--excluded prints them) by shape: failure branch passes 14 `… 2>/dev/null … || echo PASSED` From 672b54794eb9e86e544e253f98817762e02417bb Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Mon, 19 Oct 2026 17:40:03 +0700 Subject: [PATCH 4/4] census: re-bless quiet 'named a path but not quiet' 243 -> 252 (Closes #10552) Master pins 243. This branch adds nine workflow concurrency group lines, each containing '||' (github.event.pull_request.number || github.ref), so the count moves by exactly nine. No other census line moved. Co-Authored-By: Claude Sonnet 5.5 --- tools/census/quiet.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/census/quiet.txt b/tools/census/quiet.txt index d07ac34ed8..3bb974d728 100644 --- a/tools/census/quiet.txt +++ b/tools/census/quiet.txt @@ -2,7 +2,7 @@ GATE STEPS WHOSE PASS SURVIVES THE SUBJECT GOING MISSING workflow files read 67 steps in a quiet shape 35 - named a path but not quiet 243 (--excluded prints them) + named a path but not quiet 252 (--excluded prints them) by shape: failure branch passes 16 `… 2>/dev/null … || echo PASSED`