ci(coq): unpin coq-interval, which required a Coq the image does not have

[gHashTag]

Refs #3316

#3324 fixed OPAMROOT and the job
got further — opam now updates both repositories and reaches the solver. It then
fails on a second, independent defect that was invisible until the first was
repaired:

[ERROR] Package conflict!
  * Missing dependency:
    - coq-interval = 4.9.0 -> coq < 8.19~
No solution found, exiting

The image is coqorg/coq:8.19-ocaml-4.14-flambda. The pin asks for a package
requiring a Coq older than the one it runs on, so it could never have
installed — the job just never got far enough to say so.

The dependency is real and not droppable: 7 of the 13 compiled files
Require Import Interval.Tactic — Bounds_Masses, Bounds_Mixing,
Bounds_Gauge, Bounds_LeptonMasses, Bounds_QuarkMasses, Unitarity,
ConsistencyChecks. Only the version can move.

Left unpinned on purpose, rather than pinned to a guess. No version of
coq-interval has been observed resolving against Coq 8.19 in this job, because
the job has never run far enough to try one. opam list --installed coq-interval
now prints what the solver chose — and that reading is what a pin should be
restored from, in a commit that can cite it.

This PR runs the workflow on itself; #3324 added this file to the
pull_request paths for exactly this reason.

[github-actions]

PR Dashboard

Generated at: 2026-09-05 18:51:18 UTC

• ci(coq): unpin coq-interval, which required a Coq the image does not have #3326 ci(coq): unpin coq-interval, which required a Coq the image does not have | Created: 2026-09-05 | Updated: 2026-09-05 | 23 failing / 29 total
• ci(release): drop a dispatch that can only fail #3325 ci(release): drop a dispatch that can only fail | Created: 2026-09-05 | Updated: 2026-09-05 | 2 failing / 28 total
• skill: make the spool the way lessons are added, and guard it #3323 skill: make the spool the way lessons are added, and guard it | Created: 2026-09-05 | Updated: 2026-09-05 | 1 failing / 36 total
• compiler: two frozen tests get the anchor their region needed #3317 compiler: two frozen tests get the anchor their region needed | Created: 2026-09-05 | Updated: 2026-09-05 | 0 failing / 38 total
• ci: zero checks is not zero failures, on the path that merges #3314 ci: zero checks is not zero failures, on the path that merges | Created: 2026-09-05 | Updated: 2026-09-05 | 0 failing / 28 total
• chore(ci)(deps): bump actions/attest-build-provenance from 1 to 4 #3001 chore(ci)(deps): bump actions/attest-build-provenance from 1 to 4 | Created: 2026-09-01 | Updated: 2026-09-05 | 5 failing / 32 total
• chore(ci)(deps): bump softprops/action-gh-release from 2 to 3 #3000 chore(ci)(deps): bump softprops/action-gh-release from 2 to 3 | Created: 2026-09-01 | Updated: 2026-09-05 | 4 failing / 32 total
• chore(ci)(deps): bump github/codeql-action from 3 to 4 #2999 chore(ci)(deps): bump github/codeql-action from 3 to 4 | Created: 2026-09-01 | Updated: 2026-09-05 | 4 failing / 32 total
• Land the formal verification harness on master (it has never run) #2727 Land the formal verification harness on master (it has never run) | Created: 2026-08-27 | Updated: 2026-09-05 | 5 failing / 24 total
• chore(deps)(deps): bump thiserror from 2.0.18 to 2.0.20 #2693 chore(deps)(deps): bump thiserror from 2.0.18 to 2.0.20 | Created: 2026-08-24 | Updated: 2026-08-28 | 3 failing / 34 total
• chore(deps)(deps): bump hyper from 1.10.1 to 1.11.0 #2692 chore(deps)(deps): bump hyper from 1.10.1 to 1.11.0 | Created: 2026-08-24 | Updated: 2026-08-28 | 3 failing / 33 total
• chore(deps)(deps): bump base64 from 0.22.1 to 0.23.1 #2691 chore(deps)(deps): bump base64 from 0.22.1 to 0.23.1 | Created: 2026-08-24 | Updated: 2026-08-28 | 3 failing / 34 total
• chore(deps)(deps): bump serde from 1.0.228 to 1.0.229 #2690 chore(deps)(deps): bump serde from 1.0.228 to 1.0.229 | Created: 2026-08-24 | Updated: 2026-08-28 | 3 failing / 34 total
• chore(deps)(deps): bump uuid from 1.23.2 to 1.25.0 #2689 chore(deps)(deps): bump uuid from 1.23.2 to 1.25.0 | Created: 2026-08-24 | Updated: 2026-08-28 | 3 failing / 34 total
• Unbreak FPGA CI and correct two unbacked hardware claims #2081 Unbreak FPGA CI and correct two unbacked hardware claims | Created: 2026-08-11 | Updated: 2026-08-20 | 5 failing / 27 total

Summary

Status	Count
Total Open PRs	15
PRs with Failing Checks	10
PRs with All Checks Green	5
READY	2
FAILING	10
PENDING	0

Seal Status

• ⚠️ STALE -- sha256(compiler.rs)=ffccfa1a71cf != manifest seal=87e5cbd3ad94.
  The committed NMSE numbers were certified against an older compiler.rs.
  Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

[github-actions]

📓 NotebookLM Notebook linked to this PR

• Notebook ID: b83263109fb055dc
• URL: https://notebooklm.google.com/notebook/b83263109fb055dc

This notebook contains session context, decisions, and artifacts for this work.

[gHashTag]

The unpin worked, and the job reached a third layer.

Install Coq Interval now succeeds — the solver picks a compatible coq-interval and pulls coq-coquelicot 3.4.5 with it. Run time went 1m44s → 4m10s. The failure moved to Compile Proofs:

File "./CorePhi.v", line 14, characters 8-24:
Error: The variable Rmult_lt_pos_pos was not found in the current environment.

That is the source, not the workflow, and this is where I stop.

Rmult_lt_pos_pos is used at CorePhi.v:14 and AlphaPhi.v:27 and is defined nowhere in the tree. It is not in Coq's Reals; the lemma with that statement is Rmult_lt_0_compat. CorePhi.v requires only Reals.Reals, so Interval is not in scope there either.

Renaming it would not be enough. The script under it is:

apply Rmult_lt_pos_pos.
- apply (Rlt_trans 0 2). lra.

apply (Rlt_trans 0 2) leaves 0 < 2 and 2 < 1 + sqrt 5; lra closes the first and cannot close the second without a bound on sqrt 5. So the proof needs rewriting, not a substitution, and iterating a Coq proof blind through a 4-minute CI cycle is not a good use of the loop.

The finding worth recording: because this workflow never got past opam install, coqc has never run on these files in CI, and the first line it reaches does not compile. The proofs are not "passing but ungated" — they are unbuilt.

Three layers, each invisible until the one before it was repaired:

1. OPAMROOT → opam could not start (ci: repair the two workflows whose failure was in the workflow #3324)
2. coq-interval pinned below the image's Coq (ci(coq): unpin coq-interval, which required a Coq the image does not have #3326, this PR)
3. CorePhi.v does not compile — left open, source work

This PR is still worth merging: it fixes a real workflow defect and moves the failure from infrastructure to substance.