Stream: Coq devs & plugin devs

Topic: ✔ Compiled library elpi.elpi (in file /usr/lib/ocaml/coq/...


view this post on Zulip Julien Puydt (Apr 15 2022 at 16:10):

I have trouble with the Debian packages for coq stuff: for example, the current coq-hierarchy-builder is broken on arm64 ; the error message is the subject of this topic.

The problem is that I upload source packages to Debian, and they get compiled on the various architectures by build servers ; and for most architectures, the above issue just doesn't exist! So I'm a bit at loss as to why there is something broken in some cases and not in others. There are in fact two questions there: why is it broken? how to fix the issue properly?

I have the following idea for the why -- I'm not sure how well is flies: at some point I uploaded coq, elpi, coq-elpi and coq-hierarchy-builder ; most architectures hence built them in that order, but some slower ones ended up compiling in order elpi, coq-elpi, coq, coq-hierarchy-builder. That breaks because coq-elpi comes from an old coq.

For the how... apart from uploading new versions slowly enough to make sure everything gets in place, I don't know.

view this post on Zulip Gaëtan Gilbert (Apr 15 2022 at 16:20):

the error message is the subject of this topic.

it got eaten by length limits

some slower ones ended up compiling in order elpi, coq-elpi, coq, coq-hierarchy-builder.

coq-elpi depends on coq

view this post on Zulip Enrico Tassi (Apr 15 2022 at 17:48):

apparently you compiled coq-elpi against one version of coq, and you are compiling hb against another one.

view this post on Zulip Enrico Tassi (Apr 15 2022 at 17:52):

as for ocaml, you must trigger bin nmus if you don't follow topological order when you upload.

view this post on Zulip Julien Puydt (Apr 15 2022 at 19:09):

@Gaëtan Gilbert Yes, I know coq-elpi depends on coq, but there's an old coq, there's a new coq.

@Enrico Tassi There should be some kind of dependance to trigger new builds automatically when a new coq is available. I thought the tricks with coq-${F:CoqABI} (see here) did just that, but apparently, it doesn't. Or perhaps also libcoq-elpi-ocaml and libcoq-elpi-ocaml-dev should also get that?

view this post on Zulip Enrico Tassi (Apr 15 2022 at 20:08):

I think so, because they are ocaml libraries depending on another ocaml library (coq)

view this post on Zulip Julien Puydt (Apr 16 2022 at 05:55):

Hmm..., coq-${F:CoqABI} is about coq (and doesn't seem to do much), and I don't think ${ocaml:Depends} does anything for coq files...

view this post on Zulip Guillaume Melquiond (Apr 16 2022 at 06:41):

Julien Puydt said:

I thought the tricks with coq-${F:CoqABI} (see here) did just that, but apparently, it doesn't.

It does, but that is only if the value of ${F:CoqABI} changes between two consecutive upload. Since the value stayed the same, the system cannot notice the change.

view this post on Zulip Enrico Tassi (Apr 16 2022 at 07:29):

Hum, then what did change? Do we have another reproducibility issues on vo files?

view this post on Zulip Enrico Tassi (Apr 16 2022 at 07:30):

Anyway, elpi libraries depend on the Coq ABI so they should get that dependency

view this post on Zulip Julien Puydt (Apr 16 2022 at 08:39):

I added it. There's also another problem on other architectures: integer too large

view this post on Zulip Guillaume Melquiond (Apr 16 2022 at 08:42):

The "integer too large" message means that you are trying to load a 64-bit library on a 32-bit system.

view this post on Zulip Julien Puydt (Apr 16 2022 at 08:44):

How can that happen?

view this post on Zulip Guillaume Melquiond (Apr 16 2022 at 08:49):

Because you declared libcoq-stdlib as Architecture: any?

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 09:28):

Architecture: all for libcoq-elpi is also suspicious in https://salsa.debian.org/ocaml-team/coq-elpi/-/blob/master/debian/control#L16https://unix.stackexchange.com/a/258807/28519 shows the difference and confirms the problem.

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 09:31):

IOW, .vo files are arch-dependent, so they cannot use Architecture: all AFAICT.

view this post on Zulip Karl Palmskog (Apr 16 2022 at 09:58):

I think this [arch dependence of stdlib] is due to OCaml Marshal serialization of .vo files, right? Marshal is tied to the OCaml compiler and platform

view this post on Zulip Guillaume Melquiond (Apr 16 2022 at 10:03):

Yes, but not just that. For instance, if the .v files use primitive integers, their representation changes depending on the architecture, irrespective of the actual implementation of OCaml's serialization.

view this post on Zulip Julien Puydt (Apr 17 2022 at 11:50):

Oh dear, that's it: libcoq-elpi shouldn't have been Architecture: all... sigh... thanks!

view this post on Zulip Julien Puydt (Apr 17 2022 at 12:01):

I tracked down other places where I made the same mistake... things should be smoother now!


Last updated: May 31 2023 at 15:01 UTC