Re: coq rdeps in experimental build against coq/sid
On Fri, Oct 31, 2025 at 04:32:33PM +0100, Julien Puydt wrote:
> Hi,
>
> Le ven. 31 oct. 2025, 12:45, Adrian Bunk <bunk@debian.org> 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
Reply to: