From 91f66d3ba7cae3af46dd7840d39c95e2034d1b26 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 08:01:53 +0200 Subject: [PATCH] ci(diet): path-filter the non-required heavy gates on PRs (tier A) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The agents generate more CI than the fleet absorbs: with no path-filtering, every PR — including docs- and artifact-only ones — detonates the full matrix. This economizes the NON-REQUIRED heavy workflows so a PR only runs the ones its changes can actually affect. Deadlock-safe by construction: these five checks (Coverage, Rocq+Gappa, Lean, Spar, Bazel/cascade) are NOT in branch protection's required set (verified against the API: only Clippy/Format/Verification-gate/Test×3/Kani-gate are required), so a path-skipped run never leaves a required check pending. Filters are applied to the `pull_request` trigger ONLY — every `push: main` stays UNFILTERED, so main-branch evidence/gates always run in full (the backstop, and where a too-narrow glob would still be caught). Globs err generous (a miss on a non-required check = green-PR-then-red-main, not a silent hole): bazel includes wasm/** + embedded/** (the cascade composes wasm/cm/flight); rocq includes crates/relay-math/** (drift catch — the proofs hardcode the kernel coefficients). Tier B (the real prize — Kani ×24, Test ×3, Verification-gate) touches REQUIRED checks and needs the job-level `if` + skip-safe aggregate pattern; it follows as its own carefully-validated PR. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- .github/workflows/bazel.yml | 17 +++++++++++++++++ .github/workflows/coverage.yml | 12 ++++++++++++ .github/workflows/lean.yml | 6 ++++++ .github/workflows/rocq.yml | 10 ++++++++++ .github/workflows/spar.yml | 7 +++++++ 5 files changed, 52 insertions(+) diff --git a/.github/workflows/bazel.yml b/.github/workflows/bazel.yml index ffad65a..c40c1c2 100644 --- a/.github/workflows/bazel.yml +++ b/.github/workflows/bazel.yml @@ -14,8 +14,25 @@ name: Bazel on: push: branches: [main] + # PR runs are path-filtered (CI diet): the Bazel build + Component Model + # cascade compose the flight component (wasm/cm/flight) and build the + # crates/proofs via Bazel. Generous globs — a too-narrow filter would let a + # breaking PR skip this and redden main. NON-REQUIRED check; skip never blocks + # a merge. push:main stays UNFILTERED (backstop). pull_request: branches: [main] + paths: + - 'crates/**' + - 'wasm/**' + - 'embedded/**' + - 'proofs/**' + - 'wit/**' + - '**/BUILD.bazel' + - '**/*.bzl' + - 'MODULE.bazel' + - 'MODULE.bazel.lock' + - '.bazelrc' + - '.github/workflows/bazel.yml' # Group key: head_ref (PR branch name) for pull_request events; ref # (e.g. refs/heads/main) for push events — unique per branch/PR. diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index 54c12b5..759e8b1 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -15,7 +15,19 @@ name: Coverage on: push: branches: [main] + # PR runs are path-filtered (CI diet): coverage is a Rust-source concern, so + # skip it on PRs that touch no code (docs, artifacts, wit). NON-REQUIRED + # check, so a skip never blocks a merge. The push:main trigger above stays + # UNFILTERED — every main commit still produces the DO-178C/EN-50128 coverage + # evidence record (the backstop). pull_request: + paths: + - 'crates/**' + - 'wasm/**' + - 'embedded/**' + - 'Cargo.toml' + - 'Cargo.lock' + - '.github/workflows/coverage.yml' # PRs and non-main branch pushes: cancel superseded runs. # Main pushes: never cancel — coverage artifact is the DO-178C/EN-50128 diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml index c03144d..b400627 100644 --- a/.github/workflows/lean.yml +++ b/.github/workflows/lean.yml @@ -17,8 +17,14 @@ name: Lean on: push: branches: [main] + # PR runs are path-filtered (CI diet): the Lean proofs (Lyapunov/WCET) are + # self-contained under proofs/lean. NON-REQUIRED check; skip never blocks a + # merge. push:main stays UNFILTERED (backstop). pull_request: branches: [main] + paths: + - 'proofs/lean/**' + - '.github/workflows/lean.yml' concurrency: # PRs and non-main branch pushes: cancel superseded runs. diff --git a/.github/workflows/rocq.yml b/.github/workflows/rocq.yml index 97a46c3..4c6e5ab 100644 --- a/.github/workflows/rocq.yml +++ b/.github/workflows/rocq.yml @@ -16,8 +16,18 @@ name: Rocq on: push: branches: [main] + # PR runs are path-filtered (CI diet): the Rocq/Gappa proofs cover the + # relay-math FP kernels, so re-run on proof changes AND on relay-math changes + # (drift catch — the proofs hardcode the kernel coefficients). NON-REQUIRED + # check; skip never blocks a merge. push:main stays UNFILTERED (backstop). pull_request: branches: [main] + paths: + - 'proofs/rocq/**' + - 'proofs/gappa/**' + - 'crates/relay-math/**' + - 'MODULE.bazel' + - '.github/workflows/rocq.yml' concurrency: group: rocq-${{ github.head_ref || github.ref }} diff --git a/.github/workflows/spar.yml b/.github/workflows/spar.yml index d9378b7..bec2115 100644 --- a/.github/workflows/spar.yml +++ b/.github/workflows/spar.yml @@ -10,8 +10,15 @@ name: Spar on: push: branches: [main] + # PR runs are path-filtered (CI diet): the Spar AADL->WIT drift gate concerns + # the architecture models and the generated WIT. NON-REQUIRED check; skip + # never blocks a merge. push:main stays UNFILTERED (backstop). pull_request: branches: [main] + paths: + - 'spar/**' + - 'wit/**' + - '.github/workflows/spar.yml' concurrency: # PRs / non-main pushes: cancel superseded runs. Main: never cancel — every