From 3472e70d06022b172579c4d2e63ea22b5224c0ab Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 30 May 2026 21:41:04 +0100 Subject: [PATCH] feat(coq-build): always-on aggregator gate (closes #244 path-filter blocker) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The `Coq build — formal/_CoqProject` check shipped in #231 is path-filtered to `formal/**` + the workflow file itself. Once the Base ruleset (id 14285235) gains a `required_status_checks` rule naming that context — the #244 owner action — every PR that does NOT touch `formal/**` would leave the check "expected but not reported" and be blocked indefinitely. The required-check machinery does not treat a not-triggered workflow as passing. Fix: refactor to the always-on aggregator pattern. The single new context that goes into the ruleset is `coq-build-gate`; it ALWAYS runs and reports the right verdict regardless of which paths changed. Mechanics --------- 1. Drop `paths:` from `on:`. The workflow now triggers on every PR and every push to main. 2. New `detect-relevant-changes` job diffs against the PR base (`github.event.pull_request.base.sha` / `github.event.before`) and sets `outputs.relevant = true|false` using the same path list that lived in the on-trigger (`formal/` + this workflow). 3. The existing `coq-build` job gains `needs: detect-relevant-changes` + `if: needs.detect-relevant-changes.outputs.relevant == 'true'`. It skips cleanly on irrelevant PRs (no container pull, no `coq_makefile` run, no `Print Assumptions` call). 4. New `coq-build-gate` job (`if: always()`, `needs: [detect, coq-build]`): - SUCCESS immediately if RELEVANT != 'true'. - FAILURE if detect-relevant-changes itself didn't succeed (fail-safe — we never confirmed relevance). - SUCCESS iff `coq-build.result == 'success'` on a relevant change. - FAILURE otherwise (any non-success from coq-build). The coq-build job itself is untouched: same container, same Coq 8.18 image, same `coq_makefile -f _CoqProject -o build.mk && make`, same `Print Assumptions` audit of the four Phase D theorems (`preservation_l1`, `preservation_l2_via_l1`, `preservation_l2_app_eff_beta_linear`, `preservation_l2_app_eff_beta_ground_nonlinear`). Ruleset migration (post-merge, separate operation) -------------------------------------------------- Once this PR is green on main, the #244 owner action becomes: gh api -X PUT repos/hyperpolymath/ephapax/rulesets/14285235 \ --input /tmp/patch.json where `patch.json` appends a `required_status_checks` rule listing the context `coq-build-gate` (NOT `Coq build — formal/_CoqProject`, because that one skips on irrelevant PRs and would re-introduce the exact "expected but not reported" block this PR exists to avoid). Prior-art --------- panic-attack#90 (already landed) applied the same pattern to `chapel-ci.yml`. That PR's body documents the same mechanics for the six chapel-ci jobs; this PR is the single-job variant of the same refactor. Test plan --------- - [ ] `coq-build-gate` green on this PR (path is `.github/workflows/coq-build.yml` → relevant=true → coq-build runs → gate aggregates). - [ ] After merge, a no-formal-change PR shows `coq-build-gate` green while `coq-build` is "Skipped". - [ ] After merge, the #244 owner action switches the Base ruleset's required context from absent → `coq-build-gate`. - [ ] An intentional broken-build PR (touching `formal/`) shows `coq-build-gate` red and admin-merge blocked. Refs ---- - #244 — owner action this PR unblocks - #231 — `coq-build.yml` ships - #236 — EACCES container fix - #243 — Print Assumptions audit expansion - panic-attack#90 — prior-art (chapel-ci aggregator) --- .github/workflows/coq-build.yml | 90 ++++++++++++++++++++++++++++++--- 1 file changed, 84 insertions(+), 6 deletions(-) diff --git a/.github/workflows/coq-build.yml b/.github/workflows/coq-build.yml index df8e17c..c2eb6e1 100644 --- a/.github/workflows/coq-build.yml +++ b/.github/workflows/coq-build.yml @@ -18,19 +18,26 @@ # results (preservation_l1 at L1; preservation_l2_via_l1 plus the two # β-case lemmas at L2) so any new `Admitted.` / `Axiom` slippage shows # up as a diff in the workflow output. +# +# **Why an aggregator gate?** The `coq-build` job is path-filtered: it +# only does real work when `formal/**` or this workflow file changes. +# But path-filtered workflows that don't trigger leave required status +# checks "expected but not reported" — which would block unrelated PRs +# from merging once this check is in the Base ruleset (#244). Solution: +# a single `coq-build-gate` job that ALWAYS runs and aggregates. The +# ruleset requires only the gate. The gate reports: +# - SUCCESS immediately if no formal-relevant paths changed. +# - SUCCESS if `coq-build` succeeded on a relevant change. +# - FAILURE if `coq-build` failed. +# +# Prior-art (same pattern): panic-attack#90. name: Coq Build (formal/) on: pull_request: - paths: - - 'formal/**' - - '.github/workflows/coq-build.yml' push: branches: [main] - paths: - - 'formal/**' - - '.github/workflows/coq-build.yml' permissions: contents: read @@ -40,8 +47,42 @@ concurrency: cancel-in-progress: true jobs: + detect-relevant-changes: + name: detect-relevant-changes + runs-on: ubuntu-latest + outputs: + relevant: ${{ steps.f.outputs.relevant }} + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + with: + fetch-depth: 2 + - id: f + name: Detect formal-relevant paths + run: | + set -euo pipefail + BASE="${{ github.event.pull_request.base.sha || github.event.before }}" + if [[ -z "$BASE" || "$BASE" == "0000000000000000000000000000000000000000" ]]; then + # First push or detached state — be safe and run the full gate. + echo "relevant=true" >> "$GITHUB_OUTPUT" + echo "detect: BASE missing/zero — treating as relevant" + exit 0 + fi + git fetch origin "$BASE" --depth=1 2>/dev/null || true + CHANGED=$(git diff --name-only "$BASE" HEAD || true) + echo "Changed files:" + echo "$CHANGED" + if echo "$CHANGED" | grep -qE '^(formal/|\.github/workflows/coq-build\.yml$)'; then + echo "relevant=true" >> "$GITHUB_OUTPUT" + echo "detect: formal-relevant paths changed — running gate" + else + echo "relevant=false" >> "$GITHUB_OUTPUT" + echo "detect: no formal-relevant paths — gate skipped via if-guard" + fi + coq-build: name: Coq build — formal/_CoqProject + needs: detect-relevant-changes + if: needs.detect-relevant-changes.outputs.relevant == 'true' runs-on: ubuntu-latest # coq:8.18 matches the toolchain pinned by formal/Justfile and the # local developer setup. Pin to a digest later once a stable @@ -98,3 +139,40 @@ jobs: Print Assumptions preservation_l2_app_eff_beta_linear. Print Assumptions preservation_l2_app_eff_beta_ground_nonlinear. EOF + + # Always-on aggregator. This is the ONLY job listed in the Base ruleset's + # required_status_checks rule (#244). If detect-relevant-changes determined + # nothing in this PR touches formal-relevant paths, the gate passes + # immediately (the underlying `coq-build` job skips via its `if:` guard). + # If a relevant change is present, the gate inspects `coq-build.result` and + # only passes when it returned `success`. + coq-build-gate: + name: coq-build-gate + needs: [detect-relevant-changes, coq-build] + if: always() + runs-on: ubuntu-latest + steps: + - name: Aggregate coq-build results + env: + RELEVANT: ${{ needs.detect-relevant-changes.outputs.relevant }} + R_DETECT: ${{ needs.detect-relevant-changes.result }} + R_BUILD: ${{ needs.coq-build.result }} + run: | + set -euo pipefail + echo "detect-relevant-changes.outputs.relevant=$RELEVANT" + echo "detect-relevant-changes.result=$R_DETECT" + echo "coq-build.result=$R_BUILD" + if [[ "$RELEVANT" != "true" ]]; then + echo "coq-build-gate: SKIP (no formal-relevant paths changed) → PASS" + exit 0 + fi + # If detect itself failed, we never confirmed relevance — fail safe. + if [[ "$R_DETECT" != "success" ]]; then + echo "coq-build-gate: detect-relevant-changes did not succeed → FAIL" + exit 1 + fi + if [[ "$R_BUILD" != "success" ]]; then + echo "coq-build-gate: coq-build did not succeed (got '$R_BUILD') → FAIL" + exit 1 + fi + echo "coq-build-gate: coq-build green → PASS"