From 4676dc4578189e163844767e30e1451a5cc8dda1 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 3 Aug 2026 13:37:27 +0100
Subject: [PATCH] =?UTF-8?q?fix(ci):=20repair=20the=20Coq=20gate=20on=20mai?=
 =?UTF-8?q?n=20=E2=80=94=20coqc=20not=20found?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

PR #709 merged the pre-fix revision of the workflow, so the gate has been
failing on main since ed4e223 with `coqc: not found`. The fix existed on the
PR branch (af7c38c) but was not included in the squash.

Two causes, both reproduced locally against the digest-pinned image:

1. The coqorg images install Coq into an opam switch owned by the `coq` user
   and expose it via an ENTRYPOINT wrapper. GitHub Actions overrides the
   entrypoint for job containers, so the wrapper never runs and `coqc` is not
   on PATH. Now resolved explicitly — globbed rather than hard-coded so an
   image bump cannot silently break it, and failing loudly if not found.

2. GitHub fell back to `sh -e {0}` (dash), which rejects `set -o pipefail`
   and the bash-only string operations the gate uses. The image ships bash
   5.2, so the shell is now declared explicitly.

Verified green via workflow_dispatch on the branch before this commit:
prover 8.20.1, 20/20 proofs checked, completeness guard passed, no axioms.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---
 .github/workflows/coq-proof-gate.yml | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/.github/workflows/coq-proof-gate.yml b/.github/workflows/coq-proof-gate.yml
index 819414ae..88fb8c65 100644
--- a/.github/workflows/coq-proof-gate.yml
+++ b/.github/workflows/coq-proof-gate.yml
@@ -28,6 +28,13 @@ jobs:
   coq-proofs:
     runs-on: ubuntu-latest
     timeout-minutes: 30
+    # The image ships bash 5.2, but GitHub fell back to `sh -e {0}` (dash) on
+    # the first run, which rejects `set -o pipefail` and the bash-only string
+    # operations below. Declare the shell explicitly rather than depending on
+    # the runner's detection.
+    defaults:
+      run:
+        shell: bash
     container:
       # coqorg/coq:8.20 — pinned by digest. `formal/README.adoc` documents 8.18;
       # the corpus was verified to check clean on 8.20.1 (deprecation warnings
@@ -37,6 +44,23 @@ jobs:
     steps:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
 
+      # The coqorg images install Coq into an opam switch owned by the `coq`
+      # user and put it on PATH via an ENTRYPOINT wrapper. GitHub Actions
+      # overrides the entrypoint for job containers, so that wrapper never
+      # runs and `coqc` is not on PATH — the switch has to be added by hand.
+      # Globbed rather than hard-coded so an image bump does not silently
+      # break the gate; fails loudly if the switch cannot be located.
+      - name: Put the image's opam switch on PATH
+        run: |
+          set -euo pipefail
+          sw="$(ls -d /home/coq/.opam/*/bin 2>/dev/null | head -1 || true)"
+          if [ -z "$sw" ] || [ ! -x "$sw/coqc" ]; then
+            echo "::error::could not locate coqc in the image's opam switch"
+            exit 1
+          fi
+          echo "$sw" >> "$GITHUB_PATH"
+          echo "added $sw to PATH"
+
       - name: Record prover version
         run: coqc --version