From 7191d3d9f32822ca1adfc54bce03dd00ad6e7ef5 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Fri, 21 Aug 2026 16:07:43 +0700 Subject: [PATCH] fix(ci): repair never-green Coq kernel build gate The 'build' check owned by .github/workflows/coq-kernel.yml has failed on every master run since it was added (run #3, 2026-04-06 .. run #173). Steps 5-9 of the job have never executed once. This is a different check from cli-tri.yml's 'build', which shares the name and masks it in the check-runs API. Cause 1: the job runs coqorg/coq:8.19 with --user root, but the image's initialised opam root belongs to the coq user at /home/coq/.opam. As root HOME=/root has no .opam, so opam exited 50. Set job-level OPAMROOT rather than running opam init, which would rebuild Coq into an empty root while coqc/coqchk on PATH still came from the image switch. Cause 2, latent behind cause 1: 'cd bootstrap && cargo build --release' then './target/release/t27c' resolves to bootstrap/target/release/t27c, but bootstrap is a member of the root cargo workspace, so the binary lands in the repo-root target/. Build with -p t27c from the root. The step is not weakened: coq-flocq is still installed and no failure is suppressed. coq/Kernel/PhiFloat.v has a hard Flocq import. Closes #2320 --- .github/workflows/coq-kernel.yml | 30 ++++++++++++++++++++- docs/now/2026-08-21-coq-kernel-opam-root.md | 10 +++++++ 2 files changed, 39 insertions(+), 1 deletion(-) create mode 100644 docs/now/2026-08-21-coq-kernel-opam-root.md diff --git a/.github/workflows/coq-kernel.yml b/.github/workflows/coq-kernel.yml index 2ae379b9f9..dac4ef6d16 100644 --- a/.github/workflows/coq-kernel.yml +++ b/.github/workflows/coq-kernel.yml @@ -20,23 +20,44 @@ jobs: container: image: coqorg/coq:8.19-ocaml-4.14-flambda options: --user root + # This image ships a fully initialised opam root, but it belongs to the + # image's `coq` user and lives at /home/coq/.opam. `--user root` above makes + # HOME=/root, so a bare `opam` looked for /root/.opam, found nothing, and + # exited 50 with "Opam has not been initialised" -- on every run since the + # workflow was added. Point every step at the root that actually exists. + # + # Deliberately NOT `opam init`: a fresh root has no Coq in it, so + # `opam install coq-flocq` would rebuild the whole compiler, and the coqc / + # coqchk already on PATH would still come from the image's switch. Reusing + # the image's root also inherits its sandbox-disabled config, which is what + # `--disable-sandboxing` would otherwise be needed for. + env: + OPAMROOT: /home/coq/.opam steps: - uses: actions/checkout@v6 - name: Install Flocq (opam) run: | + set -eux + # Echo which root/switch resolved, so a future failure here says why + # instead of just exiting 50. + opam var root + opam switch list opam update -y opam install -y coq-flocq - name: Build coq/ (T27 + Flocq) run: | + set -eux eval $(opam env) + coqc --version cd coq coq_makefile -f _CoqProject -o CoqMakefile make -f CoqMakefile -j$(nproc) - name: coqchk PhiFloat (consistency) run: | + set -eux eval $(opam env) cd coq coqchk -silent -R . T27 T27.Kernel.PhiFloat @@ -46,7 +67,14 @@ jobs: - name: Build t27c and validate phi f64 parameters run: | - cd bootstrap && cargo build --release + set -eux + # `bootstrap` is a member of the ROOT cargo workspace, so the binary + # lands in the workspace target dir at the repo root -- never in + # bootstrap/target/. The old `cd bootstrap && cargo build --release` + # followed by `./target/release/t27c` resolved to + # bootstrap/target/release/t27c, which cannot exist (exit 127). This + # step had never once executed, so the bad path was never observed. + cargo build --release -p t27c ./target/release/t27c validate-phi - name: Verify Kernel PHI layer has no Admitted diff --git a/docs/now/2026-08-21-coq-kernel-opam-root.md b/docs/now/2026-08-21-coq-kernel-opam-root.md new file mode 100644 index 0000000000..d6c7f6dba4 --- /dev/null +++ b/docs/now/2026-08-21-coq-kernel-opam-root.md @@ -0,0 +1,10 @@ +# Coq kernel `build` gate: never-green since 2026-04-06, now unblocked + +- Identified the red `build` check on `master` as `.github/workflows/coq-kernel.yml` (workflow `Coq kernel`, job `build`), **not** `cli-tri.yml` — both emit a check named `build` and the check-runs API returns only the newest per name, so one masked the other. +- Established it was born broken, not regressed: all 12 `master` runs concluded `failure`, run #3 (2026-04-06) through run #173 (2026-08-21). Steps 5-9 of the job have never executed once. +- Fixed cause 1: the job runs `coqorg/coq:8.19` with `--user root`, but the image's initialised opam root belongs to the `coq` user at `/home/coq/.opam`; as root `HOME=/root` had no `.opam`, so opam exited 50. Set a job-level `OPAMROOT: /home/coq/.opam` rather than `opam init`, which would rebuild Coq into an empty root and leave `coqc`/`coqchk` pointing at the image's switch. +- Fixed cause 2, latent behind cause 1: `cd bootstrap && cargo build --release` then `./target/release/t27c` resolved to `bootstrap/target/release/t27c`, but `bootstrap` is a member of the root cargo workspace so the binary lands in the repo-root `target/`. Now `cargo build --release -p t27c` from the root. +- Step not weakened: no `|| true`, no `continue-on-error`, and `coq-flocq` still installed — `coq/Kernel/PhiFloat.v` has a hard `From Flocq Require Import IEEE754.Binary`. +- Noted but not changed: `.github/workflows/coq-proofs.yml` (job `compile-proofs`) carries the identical `--user root` opam defect; its `paths:` filter means this PR's CI could not verify a change to it. + +Closes #2320