Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 19 additions & 14 deletions .github/workflows/coq-build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -84,25 +84,30 @@ jobs:
needs: detect-relevant-changes
if: needs.detect-relevant-changes.outputs.relevant == 'true'
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
# actions/checkout's post-step writes to /__w/_temp/_runner_file_commands
# via Node fs.writeFileSync. The coqorg/coq image defaults to the
# non-root `coq` user (UID 1000), but the runner mounts /__w as the
# host runner user — EACCES until checkout's saveState. Running the
# container as root keeps the workspace-shared paths writable while
# leaving the in-container build untouched (root in container is
# still mapped to the runner host's runner user, not host-root).
options: --user root
# Coq 8.18 via Ubuntu 24.04 noble apt (coq 8.18.0+dfsg) exactly
# matches the toolchain pinned by formal/Justfile and the local
# developer setup.
#
# Why not the `coqorg/coq:8.18` container? Previously this job ran
# it with `--user root` to dodge the EACCES from checkout writing
# to a runner-user-owned /__w mount. But the image only configures
# `coqc` on the non-root `coq` user's PATH (via opam env in their
# .profile). With `--user root`, no opam env → `coqc: not found` →
# exit 127 immediately at the version step. Several proof PRs were
# silently blocked while main stayed green (path-filter skipped
# main pushes that didn't touch formal/). See the proven 37s
# pattern in [[reference_coqorg_image_apt_coq_simpler]] used by
# verisimdb#87.

steps:
- name: Checkout repository
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2

- name: Install Coq 8.18 (noble apt)
run: |
sudo apt-get update -qq
sudo apt-get install -y --no-install-recommends coq

- name: Coq version (provenance)
run: |
coqc --version
Expand Down
Loading