Skip to content

rocq-elpi-json, rocq-elpi-xml: bound dune < 3.24 on the 5 released rows - #3826

Merged
gares merged 1 commit into
rocq-prover:masterfrom
JasonGross:claude/elpi-json-xml-dune-324
Aug 12, 2026
Merged

rocq-elpi-json, rocq-elpi-xml: bound dune < 3.24 on the 5 released rows#3826
gares merged 1 commit into
rocq-prover:masterfrom
JasonGross:claude/elpi-json-xml-dune-324

Conversation

@JasonGross

Copy link
Copy Markdown
Member

dune 3.24 deleted the coq dune-language extension, so a dune-project
containing (using coq X.Y) no longer parses whatever its own (lang dune ...)
says. opam solves one dune version per switch, so an uncapped recipe in a
closure can select dune >= 3.24 for everything in it.

rocq-elpi-json and rocq-elpi-xml are built out of the same coq-elpi release
tarballs as rocq-elpiapps/json/ and apps/xml/ of that tree — so the
defect reaches them identically. They were missed by every cap so far because
they are missed by name:

commit / PR rows capped
34f82e5 rocq-elpi.3.5.0
#3806 rocq-elpi.dev
#3819 the remaining 16 released rocq-elpi / coq-elpi rows

That leaves 18 capped rows at master and these 5 uncapped.

Evidence

The dune-project files were read out of the three release tarballs these 5
rows name in their own url { src: }v3.3.1, v3.4.0, v3.5.0 — rather
than guessed from opam metadata. All three:

(lang dune 3.13)
(using coq 0.8)

Satisfiability

rocq-elpi, which all 5 rows depend on, already asks for
dune {>= "3.13" & < "3.24"}, and rocq-core.dev / rocq-runtime.dev ask
dune {>= "3.21"}, so 3.21–3.23.x satisfies the whole closure. opam lint
passes on all 5 files.

Deliberately not touched

The coq-elpi rows at 2.5.0 and above are metapackages depending on
rocq-elpi, with no dune dependency and no build; the coq-elpi rows below
2.2.0 have no dune dependency either.

The two extra-dev rows rocq-elpi-json.dev and rocq-elpi-xml.dev carry the
same uncapped dune {>= "3.13"}, but they exist only on #3812 and not at
master, so they are not in scope here and should be capped there.

dune 3.24 deleted the `coq` dune-language extension, so a dune-project
containing `(using coq X.Y)` no longer parses whatever its own
`(lang dune ...)` says. opam solves one dune version per switch, so an
uncapped recipe in a closure can select dune >= 3.24 for everything in it.

rocq-elpi-json and rocq-elpi-xml are built out of the same coq-elpi
release tarballs as rocq-elpi -- apps/json/ and apps/xml/ of that tree --
so they are hit by exactly the same defect, and they were missed by every
cap so far because they are missed by name: 34f82e5 capped
rocq-elpi.3.5.0, rocq-prover#3806 capped rocq-elpi.dev, and rocq-prover#3819 capped the
remaining 16 released rocq-elpi/coq-elpi rows, leaving 18 capped rows at
master and these 5 uncapped.

The dune-project files were read out of the three release tarballs these
5 rows name in their own `url { src: }` -- v3.3.1, v3.4.0, v3.5.0 -- not
guessed from opam metadata. All three read `(lang dune 3.13)` on line 1
and `(using coq 0.8)` on line 2.

The cap is satisfiable: rocq-elpi, which every one of these rows depends
on, already asks for `dune {>= "3.13" & < "3.24"}`, and rocq-core.dev /
rocq-runtime.dev ask `dune {>= "3.21"}`, so 3.21-3.23.x satisfies the
whole closure.

Not touched, deliberately: the coq-elpi rows at 2.5.0 and above are
metapackages that depend on rocq-elpi and have no dune dependency and no
build, and the coq-elpi rows below 2.2.0 have no dune dependency either.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
@gares
gares merged commit 6ed7bd0 into rocq-prover:master Aug 12, 2026
3 checks passed
@JasonGross
JasonGross deleted the claude/elpi-json-xml-dune-324 branch August 12, 2026 21:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants