Skip to content

Commit 16a1544

Browse files
ci(coq-build): run coqorg/coq container as root to fix actions/checkout EACCES (#236)
## Summary The Coq merge-oracle workflow (`coq-build.yml`) was failing across every `formal/` PR (including #234 which had to bypass) with: ``` Error: EACCES: permission denied, open '/__w/_temp/_runner_file_commands/save_state_…' ``` ## Root cause `coqorg/coq:8.18` defaults to the non-root `coq` user (UID 1000). `actions/checkout` writes save_state files to `/__w/_temp/_runner_file_commands` which is mounted from the runner host — the `coq` user lacks write permission there. The job dies in checkout's post-step before `coq_makefile` runs. ## Fix `container.options: --user root` runs the container as root. The shared workspace paths become writable; the in-container build environment is otherwise unchanged (root inside the container maps to the runner host's runner user via the Actions sandbox, not host-root). ## Why this matters Per `[[feedback_proof_pr_build_oracle_is_only_truth]]` the Coq workflow is the *only* merge oracle for `formal/` PRs. If the workflow itself can't run, the hard gate is effectively bypassed. ## Test plan - [ ] `Coq build — formal/_CoqProject` goes green on this PR - [ ] `Print Assumptions of load-bearing theorem` step actually executes (visible in run log) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 372b352 commit 16a1544

1 file changed

Lines changed: 8 additions & 0 deletions

File tree

.github/workflows/coq-build.yml

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,14 @@ jobs:
4848
# `make` semantics — "what the maintainer's machine has".
4949
container:
5050
image: coqorg/coq:8.18
51+
# actions/checkout's post-step writes to /__w/_temp/_runner_file_commands
52+
# via Node fs.writeFileSync. The coqorg/coq image defaults to the
53+
# non-root `coq` user (UID 1000), but the runner mounts /__w as the
54+
# host runner user — EACCES until checkout's saveState. Running the
55+
# container as root keeps the workspace-shared paths writable while
56+
# leaving the in-container build untouched (root in container is
57+
# still mapped to the runner host's runner user, not host-root).
58+
options: --user root
5159

5260
steps:
5361
- name: Checkout repository

0 commit comments

Comments
 (0)