ci: add Coq build oracle workflow (closes #227) (#231)

## Summary

Closes #227 — adds `.github/workflows/coq-build.yml` so the standing
directive "for proof PRs, the toolchain build is the ONLY merge oracle"
is machine-enforced.

## Today's incident motivating this

PR #224 admin-merged 7 min after PR #223; all 17 governance/scanner
checks were green; `coqc` was not run; main broke with
`tfuneff_lambda_retype_l1_m already exists`. Hotfix #226 restored
compilation; #227 was filed in parallel asking for the oracle gap to be
closed at workflow-level.

## What the workflow does

- Triggers on PR + push-to-main, scoped to `formal/**` paths (only fires
when proofs change).
- Container: `coqorg/coq:8.18` (matches `formal/Justfile`'s pinned
toolchain).
- Builds via the same recipe `formal/Justfile all` uses:
  ```
  coq_makefile -f _CoqProject -o build.mk
  make -f build.mk
  ```
- After a clean build, runs `Print Assumptions preservation_l2_via_l1`
and prints the tail. Any new `Admitted.` / `Axiom` slippage shows as a
workflow-output diff.

## What this PR does NOT do

- Branch-protection / required-check designation is **owner's call**
(admin-only in GitHub Settings). The workflow file ships first so the
check identity exists; one green run on main lets you mark it required.

## Test plan

- [ ] First CI run on this PR builds `formal/_CoqProject` clean
- [ ] `Print Assumptions preservation_l2_via_l1` output appears in the
log
- [ ] (Manual, post-merge) Mark `Coq build — formal/_CoqProject` as a
required check

## Refs

- Closes #227
- Refs #229 (sibling — the broader "no Coq oracle" surface this closes)
- Refs #226 (hotfix that motivated this)

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/coq-build.yml

@@ -0,0 +1,80 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# coq-build.yml — type-checks every module in `formal/` (Rocq/Coq).
+#
+# Standing directive [[feedback_proof_pr_build_oracle_is_only_truth]]:
+# for proof PRs, the toolchain build is the ONLY merge oracle. Until
+# this workflow existed, the rule relied entirely on human discipline
+# — admin-merge could and did land a broken main when PR #224
+# duplicated `tfuneff_lambda_retype_l1_m` and all 17 unrelated
+# governance/scanner checks went green (see #227, hotfix #226).
+#
+# This is now a HARD GATE: any PR (or push to main) that breaks
+# `coq_makefile`-driven compilation of `formal/_CoqProject` fails
+# here BEFORE the admin-merge button is reachable for the auto-bot.
+#
+# The job also `Print Assumptions`-checks the load-bearing top-level
+# theorem `preservation_l2_via_l1` (TypingL2.v) so any new `Admitted.`
+# / `Axiom` slippage shows up as a diff in the workflow output.
+
+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
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  coq-build:
+    name: Coq build — formal/_CoqProject
+    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
+    # known-good image is decided on; for now the floating tag mirrors
+    # `make` semantics — "what the maintainer's machine has".
+    container:
+      image: coqorg/coq:8.18
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
+
+      - name: Coq version (provenance)
+        run: |
+          coqc --version
+          coq_makefile --help 2>&1 | head -1 || true
+
+      - name: Build formal/ via coq_makefile (the merge-oracle command)
+        working-directory: formal
+        run: |
+          # Mirrors `formal/Justfile`'s `all` recipe:
+          #   coq_makefile -f _CoqProject -o build.mk
+          #   make -f build.mk
+          # (Plain `make` instead of `just` so we don't need `just` in
+          # the container — the recipe is two lines.)
+          coq_makefile -f _CoqProject -o build.mk
+          make -f build.mk
+
+      - name: Print Assumptions of load-bearing theorem
+        working-directory: formal
+        run: |
+          # Surfaces any new Admitted / Axiom additions feeding into
+          # preservation_l2_via_l1 (Phase D top-level result). A diff
+          # in this output between PRs is the canonical "did this PR
+          # introduce a new admit" signal.
+          echo 'From Ephapax Require Import TypingL2. Print Assumptions preservation_l2_via_l1.' \
+            | coqtop -R . Ephapax 2>&1 | tail -40