feat(coq-build): always-on aggregator gate (closes #244 path-filter blocker)

[hyperpolymath]

Summary

Closes the path-filter blocker that prevents #244 (the owner action that
adds required_status_checks to the Base ruleset on main) from landing
without collateral damage.

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, every
PR that does NOT touch formal/** would leave the check "expected but not
reported" and be blocked indefinitely.

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. on: block drops the paths: filter — workflow 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.
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).
   • SUCCESS iff coq-build.result == 'success' on a relevant change.
   • FAILURE otherwise.

The coq-build job itself is untouched: same coqorg/coq:8.18 container
with --user root, 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:

# Append required_status_checks naming `coq-build-gate` (NOT the underlying
# `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).
gh api -X PUT repos/hyperpolymath/ephapax/rulesets/14285235 --input /tmp/patch.json

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 ci: mark 'Coq build — formal/_CoqProject' as REQUIRED in main ruleset (owner action) #244 owner action switches the Base ruleset's
  required context from absent to coq-build-gate.
• An intentional broken-build PR (touching formal/) shows
  coq-build-gate red and admin-merge blocked.

Prior-art

panic-attack#90 (already landed) applied the same pattern to chapel-ci.yml.
This PR is the single-job variant of the same refactor.

Refs

• ci: mark 'Coq build — formal/_CoqProject' as REQUIRED in main ruleset (owner action) #244 — owner action this PR unblocks
• ci: add Coq build oracle workflow (closes #227) #231 — coq-build.yml ships
• ci(coq-build): run coqorg/coq container as root to fix actions/checkout EACCES #236 — EACCES container fix
• ci(coq-build): expand Print Assumptions to all four Phase D theorems #243 — Print Assumptions audit expansion
• panic-attack#90 — prior-art (chapel-ci aggregator)

Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 73 issues detected

Severity	Count
🔴 Critical	9
🟠 High	16
🟡 Medium	48

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in abi-verify.yml",
    "type": "missing_timeout_minutes",
    "file": "abi-verify.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in coq-build.yml",
    "type": "missing_timeout_minutes",
    "file": "coq-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in coq-build.yml",
    "type": "missing_timeout_minutes",
    "file": "coq-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in coq-build.yml",
    "type": "missing_timeout_minutes",
    "file": "coq-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "missing_timeout_minutes",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "missing_timeout_minutes",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "missing_timeout_minutes",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in rust-ci.yml",
    "type": "missing_timeout_minutes",
    "file": "rust-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence