|
| 1 | +# SPDX-License-Identifier: MPL-2.0 |
| 2 | +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | +# |
| 4 | +# coq-build.yml — type-checks every module in `formal/` (Rocq/Coq). |
| 5 | +# |
| 6 | +# Standing directive [[feedback_proof_pr_build_oracle_is_only_truth]]: |
| 7 | +# for proof PRs, the toolchain build is the ONLY merge oracle. Until |
| 8 | +# this workflow existed, the rule relied entirely on human discipline |
| 9 | +# — admin-merge could and did land a broken main when PR #224 |
| 10 | +# duplicated `tfuneff_lambda_retype_l1_m` and all 17 unrelated |
| 11 | +# governance/scanner checks went green (see #227, hotfix #226). |
| 12 | +# |
| 13 | +# This is now a HARD GATE: any PR (or push to main) that breaks |
| 14 | +# `coq_makefile`-driven compilation of `formal/_CoqProject` fails |
| 15 | +# here BEFORE the admin-merge button is reachable for the auto-bot. |
| 16 | +# |
| 17 | +# The job also `Print Assumptions`-checks the four Phase D top-level |
| 18 | +# results (preservation_l1 at L1; preservation_l2_via_l1 plus the two |
| 19 | +# β-case lemmas at L2) so any new `Admitted.` / `Axiom` slippage shows |
| 20 | +# up as a diff in the workflow output. |
| 21 | +# |
| 22 | +# **Why an aggregator gate?** The `coq-build` job is path-filtered: it |
| 23 | +# only does real work when `formal/**` or this workflow file changes. |
| 24 | +# But path-filtered workflows that don't trigger leave required status |
| 25 | +# checks "expected but not reported" — which would block unrelated PRs |
| 26 | +# from merging once this check is in the Base ruleset (#244). Solution: |
| 27 | +# a single `coq-build-gate` job that ALWAYS runs and aggregates. The |
| 28 | +# ruleset requires only the gate. The gate reports: |
| 29 | +# - SUCCESS immediately if no formal-relevant paths changed. |
| 30 | +# - SUCCESS if `coq-build` succeeded on a relevant change. |
| 31 | +# - FAILURE if `coq-build` failed. |
| 32 | +# |
| 33 | +# Prior-art (same pattern): panic-attack#90. |
| 34 | + |
| 35 | +name: Coq Build (formal/) |
| 36 | + |
| 37 | +on: |
| 38 | + pull_request: |
| 39 | + push: |
| 40 | + branches: [main] |
| 41 | + |
| 42 | +permissions: |
| 43 | + contents: read |
| 44 | + |
| 45 | +concurrency: |
| 46 | + group: ${{ github.workflow }}-${{ github.ref }} |
| 47 | + cancel-in-progress: true |
| 48 | + |
| 49 | +jobs: |
| 50 | + detect-relevant-changes: |
| 51 | + name: detect-relevant-changes |
| 52 | + runs-on: ubuntu-latest |
| 53 | + timeout-minutes: 10 |
| 54 | + outputs: |
| 55 | + relevant: ${{ steps.f.outputs.relevant }} |
| 56 | + steps: |
| 57 | + - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 |
| 58 | + with: |
| 59 | + fetch-depth: 2 |
| 60 | + - id: f |
| 61 | + name: Detect formal-relevant paths |
| 62 | + run: | |
| 63 | + set -euo pipefail |
| 64 | + BASE="${{ github.event.pull_request.base.sha || github.event.before }}" |
| 65 | + if [[ -z "$BASE" || "$BASE" == "0000000000000000000000000000000000000000" ]]; then |
| 66 | + # First push or detached state — be safe and run the full gate. |
| 67 | + echo "relevant=true" >> "$GITHUB_OUTPUT" |
| 68 | + echo "detect: BASE missing/zero — treating as relevant" |
| 69 | + exit 0 |
| 70 | + fi |
| 71 | + git fetch origin "$BASE" --depth=1 2>/dev/null || true |
| 72 | + CHANGED=$(git diff --name-only "$BASE" HEAD || true) |
| 73 | + echo "Changed files:" |
| 74 | + echo "$CHANGED" |
| 75 | + if echo "$CHANGED" | grep -qE '^(formal/|\.github/workflows/coq-build\.yml$)'; then |
| 76 | + echo "relevant=true" >> "$GITHUB_OUTPUT" |
| 77 | + echo "detect: formal-relevant paths changed — running gate" |
| 78 | + else |
| 79 | + echo "relevant=false" >> "$GITHUB_OUTPUT" |
| 80 | + echo "detect: no formal-relevant paths — gate skipped via if-guard" |
| 81 | + fi |
| 82 | +
|
| 83 | + coq-build: |
| 84 | + name: Coq build — formal/_CoqProject |
| 85 | + needs: detect-relevant-changes |
| 86 | + if: needs.detect-relevant-changes.outputs.relevant == 'true' |
| 87 | + runs-on: ubuntu-latest |
| 88 | + timeout-minutes: 30 |
| 89 | + # Coq 8.18 via Ubuntu 24.04 noble apt (coq 8.18.0+dfsg) exactly |
| 90 | + # matches the toolchain pinned by formal/Justfile and the local |
| 91 | + # developer setup. |
| 92 | + # |
| 93 | + # Why not the `coqorg/coq:8.18` container? Previously this job ran |
| 94 | + # it with `--user root` to dodge the EACCES from checkout writing |
| 95 | + # to a runner-user-owned /__w mount. But the image only configures |
| 96 | + # `coqc` on the non-root `coq` user's PATH (via opam env in their |
| 97 | + # .profile). With `--user root`, no opam env → `coqc: not found` → |
| 98 | + # exit 127 immediately at the version step. Several proof PRs were |
| 99 | + # silently blocked while main stayed green (path-filter skipped |
| 100 | + # main pushes that didn't touch formal/). See the proven 37s |
| 101 | + # pattern in [[reference_coqorg_image_apt_coq_simpler]] used by |
| 102 | + # verisimdb#87. |
| 103 | + |
| 104 | + steps: |
| 105 | + - name: Checkout repository |
| 106 | + uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 |
| 107 | + |
| 108 | + - name: Install Coq 8.18 (noble apt) |
| 109 | + run: | |
| 110 | + sudo apt-get update -qq |
| 111 | + sudo apt-get install -y --no-install-recommends coq |
| 112 | +
|
| 113 | + - name: Coq version (provenance) |
| 114 | + run: | |
| 115 | + coqc --version |
| 116 | + coq_makefile --help 2>&1 | head -1 || true |
| 117 | +
|
| 118 | + - name: Build formal/ via coq_makefile (the merge-oracle command) |
| 119 | + working-directory: formal |
| 120 | + run: | |
| 121 | + # Mirrors `formal/Justfile`'s `all` recipe: |
| 122 | + # coq_makefile -f _CoqProject -o build.mk |
| 123 | + # make -f build.mk |
| 124 | + # (Plain `make` instead of `just` so we don't need `just` in |
| 125 | + # the container — the recipe is two lines.) |
| 126 | + coq_makefile -f _CoqProject -o build.mk |
| 127 | + make -f build.mk |
| 128 | +
|
| 129 | + - name: Print Assumptions of Phase D theorems |
| 130 | + working-directory: formal |
| 131 | + run: | |
| 132 | + # Surfaces any new Admitted / Axiom additions feeding into |
| 133 | + # the four Phase D top-level results. A diff in this output |
| 134 | + # between PRs is the canonical "did this PR introduce a new |
| 135 | + # admit" signal. |
| 136 | + # preservation_l1 (Semantics_L1.v) |
| 137 | + # preservation_l2_via_l1 (TypingL2.v) |
| 138 | + # preservation_l2_app_eff_beta_linear (TypingL2.v, #228) |
| 139 | + # preservation_l2_app_eff_beta_ground_nonlinear (TypingL2.v, #233) |
| 140 | + # Single coqtop session amortises ML startup across four prints. |
| 141 | + coqtop -R . Ephapax 2>&1 <<'EOF' | tail -160 |
| 142 | + From Ephapax Require Import Semantics_L1. |
| 143 | + From Ephapax Require Import TypingL2. |
| 144 | + Print Assumptions preservation_l1. |
| 145 | + Print Assumptions preservation_l2_via_l1. |
| 146 | + Print Assumptions preservation_l2_app_eff_beta_linear. |
| 147 | + Print Assumptions preservation_l2_app_eff_beta_ground_nonlinear. |
| 148 | + EOF |
| 149 | +
|
| 150 | + # Always-on aggregator. This is the ONLY job listed in the Base ruleset's |
| 151 | + # required_status_checks rule (#244). If detect-relevant-changes determined |
| 152 | + # nothing in this PR touches formal-relevant paths, the gate passes |
| 153 | + # immediately (the underlying `coq-build` job skips via its `if:` guard). |
| 154 | + # If a relevant change is present, the gate inspects `coq-build.result` and |
| 155 | + # only passes when it returned `success`. |
| 156 | + coq-build-gate: |
| 157 | + name: coq-build-gate |
| 158 | + needs: [detect-relevant-changes, coq-build] |
| 159 | + if: always() |
| 160 | + runs-on: ubuntu-latest |
| 161 | + timeout-minutes: 10 |
| 162 | + steps: |
| 163 | + - name: Aggregate coq-build results |
| 164 | + env: |
| 165 | + RELEVANT: ${{ needs.detect-relevant-changes.outputs.relevant }} |
| 166 | + R_DETECT: ${{ needs.detect-relevant-changes.result }} |
| 167 | + R_BUILD: ${{ needs.coq-build.result }} |
| 168 | + run: | |
| 169 | + set -euo pipefail |
| 170 | + echo "detect-relevant-changes.outputs.relevant=$RELEVANT" |
| 171 | + echo "detect-relevant-changes.result=$R_DETECT" |
| 172 | + echo "coq-build.result=$R_BUILD" |
| 173 | + if [[ "$RELEVANT" != "true" ]]; then |
| 174 | + echo "coq-build-gate: SKIP (no formal-relevant paths changed) → PASS" |
| 175 | + exit 0 |
| 176 | + fi |
| 177 | + # If detect itself failed, we never confirmed relevance — fail safe. |
| 178 | + if [[ "$R_DETECT" != "success" ]]; then |
| 179 | + echo "coq-build-gate: detect-relevant-changes did not succeed → FAIL" |
| 180 | + exit 1 |
| 181 | + fi |
| 182 | + if [[ "$R_BUILD" != "success" ]]; then |
| 183 | + echo "coq-build-gate: coq-build did not succeed (got '$R_BUILD') → FAIL" |
| 184 | + exit 1 |
| 185 | + fi |
| 186 | + echo "coq-build-gate: coq-build green → PASS" |
0 commit comments