fix(ci): repair the Coq gate on main — coqc not found - #711
Conversation
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>
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ ApprovedExplicitly adds the opam bin path and bash shell to the Coq CI container workflow, resolving the missing coqc binary and runner fallback issues. No issues found.
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Important Your trial ends in 7 days — upgrade now to keep code review, CI analysis, auto-apply, custom automations, and more. Was this helpful? React with 👍 / 👎 | Gitar |
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
|
1 participant
Problem
The Coq Proof Gate has been failing on
mainsinceed4e223withcoqc: not found.PR #709 merged the pre-fix revision of the workflow. The fix was already
written and verified on the PR branch (
af7c38c) but was not part of thesquash, so
mainreceived the broken version.Causes (both reproduced locally against the digest-pinned image)
Entrypoint override. The
coqorgimages install Coq into an opam switchowned by the
coquser and put it onPATHvia anENTRYPOINTwrapper.GitHub Actions overrides the entrypoint for job containers, so that wrapper
never runs. The switch is now added explicitly — globbed rather than
hard-coded, so an image bump cannot silently break it, and failing loudly if
it cannot be located.
Shell fallback. GitHub used
sh -e {0}(dash), which rejectsset -o pipefailand the bash-only string operations the gate relies on.The image ships bash 5.2, so the shell is now declared explicitly rather
than left to runner detection.
Verification
Already proven green via
workflow_dispatchon the branch:All 11 steps succeeded. The same logic was also run locally inside the pinned
container under podman before first push.
🤖 Generated with Claude Code