extra-dev: dev recipes for 13 packages whose release cap is stale - #3810
Open
JasonGross wants to merge 7 commits into
Open
extra-dev: dev recipes for 13 packages whose release cap is stale#3810JasonGross wants to merge 7 commits into
JasonGross wants to merge 7 commits into
Conversation
…upstream is not
For each of these packages the archive's newest release is capped below Rocq
9.0, while upstream's own opam metadata on the default branch already claims
Rocq 9.x, `dev`, or no upper bound at all. The cap is an artefact of the
release recipe, not a statement about the sources.
package newest release upstream's own constraint
coq-stalmarck < 8.21 coq {= "dev"}
coq-stalmarck-tactic < 8.21 coq {= "dev"}
coq-waterproof < 8.18 rocq-prover {>= 9.0 & < 9.1 | = dev}
coq-mathcomp-abel < 8.17~ rocq-core {>= "9.0"}
coq-hanoi < 8.16~ coq {>= "9.1"}
coq-cds4ltl < 8.17~ rocq-core {>= 9.1 & < 9.2~}
coq-mmaps < 8.21 coq {>= "8.16"}, unbounded
coq-mathcomp-apery < 8.19~ coq {>= "8.20"}, unbounded
coq-bits < 8.17~ coq {>= "8.16"}, unbounded
coq-coqtail < 8.21 coq {>= "8.17"}, unbounded
coq-comp-dec-modal < 8.21 coq {>= "8.16"}, unbounded
coq-sum-of-two-square < 8.11~ coq, unbounded
coq-exact-real-arithmetic < 8.11~ (no opam file upstream)
Each recipe is upstream's in-tree opam file at the default branch, with
`version:` dropped and the source replaced by `url { src: "git+...#<branch>" }`.
Coq/Rocq *upper* bounds are dropped, because opam orders the version string
`dev` above every numeric version, so a `.dev` recipe carrying an upper bound
can never be selected; that affects coq-cds4ltl only. Lower bounds are left
exactly as upstream wrote them.
Three departures from a verbatim copy:
* coq-waterproof depends on both `coq` and `rocq-prover`. core-dev has
`coq.dev` but no `rocq-prover.dev` -- only `rocq-prover.9.3.dev`, which pins
`rocq-core` to 9.3.dev and so cannot be co-installed with the
`rocq-runtime.dev` that `coq.dev` pulls in. Requiring both names at once is
unsatisfiable on a dev switch, so this recipe keeps the one that resolves.
Adding a `rocq-prover.dev` to core-dev would let the line be restored.
* coq-sum-of-two-square's in-tree file is a coq-community template copy whose
homepage, dev-repo and bug-reports point at a `thery/SumOfTwoSquare` repo
that does not exist; they are redirected to the repository the recipe
actually builds from.
* coq-exact-real-arithmetic ships no opam file, so its recipe is the newest
released one with the tarball swapped for the git source. Its opam 1-era
`remove:` field named a user-contrib path under the old layout and is
redundant now that opam records the files a package adds to the prefix, so
it and the accompanying `light-uninstall` flag are dropped.
Not build-verified: these recipes assert what upstream's metadata asserts.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
Every row here is one this branch introduces, and every one declared a
prover permission that does not require the prover it exists to test:
coq-mmaps "coq" {>= "8.16"}
coq-bits "coq" {>= "8.16"}
coq-exact-real-arithmetic "coq" {>= "8.10"}
coq-sum-of-two-square "coq" (no constraint at all)
coq-mathcomp-abel "rocq-core" {>= "9.0"}
coq-mathcomp-apery "coq" {>= "8.20"}
opam orders `dev` above every numeric version, so a bare floor *prefers*
dev without *requiring* it: the row can go green having resolved a
released prover, and then it never tested the compiler it was added for.
Only the constraint distinguishes the two, so each becomes `{= "dev"}`.
`coq.dev` is a renaming metapackage depending on `coq-core {= version}`,
so pinning "coq" still delivers the package that supplies coqc; the name
is left alone in every row and only the constraint moves. `rocq-prover`
is deliberately not used anywhere here -- it publishes no literal `dev`
version, so `rocq-prover {= "dev"}` would select nothing.
THIS IS THE FIX FOR THE 4.09.0 CI JOB, NOT TIDINESS
---------------------------------------------------
The preference-versus-requirement gap above is not hypothetical on this
branch; it is what the 4.09.0 job is already doing, and it is legible in
the log rather than inferred. Measured in pipeline 1455718, job 7695087
(gitlab.inria.fr/coq/opam-repositories), whose switch invariant is
`ocaml-base-compiler < 4.11.0` and therefore forces ocaml 4.09.0:
coq-bits resolved coq.8.16.dev -> FAILED
coq-exact-real-arithmetic resolved coq.8.16.dev -> FAILED
coq-sum-of-two-square resolved coq.8.16.dev -> FAILED
coq-mmaps resolved coq.8.16.dev -> installed green
Not one of the four resolved the dev prover. The dev prover requires
ocaml >= 4.14.0, so on this switch it is unreachable and the loose floor
lets the solver walk backward into a released-line prover instead. The
three failures are all downstream of that choice: exact-real-arithmetic
and sum-of-two-square die with `Cannot find a physical path bound to
logical path <X> with prefix Stdlib`, because their ported sources say
`From Stdlib Require` and an 8.x prover roots the stdlib at `Coq`; bits
dies inside its dependency coq-mathcomp-zify.dev with `make: rocq: No
such file or directory`, an 8.x tree that has no `rocq` binary. The
fourth, mmaps, is worse than a failure in one respect -- it went green
without ever touching the compiler the row exists to test.
The gate is scripts/opam-coq-install-remove, which sets RC=1 in exactly
two places: a package that is installable on the current compiler and
then fails to build (`Packages that failed to install:`), and a package
installable on *no* compiler (`Packages that can never be installed:`).
A package that is simply not installable here but installable elsewhere
prints `Skipping <row> since not installable with the current compiler`
and lands in `Packages that were not compatible with the current
compiler:`, which is free.
So `{= "dev"}` moves these rows from the first bucket to the third.
PREDICTED, NOT OBSERVED. CI has not re-run since this edit, so the
paragraph above is a prediction about the next run and should be read as
one. Two things make it a strong one, both measured rather than assumed:
* The predicted path is already the observed path for rows that
already carry the constraint. coq-stalmarck and coq-stalmarck-tactic
are the only two rows this branch adds that were already `coq {=
"dev"}`, and they are exactly the rows the 4.09.0 job skips --
7695087:4389 and :4502, `Skipping ... since not installable with the
current compiler`, both landing in the free bucket. That is a
known-answer control inside the population, not an argument by
analogy.
* The tightening cannot turn 4.14.2 or 5.3.0 red, because on both of
those jobs all six rows already resolve the dev prover today
(7695088 and 7695089, `rocq-runtime dev` / `rocq-core dev` /
`coq-core dev` in each row's plan). The constraint is a no-op there.
The residual risk is the third bucket: if a tightened row were
installable on no compiler at all it would become a hard failure and
still set RC=1. The stalmarck control rules this out for the shape, and
the 4.14/5.3 greens rule it out for these six specifically.
Every row was re-checked for satisfiability from the patched text
afterwards. Tightening a row whose dependencies cap the prover below dev
turns a diagnosable floor into a recipe no solver can satisfy, which is
the worse state. The row at risk here was coq-mathcomp-apery, through
`coq-coqeal {>= "2.1.0"}`: all three admissible coqeal versions (dev,
2.1.1, 2.1.2) carry an explicit `(= "dev")` arm in their prover formula,
so the tightening is safe. A transitive dev-reachability sweep over all
304 extra-dev `.dev` rows, run against the merge of this branch with
master, reports 15 rows unable to resolve a dev prover and none of these
6 is among them, before or after the edit.
SCOPE: THE CRITERION COVERS ELEVEN ROWS, THIS COMMIT EDITS SIX
--------------------------------------------------------------
Stated plainly so the criterion above is not read as a completed sweep.
This branch adds 13 `.dev` rows. Two (coq-stalmarck, coq-stalmarck-
tactic) already required a dev prover. The other 11 all met the
criterion in the first paragraph; 6 are tightened here and 5 are not:
coq-cds4ltl "rocq-core" {>= "9.1"}, "rocq-stdlib" {>= "9.1"}
coq-comp-dec-modal "coq" {>= "8.16"}
coq-coqtail "coq" {>= "8.17"}
coq-hanoi "coq" {(>= "9.1")}
coq-waterproof "coq" {>= "9.0" & < "9.1" | = "dev"}
The six were selected by authorship, not by the criterion: they are the
rows whose source ports were done alongside this work. That is not a
principled boundary, and three of the five above are demonstrated false
greens on the same 4.09.0 job -- comp-dec-modal resolved coq.8.16.dev,
coqtail resolved coq.8.20.dev, waterproof resolved coq.9.0.dev, all
three installing green against a prover the row was not added to test.
waterproof is the subtlest: it already has a `| = "dev"` arm, but the
`>= "9.0" & < "9.1"` arm beside it is what the solver took.
These five want the same treatment and it is left to a follow-up rather
than folded in silently, because for four of them the tightening changes
nothing that is currently red (see below) and it would be misleading to
ship it as part of a commit whose claim is that the constraint fixes a
job.
WHAT THIS BRANCH CANNOT FIX
---------------------------
Four rows fail on the 4.14.2 and 5.3.0 jobs for a reason no constraint
on this branch reaches: their `url { src: }` points at the unported
upstream tree. Each dies in its own build, measured on 7695088:
coq-coqtail make[2]: *** [Complex/Canalysis_def.vo] Error 1
coq-hanoi Error: The LHS of subn_eq0 (extra.vo)
coq-stalmarck-tactic Error: Extension coq was deleted in the 3.24
version of the dune language
coq-waterproof same dune 3.24 error
Ports for all four exist on forks and are deliberately not wired in --
an extra-dev row points at the real upstream, and repointing it at a
fork would make the green meaningless. So their red is the intended
state, and this PR cannot reach a fully green CI until those ports land
upstream. Anyone reading the job summary should not try to fix them.
A fifth row, coq-comp-dec-modal, fails on the same two jobs and is NOT
in that group. Its error text is identical to stalmarck-tactic's and
waterproof's -- `Extension coq was deleted in the 3.24 version of the
dune language` -- but it is raised while building rocq-elpi.3.4.0, a
released dependency, and comp-dec-modal's own plan resolves dev
correctly. Grouping the three by error string gets this wrong; the
discriminator is which package the `[ERROR] The compilation of ...`
line names. Nothing on this branch or in our fork ports affects it.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
SEPARABLE FROM THE COMMIT BELOW, AND A DIFFERENT CLASS. The previous
commit makes each row honour its own stated purpose; this one changes
what the row tests, so it can be dropped on its own without touching the
prover work.
Requiring a dev prover does not by itself select dev mathcomp.
`coq-mathcomp-ssreflect.2.6.0` is a shim onto `rocq-mathcomp-ssreflect
{= version}`, that onto `rocq-mathcomp-boot {= version}`, and
`rocq-mathcomp-boot.2.6.0` declares a bare `rocq-core {>= "9.0"}` floor
-- so released mathcomp 2.6.0 remains selectable alongside a dev prover,
three hops out where no cell of these rows can show it. These three rows
therefore carry a second live permission, not a duplicate of the first.
Only the atoms with real solver freedom are pinned:
bits coq-mathcomp-algebra
abel coq-mathcomp-ssreflect, coq-mathcomp-real-closed
apery coq-mathcomp-ssreflect, coq-mathcomp-real-closed,
coq-mathcomp-bigenough
One pin per row is enough for the mathcomp core. ssreflect, fingroup,
algebra, solvable and field all reach `rocq-mathcomp-boot` through a
chain of `{= version}` edges, so pinning any one of them forces the
whole family; fingroup, algebra, solvable and field are deliberately
left bare rather than pinned redundantly.
For the same reason coq-coqeal, coq-mathcomp-zify and
coq-mathcomp-algebra-tactics are NOT pinned: every released version of
each already excludes a dev prover or a dev ssreflect (coqeal 2.1.1/2.1.2
cap ssreflect below dev, every released zify and algebra-tactics caps the
prover), so `.dev` is the only survivor and the constraint is inherited
with zero freedom. Copying a bound you do not own is not defence in
depth -- the only case where the copy changes the outcome is the case
where upstream has moved and the copy is wrong, and it would then fail in
the blocking direction, which emits no error naming itself.
coq-mathcomp-bigenough is pinned because it is genuinely free: 1.0.3
carries `coq {(>= "8.10" & < "9.2~") | (= "dev")}` and a bare
`coq-mathcomp-ssreflect {>= "1.6"}`, so it survives both dev axes and
would otherwise still be chosen at a release.
Re-checked for satisfiability from the patched text: the transitive
dev-reachability sweep over all 304 extra-dev `.dev` rows reports the
same 15 unreachable rows before and after, with none of these three
among them.
Note for review: upstream's own mathcomp `.dev` rows use the menu form
`("coq" {>= "8.20" & < "8.21~"} | "rocq-core" {>= "9.0" | = "dev"})`
rather than a hard `{= "dev"}`, with a comment asking that the dev arm be
kept for the coq-dev Docker images. The hard form is used here because
these are rows added to test dev specifically.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
This is the seventh row of the class the previous commit addresses, and it was
missed there. That commit's own "SCOPE" section admits the selection was made by
authorship rather than by the criterion; coq-cds4ltl.dev is the row that slipped
through as a result. It has exactly the shape the criterion names:
- "rocq-core" {>= "9.1"} -> {= "dev"}
- "rocq-stdlib" {>= "9.1"} -> {= "dev"}
Same shape as coq-mathcomp-abel.dev, whose `rocq-core {>= "9.0"}` this branch
already tightened. A floor admits `dev` -- `dev` sorts above every numeric
version -- so it *prefers* dev without *requiring* it, and the solver is free to
walk backward into a released prover.
IN MANDATE. The row is absent at upstream/master and added by this branch:
extra-dev/packages/coq-cds4ltl/coq-cds4ltl.dev/opam
ABSENT upstream/master, origin/master
present claude/dev-stale-recipes-tighten
SATISFIABLE. rocq-core.dev and rocq-stdlib.dev both exist (core-dev/), and
coq-cds4ltl has no other dependency, so nothing else can cap the prover.
BOTH LINES ARE LOAD-BEARING; THE STDLIB LINE CLOSES AN INDEPENDENT ARM.
Tightening `rocq-core` alone would not have been enough, because a released
`rocq-stdlib` that satisfies the old `{>= "9.1"}` floor is co-installable with a
dev core. The witness is a real row:
rocq-stdlib.9.1.0 "rocq-runtime" <- bare atom
"rocq-core" {>= "9.0"} <- bare floor, admits dev
`rocq-core.dev` imposes no reverse constraint on rocq-stdlib at all (its depends
are dune, `rocq-runtime {= version}`, and odoc/with-doc), so
{ rocq-core.dev, rocq-runtime.dev, rocq-stdlib.9.1.0 }
is a complete, satisfying assignment for the pre-commit recipe with only the
core line tightened: 9.1.0 clears the old `{>= "9.1"}`, its floor on core
admits dev, and its bare `rocq-runtime` accepts rocq-runtime.dev. That is a
released stdlib against a dev prover -- precisely the state the criterion
exists to exclude. The second line is what rules it out.
The published rocq-stdlib population splits two and two:
rocq-stdlib.9.0+rc1 rocq-core {>= "9.0" & < "9.1~"} caps below dev
rocq-stdlib.9.2.0 rocq-core {>= "9.1" & < "9.4~"} caps below dev
rocq-stdlib.9.0.0 rocq-core uncapped (below the floor)
rocq-stdlib.9.1.0 rocq-core {>= "9.0"} uncapped, IN REACH
The two that cap live in this archive; the two that do not live in the `default`
repo (opam.ocaml.org). Only 9.1.0 is in reach of this row's old floor -- 9.0.0
is below it -- but one witness is all the claim needs.
AND THE WITNESS IS REACHABLE IN CI, not merely on a developer's switch. The
repo's own scripts put `default` in the root that solves these rows:
scripts/opam-coq-init:10 opam init --root=$OPAM_ROOT_DIR ...
scripts/opam-coq-setup-root:14 opam update default
scripts/opam-coq-setup-root:16 opam repo add released ...
Line 14 is unconditional inside `setup_root()`, and it would fail on a root that
had no `default` -- so its presence is load-bearing for CI, not incidental.
`setup_root` is on the path CI actually takes (`.gitlab-ci.yml:58` and
`scripts/opam-coq-install-remove:9` both source it). So rocq-stdlib.9.1.0 is
selectable in the environment that resolves this row.
THIS CHANGES NO CI OUTCOME. Unlike the six rows in the previous commit, this one
is not a fix for the 4.09.0 job: coq-cds4ltl is already in that job's free-pass
bucket (not installable with the current compiler -> skipped), and it already
resolves a dev prover on both the 4.14.2 and 5.3.0 legs. It is a correctness fix
on the constraint, not a green.
Kept as its own commit so it can be dropped independently of the six.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
e64b42b and efc9444 tightened six of this branch's new .dev rows. Four were left: coq-comp-dec-modal.dev, coq-coqtail.dev, coq-hanoi.dev and coq-waterproof.dev. All four are rows THIS branch adds -- none exists at upstream/master (`git cat-file -e upstream/master:<path>` fails for all four) -- so their prover lines are ours to get right. coq-comp-dec-modal.dev "coq" {>= "8.16"} -> {= "dev"} coq-coqtail.dev "coq" {>= "8.17"} -> {= "dev"} coq-hanoi.dev "coq" {(>= "9.1")} -> {= "dev"} coq-waterproof.dev "coq" {>= "9.0" & < "9.1" | = "dev"} -> {= "dev"} The added line is byte-identical in all four to the eight rows already tightened (2-space indent, ` "coq" {= "dev"}`); coq-bits.dev:20 was the spelling control. `git diff --numstat` is `1 1` on exactly these four files and lists nothing else. opam 2.1.2 -- the version the archive CI pins -- lints all four package directories at rc=0. WHAT THIS ACHIEVES, AND IT IS NARROW: it converts false greens into honest skips. It fixes none of these packages' real breaks. THE FALSE GREENS, from the 4.09.0 job (7695087) That job's succeeded-to-install bucket at :5294 lists comp-dec-modal, coqtail and waterproof. None of the three resolved a dev prover: coq-comp-dec-modal coq 8.16.dev [required by coq-comp-dec-modal] coq-coqtail coq 8.20.dev (+ coq-core/coq-stdlib/coqide-server) coq-waterproof rocq-core 9.0.dev, rocq-runtime 9.0.dev, coq-core 9.0.dev, coqide-server 9.0.dev So a `.dev` row in a `dev` repository reported green having built against a released prover. That is the defect; the floor is what permits it. The criterion is NOT "the prover line is loose". A loose floor of `>= 9.1` still resolves 9.1+rc1, which requires `ocaml >= 4.14.0`, so it excludes 4.09.0 exactly as a pin would. The floor has to reach back to a prover old enough to build on the job's compiler. That is why 8.16 / 8.17 / 9.0 go false-green here and `>= 9.1` does not. coq-hanoi is the row that shows it: its `{(>= "9.1")}` was loose and it skipped anyway. opam's own conflict report above the Skipping line reads `coq >= 9.1 -> coq-core = 9.1+rc1 -> rocq-runtime = 9.1+rc1 -> ocaml >= 4.14.0`. hanoi is already in the free bucket at :5296, so this edit changes nothing about its behaviour on any current job -- it is criterion consistency, not a fix. coq-waterproof IS A SEMANTIC CHANGE, NOT A FLOOR BUMP Its line was `{>= "9.0" & < "9.1" | = "dev"}` -- it already had a dev arm. Tightening deletes the released arm, and the named witness for why is that the solver actually took that arm: on 4.09.0 the plan reads `install coq 9.0.dev [required by coq-waterproof]`. That plan is also internally mixed -- rocq-runtime/rocq-core/coq-core/coqide-server at 9.0.dev alongside rocq-stdlib 9.1.0 and coq-stdlib 9.1.0 -- so the released arm was not merely selecting an older prover, it was selecting a combination nobody tests. After this change coq-waterproof.dev is unsatisfiable on any job whose compiler cannot build a dev prover, instead of resolving to 9.0. That is the intended outcome for a `.dev` row and it is free in the CI gate: the harness's *not compatible with the current compiler* bucket does not set RC=1. In scripts/opam-coq-install-remove the four buckets are printed at :101-104, and `RC=1` appears on exactly two paths -- :67 with FAILURES and :83 with HARDFAILURES. The UNTESTED path at :86 sets nothing. NO ROW BECOMES A HARD FAILURE Checked per row rather than argued: on both 4.14.2 (7695088) and 5.3.0 (7695089), all four rows resolve `coq dev`, with the `coq` line reading `[required by <the row>]` in each of the eight plans. Neither job has any member in the not-compatible or can-never-be-installed buckets (:4727/:4728 and :4920/:4921 are both empty). So the tightening cannot move a row into *can never be installed*. THE REAL BREAKS, WHICH THIS COMMIT DOES NOT TOUCH Measured on 7695088 (4.14.2), where all four are in the failed bucket: comp-dec-modal its dependency rocq-elpi.3.4.0 fails to compile (:2856, inside comp-dec-modal's own install block :2847-:2881): `(using coq 0.8)` / "Extension coq was deleted in the 3.24 version of the dune language". Addressed separately by the dune < 3.24 caps in rocq-prover#3819. coqtail its own tree: Complex/Canalysis_def.vo, Error 1 (:3001). hanoi its own tree: extra.v:225, "The LHS of subn_eq0 (_ - _ == 0) does not match any subterm of the goal". waterproof its own dune-project line 2, same dune 3.24 message as above -- here in waterproof's source, not a dependency. All four remain red after this change. The claim of this commit is only that they are red for their real reasons on every compiler, rather than green on 4.09.0 against a prover the row was never meant to admit. CORRECTION TO e64b42b (pushed; corrected here rather than amended) Two errors in that commit's message. Neither affects any recipe, on this branch or elsewhere; both were found by review, and the second is mine. 1. "coq-stalmarck and coq-stalmarck-tactic ... are exactly the rows the 4.09.0 job skips" -- the first clause is right, the "exactly" is wrong. The skip bucket has six members, enumerated by the job itself at 7695087:5296: coq-cds4ltl, coq-hanoi, coq-mathcomp-abel, coq-mathcomp-apery, coq-stalmarck-tactic, coq-stalmarck. 2. The heading "THIS IS THE FIX FOR THE 4.09.0 CI JOB" covers four of the six rows that commit edits, not six. coq-mathcomp-abel and coq-mathcomp-apery were already skipping before it, so for them `{= "dev"}` is a 4.09.0 no-op. (The section body underneath was already correctly scoped to four.) The skip bucket splits three ways, not two, with every binding edge below quoted from opam's conflict report above the corresponding Skipping line in 7695087: (a) prover-driven, already tight -- the control, and it holds coq-stalmarck, coq-stalmarck-tactic: `coq >= dev -> coqide-server >= dev -> rocq-runtime >= dev -> ocaml >= 4.14.0` (b) prover-driven, loose, and skipping anyway coq-cds4ltl: `rocq-core >= 9.1 -> rocq-runtime = 9.1+rc1 -> ocaml >= 4.14.0` coq-hanoi: `coq >= 9.1 -> coq-core = 9.1+rc1 -> rocq-runtime = 9.1+rc1 -> ocaml >= 4.14.0` (c) dependency-driven -- the prover line is irrelevant coq-mathcomp-abel: `coq-mathcomp-ssreflect >= 2.4 -> ... -> coq-elpi >= 2.0 -> ocaml >= 4.10.0` coq-mathcomp-apery: `coq-coqeal >= 2.1.0 -> coq-elpi >= 2.4.1 -> rocq-elpi < 2.5.1 -> ocaml >= 4.10.0` Class (b) is why the criterion above is stated as reach-back rather than looseness: describing it as looseness overstates the affected set by two rows on this very job. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
…v rows using the deleted (using coq) extension
These are two of the five rows failing in this PR's own CI, and the only
two with a recipe-side fix. Both die at line 2 of their dune-project,
before anything is compiled:
Error: Extension coq was deleted in the 3.24 version of the dune language
CI resolved dune 3.24.2 for them because neither recipe had an upper
bound. Read out of the trees the two url { src: } targets actually name:
rocq-community/stalmarck#master (lang dune 2.8) / (using coq 0.3)
impermeable/coq-waterproof#main (lang dune 3.8) / (using coq 0.8)
so each existing floor already matches its own (lang dune ...) line and
only the ceiling was missing.
Same shape and same spelling as rocq-prover#3819, which capped the 16 released elpi
rows. Nothing becomes unsatisfiable: rocq-runtime.dev and rocq-core.dev
both ask for "dune" {>= "3.21"}, and rocq master's own dune-project is
(lang dune 3.21), so 3.21-3.23.x satisfies the prover and both rows.
These are the only two of the 13 rows this branch adds that depend on
dune at all; the sibling coq-stalmarck.dev is make-driven and needs
nothing. The other three CI failures are source breaks in the packages
themselves and are not addressed here.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
…branch
The .dev row pointed at impermeable/coq-waterproof#main, which is the
branch for released Rocq: its own opam declares
`rocq-prover {>= "9.0" & < "9.1"}`. Upstream keeps a separate
`coq-master` branch for tracking the development prover, carrying the
adaptations `main` does not have -- rocq-prover/rocq#21987 (secvar
status) and #22114 (projection names) among them, 90 commits and 12
files under src/.
The dune bound in the previous commit is needed either way: both
branches still open with `(lang dune 3.8)` / `(using coq 0.8)`.
The ten commits `main` has that `coq-master` does not are a version
bump, two coq-lsp documentation updates and a notation tweak, so
nothing the dev row wants is lost.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
JasonGross
added a commit
to JasonGross/opam-coq-archive
that referenced
this pull request
Aug 11, 2026
Copying upstream's lower bound verbatim was the wrong default for an
extra-dev row, and the first CI run made the point in its strongest form.
On pipeline 1455719 job 7695092 (opam-build:4.09.0) all nine rows
installed and not one resolved a dev prover: six took coq.8.16.dev, two
took 8.20, one took 8.14, and `Packages that were not compatible with the
current compiler:` came back empty. The job was green about Coq 8.
The mechanism is the prover's own ocaml floor. rocq-runtime.9.1.dev
requires ocaml >= 4.14.0 and that job pins ocaml-base-compiler < 4.11.0,
so a dev prover cannot be installed there; a row whose floor reaches back
to a prover at 9.0 or below simply resolves one of those instead of being
skipped.
coq-sudoku shows that an OR is not a defence. Its bound already read
`{(>= "8.12" & < "8.15~") | (= "dev")}` and it resolved coq.8.14.dev:
where the dev arm is unsatisfiable opam takes the other one. Only
`{= "dev"}` alone excludes the fallback.
coq-belgames also gets its otherwise-unconstrained coq-mathcomp-algebra
pinned to dev, for the same reason one hop out.
On the two dev legs this is a no-op -- they already resolved dev for every
row -- so the change is confined to 4.09.0, which is what it is for. The
rows move from "succeeded to install" to "not compatible with the current
compiler", a bucket the harness does not count against the job. Measured
precedent: after the equivalent tightening, rocq-prover#3810's 4.09.0 leg (job
7713620) reports 13 of 13 not-compatible, "can never be installed" empty,
and the job succeeds.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds 13
extra-devrecipes for packages whose newest archive release is capped below Rocq 9.0 but whose upstream metadata already claims Rocq 9.x,dev, or no upper bound. Companion to #3811, which covers packages whose upstream has not been ported.< 8.21coq {= "dev"}< 8.21coq {= "dev"}< 8.18rocq-core {>= 9.1 & < 9.2 | = dev}< 8.17~rocq-core {>= "9.0"}< 8.16~coq {>= "9.1"}< 8.17~rocq-core {>= 9.1 & < 9.2~}< 8.21coq {>= "8.16"}, unbounded< 8.19~coq {>= "8.20"}, unbounded< 8.17~coq {>= "8.16"}, unbounded< 8.21coq {>= "8.17"}, unbounded< 8.21coq {>= "8.16"}, unbounded< 8.11~coq, unbounded< 8.11~*
coq-waterprooffollows upstream'scoq-masterdev-tracking branch; every other row follows its repository's default branch.Recipes
Each recipe uses upstream's in-tree
.opamfile, dropsversion:, replaces the source withurl { src: "git+<repo>#<branch>" }, and removes Coq/Rocq upper bounds because opam ordersdevabove every numeric version.There are three other departures:
coq-waterproofkeeps onlycoq {= "dev"}of the three prover packages named upstream.coq.devalready bringscoq-core {= version},rocq-runtime {= version},coq-stdlib, androcq-stdlib {= version}atdev.coq-sum-of-two-squarecorrectshomepage,dev-repo, andbug-reports, which point to a nonexistentthery/SumOfTwoSquarerepository upstream.coq-exact-real-arithmetichas no upstream opam file, so its recipe starts from the newest release and swaps the tarball for git. It drops the obsoleteremove:field andlight-uninstallflag.On waterproof's former
mainbranch, this was necessary rather than cosmetic:rocq-prover.9.3.devpinsrocq-coreto9.3.dev, which cannot coexist with therocq-runtime.devselected bycoq.dev. The branch declaresversion: "3.1.1+9.0-dev";coq-masterdeclaresversion: "3.1.1+dev"and avoidsrocq-prover. Tracking a dedicated prover branch is established practice: 71 of 304extra-dev/packagesurl { src: }fragments use something other thanmasterormain.All rows now constrain the prover to
{= "dev"}. The initial loose lower bounds letopam-build:4.09.0, which constrainsocaml-base-compiler < 4.11.0, resolve ported sources against old provers becauserocq-runtimehas requiredocaml >= 4.14.0since 9.1+rc1. Pipeline 1455718, job 7695087 showed the result:coq.8.16.devcoq.8.20.devcoq.9.0.dev(viarocq-core.9.0.dev)coq.8.16.devPackage conflict!, correctly skippedThe failures were also old-prover artifacts.
coq-exact-real-arithmeticandcoq-sum-of-two-squareuseFrom Stdlib Require, producingCannot find a physical path bound to logical path ZArith with prefix Stdlibon 8.x.coq-bitsmixedcoq.8.16.devandcoq-mathcomp-algebra.2.2.0withcoq-mathcomp-zify.dev, then failed withmake: rocq: No such file or directory.The recipes therefore pin all 11 rows that did not already do so to the dev prover. They also pin the otherwise-unconstrained mathcomp dependencies of
coq-mathcomp-abel,coq-mathcomp-apery, andcoq-bitstodev.coq-cds4ltl(rocq-core {>= "9.1"}) andcoq-hanoi(coq {>= "9.1"}) were already skipped on OCaml 4.09 because Rocq 9.1 requires OCaml 4.14; tightening those two is hygiene, while tightening the other nine fixes the bad resolutions.CI
Pipeline 1458297 tested PR head
0d8d6f9dcmerged with master. All three legs terminated.opam-build:4.09.0skips all 13 rows as not installable; zero are built, and itssucceeded,failed, andcan never be installedledgers are empty. This is the intended resolution result, but it exercises none of the new recipes.The 4.14.2 and 5.3.0 legs agreed: 13 attempted, 0 skipped, 8 installed, and 5 failed, with the same first error on both legs. Every installed row compiled files, ranging from 25 for
coq-cds4ltlto 112 forcoq-mathcomp-apery. The three pinned mathcomp rows had the same plans before and after tightening, so the change affects only 4.09.0.dune-project:2 Error: Extension coq was deleted in the 3.24 version of the dune language—(using coq 0.3)(using coq 0.8)edone.v:10 Unable to locate library mathcomp.ssreflect.ssreflectComplex/Canalysis_def.v:46 Error: The '%' scope delimiter in 'Arguments' commands is deprecated, use '%_' insteadextra.v:225 Error: The LHS of subn_eq0 (_ - _ == 0) does not match any subterm of the goal#3819 capped
dune < 3.24for the 16 released elpi versions using the deleted extension and fixed the earlierrocq-elpi.3.4.0failureExtension coq was deleted in the 3.24 version of the dune language; both dev legs now resolve every elpi row todev. The two remaining dune failures occur incoq-stalmarck-tacticandcoq-waterproof, the only rows here that depend on dune. Their trees specify(lang dune 2.8)/(using coq 0.3)and(lang dune 3.8)/(using coq 0.8), respectively, so their recipes add the same ceiling used by #3819:The waterproof constraint is likewise
{>= "3.8" & < "3.24"}. This remains compatible withrocq-runtime.devandrocq-core.dev, which requiredune {>= "3.21"}. Both files passopam lint --warn=-21. The ceiling is a stopgap until the projects move to(using rocq …).coq-waterproofalso moves from#main, upstream's released line, to its development-prover branch:coq-mastercontains the adaptations forrocq-prover/rocq#21987androcq-prover/rocq#22114;maintrails it by 90 commits across 117 files, including 12 undersrc/. The 10 commits present only onmainare a3.1.1+...-devversion bump, two coq-lsp documentation updates, and a notation tweak.Dune cap and waterproof branch results
The dune-cap-only commit 072925e ran in pipeline 1459862.
opam-build:4.14.2(job 7723631) andopam-build:5.3.0(job 7723632) produced byte-identical ledgers:coq-stalmarck-tactic.devinstalled, whilecoq-waterproof.devfailed. The capped packages' own solves selected:Those attributions occur at log lines 3644 and 4187 on 4.14.2 and 3736 and 4321 on 5.3.0. Across all ten independent solves, dune was otherwise only constrained to
>= 3.21and resolved to 3.24.2 five times and 3.23.1 five times, including three uncapped rows; the attribution, not the selected version alone, shows the cap acted.Before the cap, pipeline 1458297's 4.14.2 leg (job 7713621) selected
- install dune 3.24.2 [required by coq-waterproof]at log line 4671 and[required by coq-stalmarck-tactic]at 4146; both then failed atdune-project:2withError: Extension coq was deleted in the 3.24 version of the dune languageat lines 4704 and 4180. The 5.3.0 leg agrees at lines 4631 and 4125. This establishes that the cap affects each row's independent solve.After the cap, waterproof passed
dune-projectbut exposed six OCaml API errors undersrc/, identically on both OCaml versions. The first was:The other sites were
exceptions.ml:176,proofutils.ml:208,wp_rewrite.ml:36,wp_auto.ml:129, andwp_eauto.ml. All are adapted oncoq-master.The repointing commit a01f994 ran in pipeline 1459864. Both
opam-build:4.14.2(job 7723639) andopam-build:5.3.0(job 7723640) attempted 10 rows and installed all 10, with empty failure ledgers at log lines 4741 and 4883. The control and treatment trees differed only in waterproof'surl { src: }: control 7f0ebc50 used#main, while treatment bf5f4c33 used#coq-master.Both changes are required.
coq-mastertip f49b8305b still uses(lang dune 3.8)/(using coq 0.8), so without the cap it fails atdune-project:2; without the branch change, the capped row fails atunfold_framework.mli:54.coq-stalmarck-tactic's recipe is byte-identical (877 B) between control and treatment, so its four green cells represent two results. It is the 7th row and waterproof the 10th; all four legs ran through their final ledgers. The control legs took 7,411 s and 8,225 s, and the treatment legs 11,746 s and 12,544 s, under the 86,400 s GitLab limit.Known source failures
ci-skip: coq-comp-dec-modal coq-coqtail coq-hanoi
These three default branches have not been ported to Rocq dev, and no archive constraint fixes their source failures.
.gitlab-ci.ymlreadsci-skip:from this PR body only, so the skip does not apply when another PR touches the rows. The recipes knowingly remain red; they can instead be dropped if the archive should not carry them in that state.coq-comp-dec-modalalso fails against Rocq 9.2 with mathcomp 2.5.0+9.2 atbcase.v:5andedone.v:10; it builds only with mathcomp 2.4.0.ssreflect.vmoved out ofssreflect/in mathcomp 2.5.0. Itscoq-mathcomp-ssreflect {>= "2.0"}floor is therefore loose.coq-coqtailstill uses the bare%delimiter inArguments. The opam log elides the file/line andError:head, but retains the suggestedfor f in $(find . -name '*.v'); do sed '/Arguments/ s/%/%_/g' -i $f; done, the[argument-scope-delimiter,deprecated-since-8.19,…]tag, andComplex/Canalysis_def.voas the failed target.coq-hanoihas a proof break against mathcomp dev:subn_eq0no longer matches atextra.v:225.None of these three has a dependent under
released/,extra-dev/, orcore-dev/; searching the archive found zero occurrences outside their own directories, versus 568 for thecoq-mathcomp-ssreflectcontrol.Not included and caveats
coq-library-folhas a portedrocq-9.0branch and tagv1.1+9.0.1, but its opam file pins exact versions ofcoq-library-undecidabilityandrocq-metarocq-templateabsent from this archive and supplies them throughpin-depends:. It needs a released1.1+9.0.1recipe instead.The recipes were not build-verified when first opened; their first actual builds were this CI. All 13 pass
opam lint --warn=-21 --check-upstream.coq-exact-real-arithmeticretains a non-SPDX license warning andcoq-sum-of-two-squarean uncapitalized synopsis warning. Every named dependency already has a.devorcore-devrecipe in the archive.The packages were selected by surveying the 175 archive packages whose newest release is capped below Rocq 9.0 or which declare no coq/rocq dependency, then comparing upstream activity and in-tree opam constraints.
Wordsmithed by Codex.