✔ Trouble packaging for Debian · SerAPI

A bit of a guess, but I think that stripping is done to save download size for regular packages, however, then for packages like serapi that wish to build static files you need a libcoq-core-dev that includes these symbols.

I'm afraid that how to handle this is beyond my Debian expertise

Julien Puydt (May 20 2022 at 13:25):

I tried to build a set of coq packages without the stripping. That makes the coq-serapi issue go away.

I'll now check this set of coq packages doesn't break everything, and it that's the case, I'll upload them to Debian and the problem will be solved.

Emilio Jesús Gallego Arias (May 20 2022 at 14:02):

Good to hear, thanks for looking into this @Julien Puydt

Emilio Jesús Gallego Arias (May 20 2022 at 14:02):

Maybe we should get in touch with the OCaml Debian people, they are a bit busy

Emilio Jesús Gallego Arias (May 20 2022 at 14:02):

I think we should have something like dh_dune that should take care of all these complex policy stuff

Emilio Jesús Gallego Arias (May 20 2022 at 14:02):

and moreover, when dune gets support for debian-compatible install files

Emilio Jesús Gallego Arias (May 20 2022 at 14:03):

we can update that centrally

Paolo Giarrusso (May 20 2022 at 16:21):

And I guess eventually you want the stripping for some of the binaries but not for the dev libs?

Paolo Giarrusso (May 20 2022 at 16:22):

(IIUC as Emilio said above). But luckily this is just a space optimization

Julien Puydt (May 20 2022 at 19:13):

I don't think we want a dh_dune, since after all dune is just a build system. What we want is probably a dh_coq -- something that will detect the deps with some subtlety and make it possible to transition cleanly.

For example, not stripping the libs seems to have broken... mostly everything! And it's not clear to me why...

Emilio Jesús Gallego Arias (May 22 2022 at 19:05):

@Julien Puydt dh_dune would be very useful for all the packages that follow a standard dune build

Emilio Jesús Gallego Arias (May 22 2022 at 19:05):

that's like 40% of opam

Enrico Tassi (May 22 2022 at 20:53):

dh_foo takes care of the subtleties of foo. It is typically a PL, not a build system. E.g. dh_python, dh_perl, dh_lua, dh_ruby...

Emilio Jesús Gallego Arias (May 22 2022 at 20:59):

yes, dh_dune should be part of dh-ocaml in the same way pybuild is part of dh-python

Emilio Jesús Gallego Arias (May 22 2022 at 20:59):

I dunno what the good name for that would be

Emilio Jesús Gallego Arias (May 22 2022 at 20:59):

maybe dune_build ?

Julien Puydt (May 23 2022 at 11:40):

Ah, completing dh_ocaml so it supports dune builds, yes.

And dh_coq because I'm having big issues of binary compatibility with sets of packages...

Emilio Jesús Gallego Arias (May 23 2022 at 12:37):

actually if we manage to use dune as a standard build too for Coq

Emilio Jesús Gallego Arias (May 23 2022 at 12:38):

then dh_coq would only have to inspect dune's (theories fields to make the deps for the packages

Julien Puydt (May 23 2022 at 13:06):

I don't know... we do have some hack to compute a CoqABI and make the package depend on it, but:

it's only coq, not coq-related packages ;
if it actually worked, I wouldn't have uploaded by hand a half-dozen packages already and needing some more because the ABI was broken (a story of inconsistent assumptions).

Emilio Jesús Gallego Arias (May 23 2022 at 13:18):

ABI for Coq is exactly the same as the OCaml ABI, so how much can be shared I don't know, but likely a lot

Julien Puydt (May 23 2022 at 13:33):

Well, all I know is that I stopped stripping coq's .a files ; that apparently didn't change the CoqABI since they all kept installable. But none was usable...

Julien Puydt (May 23 2022 at 13:35):

Does the ocaml ABI dep have something to do with "inconsistent assumtions" ?

Emilio Jesús Gallego Arias (May 23 2022 at 16:22):

Yes, that basically is, a md5 sum of the interfaces contents I think

Emilio Jesús Gallego Arias (May 23 2022 at 16:22):

Similar to Coq, plus Coq also does the checksums of the .vo files

Julien Puydt (May 23 2022 at 16:36):

Then why would Coq find inconsistent assumptions if the only change is not stripping *.a files? Does that do anything to the .vo?

Julien Puydt (May 25 2022 at 21:20):

Ok, I dived again in my tentative Debian package for coq-serapi ; what I'm lacking before I can upload it is:

clear licensing
perhaps patching sertop.el (see other topic this evening).

That particular topic is closed, since now everything builds fine.

Thanks!

Notification Bot (May 25 2022 at 21:20):

Julien Puydt has marked this topic as resolved.

Emilio Jesús Gallego Arias (May 26 2022 at 10:39):

I will fix the licensing ASAP, sorry for that problem

Last updated: May 31 2023 at 02:31 UTC