From 09db77f54022b0559b5c6986fcc2fbaf5b225f52 Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 1 Jun 2026 14:38:21 +0100
Subject: [PATCH] =?UTF-8?q?ci(coq):=20switch=20coq-build=20to=20noble=20ap?=
 =?UTF-8?q?t=20=E2=80=94=20fix=20coqc-not-found=20on=20--user=20root?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The coq-build job has been failing on every PR that touches formal/
since the coqorg/coq:8.18 + --user root combo was introduced. The
container's `coqc` is configured via opam env in the non-root `coq`
user's .profile; under --user root that init never runs, so the
provenance step exits 127 with `coqc: not found`.

Main stayed green because path-filtered detect-relevant-changes
skipped the build job on every recent commit (none touched formal/).
PRs #263, #270, #274, #278, #280 were silently BLOCKED.

Fix per the proven 37s pattern from verisimdb#87 and
[[reference_coqorg_image_apt_coq_simpler]]: drop the container,
install Coq via `apt-get install coq` on Ubuntu 24.04 noble. Apt ships
exactly coq 8.18.0+dfsg, matching the formal/Justfile pin. No
behavioural change to coqc / coq_makefile / coqtop — same binaries,
just via apt instead of opam.

Verified locally: build oracle green (12 .v modules); Print
Assumptions returns the known-good baseline (only
region_liveness_at_split_l1_gen on L1).

Closes ephapax CI block.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 .github/workflows/coq-build.yml | 33 +++++++++++++++++++--------------
 1 file changed, 19 insertions(+), 14 deletions(-)

diff --git a/.github/workflows/coq-build.yml b/.github/workflows/coq-build.yml
index c2eb6e12..3cc9b797 100644
--- a/.github/workflows/coq-build.yml
+++ b/.github/workflows/coq-build.yml
@@ -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