Bound dune < 3.24 on extra-dev packages still using the coq extension - #3802
Merged
Conversation
dune 3.24 deleted the `coq` extension: Error: Extension coq was deleted in the 3.24 version of the dune language Hint: ... Use (using rocq <version>) instead. Any project whose dune-project still contains `(using coq X.Y)` now fails even at `dune subst`, regardless of its own `(lang dune ...)` version -- verified with both `(lang dune 3.8)` and `(lang dune 3.13)`. Since dune 3.24.0/3.24.1 are in opam-repository, the solver picks them and the build dies before anything is compiled. core-dev already carries this exact bound on 39 recipes; these 38 extra-dev recipes were missed. Each was checked by fetching its upstream dune-project at the ref its `url` names and confirming that it still uses `(using coq ...)`; packages whose upstream has migrated to `(using rocq ...)` are deliberately untouched. `opam lint --warn=-21` passes on all 38 under the opam 2.1.2 that .gitlab-ci.yml pins (the only pre-existing complaint is a synopsis warning 47 on coq-quickchick.dev, unchanged by this commit and not an error). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
JasonGross
added a commit
that referenced
this pull request
Jul 31, 2026
) Follow-up to #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: #3693 (coq-wasm.dev) and #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. Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
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.
dune 3.24 deleted the
coqextension, so any project whosedune-projectstill contains
(using coq X.Y)now fails atdune subst:This is independent of the project's own
(lang dune ...)version — I checkedboth
(lang dune 3.8)and(lang dune 3.13)and they fail alike. dune 3.24.0and 3.24.1 are in opam-repository, so the solver picks one and the build dies
before anything is compiled.
This is the archive's established remedy, applied where it was missed.
core-devalready carries a< "3.24"bound on 39 recipes; these 38extra-devrecipes did not have it.
How the list was built. For every
extra-dev/core-devrecipe with both adunedependency and aurl, I fetched the upstreamdune-projectat the refthe
urlnames and checked whether it still uses(using coq ...). 538 opamfiles scanned, 173 had a dune dep + url, 40 came back broken. Two of those 40
(
rocq-elpi.dev,rocq-micromega-plugin.dev) are already fixed in #3789, so 38are here. Recipes whose upstream has migrated to
(using rocq ...)aredeliberately untouched.
Verification.
opam lint --warn=-21passes on all 38 under the opam 2.1.2that
.gitlab-ci.ymlpins. The only complaint anywhere is a pre-existingsynopsis warning 47 on
coq-quickchick.dev, which this PR does not touch andwhich is a warning, not an error. The fix itself was proven rather than inferred
from the error text:
dune subston coq-elpi master succeeds with dune 3.23.1and fails with 3.24, and in #3789 the same one-line bound turned
opam-build:4.14.2andopam-build:5.3.0from red to green.What this does not fix. The bound only ensures these packages get a dune that
can still read their
dune-project. Several of them may still fail to buildagainst Rocq dev for source-level reasons, which CI here will now surface for the
first time (before this change they could not get far enough to try). The
durable fix in each case is upstream migrating to
(using rocq ...); this boundis what keeps the archive working until then.
🤖 Generated with Claude Code
https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b