Update mathcomp-dioid dev dependencies - #3790
Open
JasonGross wants to merge 1 commit into
Open
Conversation
JasonGross
force-pushed
the
codex/update-dioid-dev
branch
from
July 31, 2026 19:22
35d948c to
2c42c80
Compare
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>
JasonGross
force-pushed
the
codex/update-dioid-dev
branch
4 times, most recently
from
July 31, 2026 21:28
032027e to
4c2d05f
Compare
JasonGross
marked this pull request as ready for review
August 6, 2026 04:05
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.
The
coq-mathcomp-dioid.devmetadata describes the old Coq 8.13 / MathComp 1.x implementation, so current development switches reject it and may fall back to the incompatible 0.1 release when constraints are ignored. Upstream Dioid master has moved to Hierarchy Builder and the split MathComp package hierarchy; this updates the dev dependencies to match that implementation and math-comp/dioid#1.The source remains the upstream
math-comp/dioidmaster branch, not the theorem-labs fork. This draft must not merge until the upstream compatibility PR lands.opam lintpasses without warnings, and the upstream compatibility branch builds completely againstrocq-dev-testingwithmake -j4.The remaining red build is expected because upstream
math-comp/dioid#masterdoes not yet carry the migration.complete_lattice.vfails with:The
T & F Tbinder syntax is core Rocq grammar from rocq-prover/rocq#21611 (merged 2026-02-26, first tagged in 9.3+rc1), replacing ssreflect'sT of F T.Packages that can never be installed:is empty, so the solver is satisfied and only the source is stale.ci-skipremains until math-comp/dioid#1 merges.ci-skip: coq-mathcomp-dioid
Wordsmithed by Codex.