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

[hyperpolymath]

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 ci: add Coq build oracle to workflows — admin-merge can land broken main today #227
• Refs CI gap: coqc is the merge oracle for proof PRs but no CI job runs it #229 (sibling — the broader "no Coq oracle" surface this closes)
• Refs fix(L1): HOTFIX — dedupe tfuneff_lambda_retype_l1_m (main is broken) #226 (hotfix that motivated this)

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 75 issues detected

Severity	Count
🔴 Critical	13
🟠 High	13
🟡 Medium	49

⚠️ 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": "unknown",
    "file": "abi-verify.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "unknown",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "unknown",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in coq-build.yml",
    "type": "unknown",
    "file": "coq-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "unknown",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "unknown",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "unknown",
    "file": "instant-sync.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "unknown",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in rust-ci.yml",
    "type": "unknown",
    "file": "rust-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence