rocq-elpi, coq-elpi: bound dune < 3.24 on the 16 released versions still using the (using coq) extension

[JasonGross]

Bound dune < 3.24 on the 16 released rocq-elpi / coq-elpi versions whose sources still select the deleted coq dune-language extension.

Why

dune 3.24 removed the coq language extension, so any dune-project containing (using coq X.Y) now fails to parse — Error: Extension coq was deleted in the 3.24 version of the dune language — regardless of its own (lang dune ...). opam solves one dune version per switch, so a single uncapped recipe anywhere in a closure selects dune ≥ 3.24 for everything in it and breaks packages that never touch elpi.

This is the tail of a cap that has been applied three times already and keeps being escaped:

• Bound dune < 3.24 for rocq-elpi.dev and rocq-micromega-plugin.dev #3806 capped rocq-elpi.dev. The solver then chose rocq-elpi 3.5.0 with dune 3.24.1.
• upper bound to dune in rocq-elpi #3795 capped 3.5.0. The solver then chose 3.4.0.
• 3.4.0 is uncapped, and so is every released rocq-elpi below it.

The failure this reproduces today, in the archive's own CI on a dev-prover job:

Error: Extension coq was deleted in the 3.24 version of the dune language

from rocq-elpi.3.4.0, which takes the whole mathcomp stack down with it. Capping only the newest version each time leaves the next one down to be selected; this closes the remaining released versions so there is nothing left to escape to.

What

One line per file, depends: only:

-  "dune" {>= "3.13"}
+  "dune" {>= "3.13" & < "3.24"}

• released/packages/rocq-elpi/rocq-elpi.{2.5.0,2.5.1,2.5.2,2.6.0,3.0.0,3.1.0,3.2.0,3.3.0,3.3.1,3.4.0}/opam
• released/packages/coq-elpi/coq-elpi.{2.2.0,2.2.1,2.2.2,2.2.3,2.3.0,2.4.0}/opam

Each file also contains ["dune" "subst"] {dev} and a bare "dune" in the build commands; both are left alone. git diff --numstat is 1 1 for all 16 files and lists nothing else.

rocq-elpi.3.5.0 is deliberately untouched — #3795 already capped it, and its depends: line was used as the byte-for-byte spelling control, so every line added here is character-identical to it.

coq-elpi 2.5.0 and later need no change: they are metapackages whose only dependencies are coq-core and rocq-elpi {= version}, so they inherit the cap.

Evidence each version is actually affected

dune-project was read out of all 16 release tarballs — the url { src: } target in each opam file, i.e. the tree opam actually builds, rather than a guess from a raw file URL. All 16 read:

(lang dune 3.13)
(using coq 0.8)

Nothing becomes unsatisfiable

No recipe anywhere in released/, core-dev/ or extra-dev/ requires dune >= 3.24 or newer — the search returns zero. 83 recipes on master already carry a < "3.24" upper bound, so this follows an established convention rather than introducing one. opam lint passes on all 16 directories under opam 2.1.2 (the version the archive CI pins), with an untouched sibling linted alongside as a baseline.

Scope

This is not an archive-wide sweep. 334 recipes still carry an uncapped dune dependency; most are unaffected because they use (using rocq ...), which dune 3.24 kept, but the ones that are affected are not addressed here.

🤖 Generated with Claude Code

https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b