From b4e05702b815703187a7d13a7067104c2091ff3b Mon Sep 17 00:00:00 2001 From: Loop-Locksmith Date: Sat, 2 May 2026 12:25:40 +0000 Subject: [PATCH] ci(coq-proofs): include docs/phd/theorems/igla/ in verification MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per GENERAL's Wave-6 follow-up roadmap (issue #446 day-6 status comment). The Coq verification workflow previously only watched `trinity-clara/proofs/**`. INV-6-HybridQkGain.v landed in PR #490 under `docs/phd/theorems/igla/` but had no automatic Coq compile gate — every new theorem under that path would silently skip CI. Two surgical changes: 1. Path triggers — both `push` (main) and `pull_request` filters now also include `docs/phd/theorems/**` so any change there triggers the verification workflow. 2. New verification step — uses `coq_makefile` against the existing `docs/phd/theorems/igla/_CoqProject` (already wired with `-R trinity Trinity` / `-R igla IGLA`), then runs `make all`. Wrapped in an existence check so the step is a no-op if the _CoqProject is later removed. R5-honest disclosures: - This change ALONE does not verify INV6_HybridQkGain.v is a parseable proof — it merely points CI at the file. The first run on `main` after merge will be the binding verification. - If `coq_makefile` / `make all` discovers any unprovable goal (e.g. the residual `Axiom hybrid_gain_phi_bound` is not a contradiction but the file still has unresolved obligations), CI will go red and the scaffold will need follow-up before merge to main. Part-of: #441 Part-of: #446 Follow-up to: PR #490 (merged at ff02df9) Agent: Loop-Locksmith --- .github/workflows/coq-proofs.yml | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/.github/workflows/coq-proofs.yml b/.github/workflows/coq-proofs.yml index 39e8795542..0e1e442b86 100644 --- a/.github/workflows/coq-proofs.yml +++ b/.github/workflows/coq-proofs.yml @@ -13,12 +13,14 @@ on: branches: [main] paths: - 'trinity-clara/proofs/**' + - 'docs/phd/theorems/**' # invariants.rs migrated to gHashTag/trios-trainer-igla per L-T1+L-T3 - '.github/workflows/coq-proofs.yml' pull_request: branches: [main] paths: - 'trinity-clara/proofs/**' + - 'docs/phd/theorems/**' concurrency: group: coq-${{ github.ref }} @@ -65,6 +67,23 @@ jobs: coqc trinity-clara/proofs/igla/igla_asha_bound.v echo "✅ INV-2 OK: asha_champion_survives" + # --- docs/phd/theorems/igla/* via _CoqProject ------------- + # Added for INV-6-HybridQkGain (#441, PR #490) and future + # IGLA_* theorems under docs/phd/theorems/igla/. Respects + # the local _CoqProject's -R trinity Trinity / -R igla IGLA + # layout so CorePhi, AlphaPhi, FormulaEval can be imported. + echo "=== docs/phd/theorems/igla/* (Trinity anchor files) ===" + if [ -f docs/phd/theorems/igla/_CoqProject ]; then + cd docs/phd/theorems + # coq_makefile + make-all respects _CoqProject's load paths + coq_makefile -f igla/_CoqProject -o igla/Makefile + make -f igla/Makefile all + cd - + echo "✅ docs/phd/theorems/igla/* OK" + else + echo "(no _CoqProject under docs/phd/theorems/igla — skipped)" + fi + echo "=== ALL PROOFS VERIFIED ===" - name: Check no Admitted in proofs (L-R14 strict)