From 5cc0339203bbb33922ac22bed55a7cd22bd994c3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 31 Jul 2026 19:21:45 +0000 Subject: [PATCH] Bound dune < 3.24 for rocq-elpi.dev and rocq-micromega-plugin.dev 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 ) 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. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b --- extra-dev/packages/rocq-elpi/rocq-elpi.dev/opam | 2 +- .../rocq-micromega-plugin/rocq-micromega-plugin.dev/opam | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/extra-dev/packages/rocq-elpi/rocq-elpi.dev/opam b/extra-dev/packages/rocq-elpi/rocq-elpi.dev/opam index 608dcbdac..5740ecf88 100644 --- a/extra-dev/packages/rocq-elpi/rocq-elpi.dev/opam +++ b/extra-dev/packages/rocq-elpi/rocq-elpi.dev/opam @@ -15,7 +15,7 @@ tags: [ homepage: "https://github.com/LPCIC/coq-elpi" bug-reports: "https://github.com/LPCIC/coq-elpi/issues" depends: [ - "dune" {>= "3.13"} + "dune" {>= "3.13" & < "3.24"} "ocaml" {>= "4.10.0"} "elpi" {>= "3.7.1"} "rocq-core" {>= "9.0"} diff --git a/extra-dev/packages/rocq-micromega-plugin/rocq-micromega-plugin.dev/opam b/extra-dev/packages/rocq-micromega-plugin/rocq-micromega-plugin.dev/opam index 413312f6b..fd6b2624d 100644 --- a/extra-dev/packages/rocq-micromega-plugin/rocq-micromega-plugin.dev/opam +++ b/extra-dev/packages/rocq-micromega-plugin/rocq-micromega-plugin.dev/opam @@ -12,7 +12,7 @@ tags: [ homepage: "https://github.com/rocq-community/micromega-plugin" bug-reports: "https://github.com/rocq-community/micromega-plugin/issues" depends: [ - "dune" {>= "3.8"} + "dune" {>= "3.8" & < "3.24"} "ocaml" {>= "4.09.0"} "rocq-core" {>= "9.0"} "ppx_optcomp"