On Fri, Oct 31, 2025 at 04:32:33PM +0100, Julien Puydt wrote: > Hi, > > Le ven. 31 oct. 2025, 12:45, Adrian Bunk <[email protected]> a écrit : > > > > > it looks wrong that the coq rdeps are currently built against coq/sid. > > > > Experimental prefers packages from sid when they fulfill the build > > dependencies, a build dependency on "coq (>= 9)" would be needed for > > building against coq/experimental. > > > > Sigh... I'll need to re-upload the whole lot with your hint... will do next > week.
Since this is only experimental I solved it with a few binNMUs and extra-depends, so whenever rocq-stdlib passes NEW everything currently in experimental should build against the new coq. I found 3 bugs this way (plus a bonus one not in coq): 1. libcoq-stdlib has no dependencies https://buildd.debian.org/status/fetch.php?pkg=aac-tactics&arch=ppc64&ver=9.0.0-1&stamp=1761723185&raw=0 ... Unpacking coq (9.1.0+dfsg-1~ppc64) ... ... Unpacking libcoq-stdlib (8.19.1+dfsg-3) ... ... libcoq-stdlib needs automatic generation of some OCaml/Coq dependencies. 2. libcoq-core misses Breaks+Replaces https://buildd.debian.org/status/fetch.php?pkg=aac-tactics&arch=s390x&ver=9.0.0-1&stamp=1761929973&raw=0 ... Unpacking libcoq-stdlib (8.20.1+dfsg-1+b1) ... dpkg: error processing archive /tmp/apt-dpkg-install-ztHuXt/54-libcoq-stdlib_8.20.1+dfsg-1+b1_s390x.deb (--unpack): trying to overwrite '/usr/lib/s390x-linux-gnu/ocaml/5.3.0/coq/theories/Classes/CMorphisms.glob', which is also in package libcoq-core (9.1.0+dfsg-2) ... apt trying to install this combination of packages is issue 1 above, but the error would also happen for users upgrading. libcoq-core needs Breaks: libcoq-stdlib (<< 9) Replaces: libcoq-stdlib (<< 9) 3. coq-elpi needs a versioned build dependency on elpi https://buildd.debian.org/status/fetch.php?pkg=coq-elpi&arch=arm64&ver=3.2.0-2&stamp=1761837194&raw=0 ... Unpacking libelpi-ocaml (2.0.7-2+b3) ... ... Unpacking elpi (2.0.7-2+b3) ... ... Unpacking libelpi-ocaml-dev (2.0.7-2+b3) ... ... dune build --stop-on-first-error Warning: Cache directories could not be created: Permission denied; disabling cache Hint: Make sure the directory /sbuild-nonexistent/.cache/dune/db/temp can be created File "./theories-stdlib/Vector.v", line 1, characters 0-31: Warning: Using Vector.t is known to be technically difficult, see <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v>. [warn-library-file-stdlib-vector,stdlib-vector,warn-library-file,user-warn,default] File "src/rocq_elpi_utils.ml", lines 146-153, characters 28-44: 146 | ............................(fun ?loc ~id x -> 147 | let loc = Option.map to_coq_loc loc in 148 | let msg = Pp.(hv 0 (Option.cata (fun loc -> Loc.pr loc ++ spc ()) (mt()) loc ++ str x)) in 149 | match id with 150 | | API.Setup.ImplicationPrecedence -> warn_impl ?loc msg 151 | | LinearVariable -> warn_linear ?loc msg 152 | | UndeclaredGlobal -> warn_missing_types ?loc msg 153 | | FlexClause -> warn_flex_clause ?loc msg) Error: This function should have type "string -> unit" but its first argument is labeled "~id" instead of being unlabeled make[2]: *** [Makefile:10: all] Error 1 I'd guess coq-elpi needs elpi >= 3, and this should be in the build dependencies. I've added extra-depends on newer elpi for the package currently in experimental, so no need for a new experimental upload for that. 4. libstdlib-ocaml also lacks OCaml dependencies libstdlib-ocaml also needs automatic generation of some OCaml dependencies similar to issue 1, and to prevent incompatible setups with trixie reverse Breaks as for issue 2 would also be good (no need for Replaces unless a similar issue also exists there). > Sorry, > > J.Puydt cu Adrian
