Julien Puydt (Apr 15 2022 at 16:10): 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.
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
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.
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.
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?
Enrico Tassi (Apr 15 2022 at 20:08):I think so, because they are ocaml libraries depending on another ocaml library (coq)
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...
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.
Enrico Tassi (Apr 16 2022 at 07:29):Hum, then what did change? Do we have another reproducibility issues on vo files?
Enrico Tassi (Apr 16 2022 at 07:30):Anyway, elpi libraries depend on the Coq ABI so they should get that dependency
Julien Puydt (Apr 16 2022 at 08:39):I added it. There's also another problem on other architectures: integer too large
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.
Julien Puydt (Apr 16 2022 at 08:44):How can that happen?
Guillaume Melquiond (Apr 16 2022 at 08:49):Because you declared libcoq-stdlib as Architecture: any?
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#L16 — https://unix.stackexchange.com/a/258807/28519 shows the difference and confirms the problem.
Paolo Giarrusso (Apr 16 2022 at 09:31):IOW, .vo files are arch-dependent, so they cannot use Architecture: all AFAICT.
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
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.
Julien Puydt (Apr 17 2022 at 11:50):Oh dear, that's it: libcoq-elpi shouldn't have been Architecture: all... sigh... thanks!
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: Dec 07 2023 at 09:01 UTC