From ff9ee8713249373965d2bfd673e71637eb05ff08 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 11 Aug 2026 15:23:54 +0000 Subject: [PATCH] rocq-elpi-json, rocq-elpi-xml: bound dune < 3.24 on the 5 released rows 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: 34f82e57a 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 Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b --- released/packages/rocq-elpi-json/rocq-elpi-json.3.3.1/opam | 2 +- released/packages/rocq-elpi-json/rocq-elpi-json.3.4.0/opam | 2 +- released/packages/rocq-elpi-json/rocq-elpi-json.3.5.0/opam | 2 +- released/packages/rocq-elpi-xml/rocq-elpi-xml.3.4.0/opam | 2 +- released/packages/rocq-elpi-xml/rocq-elpi-xml.3.5.0/opam | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/released/packages/rocq-elpi-json/rocq-elpi-json.3.3.1/opam b/released/packages/rocq-elpi-json/rocq-elpi-json.3.3.1/opam index abbf52391..c299b261e 100644 --- a/released/packages/rocq-elpi-json/rocq-elpi-json.3.3.1/opam +++ b/released/packages/rocq-elpi-json/rocq-elpi-json.3.3.1/opam @@ -8,7 +8,7 @@ license: "LGPL-2.1-or-later" homepage: "https://github.com/LPCIC/coq-elpi/apps/json/" bug-reports: "https://github.com/LPCIC/coq-elpi/issues" depends: [ - "dune" {>= "3.13"} + "dune" {>= "3.13" & < "3.24"} "rocq-elpi" "yojson" "odoc" {with-doc} diff --git a/released/packages/rocq-elpi-json/rocq-elpi-json.3.4.0/opam b/released/packages/rocq-elpi-json/rocq-elpi-json.3.4.0/opam index ac2b2b8f8..04dee74e5 100644 --- a/released/packages/rocq-elpi-json/rocq-elpi-json.3.4.0/opam +++ b/released/packages/rocq-elpi-json/rocq-elpi-json.3.4.0/opam @@ -8,7 +8,7 @@ license: "LGPL-2.1-or-later" homepage: "https://github.com/LPCIC/coq-elpi/apps/json/" bug-reports: "https://github.com/LPCIC/coq-elpi/issues" depends: [ - "dune" {>= "3.13"} + "dune" {>= "3.13" & < "3.24"} "rocq-elpi" "yojson" "odoc" {with-doc} diff --git a/released/packages/rocq-elpi-json/rocq-elpi-json.3.5.0/opam b/released/packages/rocq-elpi-json/rocq-elpi-json.3.5.0/opam index 6d6937784..1a8e7a305 100644 --- a/released/packages/rocq-elpi-json/rocq-elpi-json.3.5.0/opam +++ b/released/packages/rocq-elpi-json/rocq-elpi-json.3.5.0/opam @@ -8,7 +8,7 @@ license: "LGPL-2.1-or-later" homepage: "https://github.com/LPCIC/coq-elpi/apps/json/" bug-reports: "https://github.com/LPCIC/coq-elpi/issues" depends: [ - "dune" {>= "3.13"} + "dune" {>= "3.13" & < "3.24"} "rocq-elpi" "yojson" "odoc" {with-doc} diff --git a/released/packages/rocq-elpi-xml/rocq-elpi-xml.3.4.0/opam b/released/packages/rocq-elpi-xml/rocq-elpi-xml.3.4.0/opam index 91e06646a..4b54c34bc 100644 --- a/released/packages/rocq-elpi-xml/rocq-elpi-xml.3.4.0/opam +++ b/released/packages/rocq-elpi-xml/rocq-elpi-xml.3.4.0/opam @@ -8,7 +8,7 @@ license: "LGPL-2.1-or-later" homepage: "https://github.com/LPCIC/coq-elpi/apps/xml/" bug-reports: "https://github.com/LPCIC/coq-elpi/issues" depends: [ - "dune" {>= "3.13"} + "dune" {>= "3.13" & < "3.24"} "rocq-elpi" "xml-light" "odoc" {with-doc} diff --git a/released/packages/rocq-elpi-xml/rocq-elpi-xml.3.5.0/opam b/released/packages/rocq-elpi-xml/rocq-elpi-xml.3.5.0/opam index 5f3887780..d39d07e6a 100644 --- a/released/packages/rocq-elpi-xml/rocq-elpi-xml.3.5.0/opam +++ b/released/packages/rocq-elpi-xml/rocq-elpi-xml.3.5.0/opam @@ -8,7 +8,7 @@ license: "LGPL-2.1-or-later" homepage: "https://github.com/LPCIC/coq-elpi/apps/xml/" bug-reports: "https://github.com/LPCIC/coq-elpi/issues" depends: [ - "dune" {>= "3.13"} + "dune" {>= "3.13" & < "3.24"} "rocq-elpi" "xml-light" "odoc" {with-doc}