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.
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
apparently you compiled coq-elpi against one version of coq, and you are compiling hb against another one.
as for ocaml, you must trigger bin nmus if you don't follow topological order when you upload.
@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?
I think so, because they are ocaml libraries depending on another ocaml library (coq)
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...
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.
Hum, then what did change? Do we have another reproducibility issues on vo files?
Anyway, elpi libraries depend on the Coq ABI so they should get that dependency
I added it. There's also another problem on other architectures: integer too large
The "integer too large" message means that you are trying to load a 64-bit library on a 32-bit system.
How can that happen?
Because you declared libcoq-stdlib
as Architecture: any
?
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.
IOW, .vo files are arch-dependent, so they cannot use Architecture: all
AFAICT.
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
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.
Oh dear, that's it: libcoq-elpi shouldn't have been Architecture: all... sigh... thanks!
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