Bound dune < 3.24 for rocq-elpi.dev and rocq-micromega-plugin.dev - #3806
Merged
JasonGross merged 1 commit intoJul 31, 2026
Merged
Conversation
Follow-up to rocq-prover#3802, which bounded 38 extra-dev recipes but not these two. dune 3.24 deleted the `coq` extension: File "dune-project", line 2, characters 0-15: 2 | (using coq 0.8) Error: Extension coq was deleted in the 3.24 version of the dune language Hint: The Coq Build Language has been replaced by the Rocq Build Language. Use (using rocq <version>) instead. Both upstreams still ship it at the ref their `url` names: LPCIC/coq-elpi master is `(lang dune 3.13)` + `(using coq 0.8)`, and rocq-community/micromega-plugin master is `(lang dune 3.8)` + `(using coq 0.8)`. The extension is rejected regardless of the project's own `(lang dune ...)` version, so the build dies at `dune subst` before anything is compiled. Because both are common dependencies, this is currently failing CI on unrelated pull requests: rocq-prover#3693 (coq-wasm.dev) and rocq-prover#3790 (coq-mathcomp-dioid.dev) both die with `The compilation of rocq-elpi.dev failed at "dune subst"`. `opam lint` passes on both files under the opam 2.1.2 that .gitlab-ci.yml pins. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
This was referenced Jul 31, 2026
gares
pushed a commit
that referenced
this pull request
Aug 6, 2026
…ing the deleted (using coq) extension dune 3.24 removed the `coq` dune-language extension, so any dune-project containing `(using coq X.Y)` now fails to parse regardless of its own `(lang dune ...)` version. opam solves one dune version per switch, so a single uncapped recipe 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 keeps being escaped: #3806 capped rocq-elpi.dev, after which the solver chose rocq-elpi 3.5.0; #3795 capped 3.5.0, after which it chose 3.4.0. 3.4.0 is uncapped, as is every released rocq-elpi below it, and it is currently failing in the archive's own CI with Error: Extension coq was deleted in the 3.24 version of the dune language taking the mathcomp stack down with it. Capping only the newest version each time leaves the next one down to be selected, so this closes the remaining released versions. The affected dune-project files were read out of all 16 release tarballs -- the url { src: } target in each opam file, i.e. the tree opam actually builds -- rather than guessed from the opam metadata. All 16 read `(lang dune 3.13)` / `(using coq 0.8)`. rocq-elpi.3.5.0 is deliberately untouched; #3795 already capped it, and its depends: line was the byte-for-byte spelling control here. coq-elpi 2.5.0 and later need no change either: they are metapackages depending only on coq-core and rocq-elpi {= version}, so they inherit the cap. Nothing becomes unsatisfiable -- no recipe in released/, core-dev/ or extra-dev/ requires dune >= 3.24 -- and 83 recipes on master already carry this same upper bound. This is not an archive-wide sweep: other affected packages remain uncapped and are not addressed here. 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
dune 3.24 deleted the `coq` dune-language extension, so a `dune-project` containing `(using coq X.Y)` no longer parses regardless of its own `(lang dune ...)`. Both rows are built from `apps/json/` and `apps/xml/` of the coq-elpi tree, whose `dune-project` carries `(using coq 0.8)`. opam solves one dune version per switch, so an uncapped recipe in a closure can select dune >= 3.24 for everything in it. Same spelling as the caps already merged for the released rows (rocq-prover#3806, rocq-prover#3819). Satisfiable: `rocq-elpi`, which both rows depend on, already asks `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 both files. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
gares
pushed a commit
that referenced
this pull request
Aug 12, 2026
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, #3806 capped rocq-elpi.dev, and #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
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.
Follow-up to #3802, which bounded 38 extra-dev recipes but not these two.
dune 3.24 deleted the
coqextension:File "dune-project", line 2, characters 0-15:
2 | (using coq 0.8)
Error: Extension coq was deleted in the 3.24 version of the dune language
Hint: The Coq Build Language has been replaced by the Rocq Build Language.
Use (using rocq ) instead.
Both upstreams still ship it at the ref their
urlnames:LPCIC/coq-elpi master is
(lang dune 3.13)+(using coq 0.8), androcq-community/micromega-plugin master is
(lang dune 3.8)+(using coq 0.8).The extension is rejected regardless of the project's own
(lang dune ...)version, so the build dies at
dune substbefore anything is compiled.Because both are common dependencies, this is currently failing CI on unrelated
pull requests: #3693 (coq-wasm.dev) and #3790 (coq-mathcomp-dioid.dev) both die
with
The compilation of rocq-elpi.dev failed at "dune subst".opam lintpasses on both files under the opam 2.1.2 that .gitlab-ci.yml pins.🤖 Generated with Claude Code
https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b