Stream: SerAPI

Topic: ✔ Trouble packaging for Debian


view this post on Zulip Julien Puydt (May 20 2022 at 11:42):

I thought I had problems with coq, and reported there, but apparently the root of the matter isn't clear.

Perhaps someone here has a better clue?

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2022 at 11:48):

That's pretty weird, maybe the symbols of coq-core were stripped incorrectly?

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2022 at 11:49):

I suggest to try a (local) build of serapi using dune build -p coq-serapi and then please paste the full _build/log

view this post on Zulip Julien Puydt (May 20 2022 at 11:56):

It's a 816-lines log!

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2022 at 12:16):

Yes, put in in pastebin for examlpe

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2022 at 12:16):

It is debug information, it is normal it is detailed

view this post on Zulip Julien Puydt (May 20 2022 at 12:19):

The log is 576k ; it's bigger than what is accepted in the pastebin sites I have tried until now

view this post on Zulip Julien Puydt (May 20 2022 at 12:20):

I cut the middle part here

view this post on Zulip Julien Puydt (May 20 2022 at 12:21):

Hopefully what you're interested in is the start & end.

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2022 at 12:37):

Thanks, so it seems the symbols exported have been cleaned, as in https://bytemeta.vip/repo/ocaml/dune/issues/5559 right?

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2022 at 12:38):

Where is the debian/rules file for coq ?

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2022 at 12:40):

The reason aac tactics is not failing is likely because coq makefile is not building the static object files

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2022 at 12:40):

we could try that too, but I'd be good to understand what's going on frist

view this post on Zulip Karl Palmskog (May 20 2022 at 12:41):

note that AAC tactics can be built with Dune, if you prefer

view this post on Zulip Karl Palmskog (May 20 2022 at 12:41):

but the default build uses coq_makefile

view this post on Zulip Julien Puydt (May 20 2022 at 12:42):

Here is debian/rules ; and indeed it's stripping things... I don't know why

view this post on Zulip Julien Puydt (May 20 2022 at 12:42):

It doesn't seem to be a problem for other pieces of software.

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2022 at 12:59):

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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2022 at 14:02):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2022 at 14:02):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2022 at 14:03):

we can update that centrally

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (May 20 2022 at 16:22):

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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2022 at 19:05):

that's like 40% of opam

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2022 at 20:59):

I dunno what the good name for that would be

view this post on Zulip Emilio Jesús Gallego Arias (May 22 2022 at 20:59):

maybe dune_build ?

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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:

  1. it's only coq, not coq-related packages ;
  2. 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).

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Julien Puydt (May 23 2022 at 13:35):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 23 2022 at 16:22):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 23 2022 at 16:22):

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

view this post on Zulip 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?

view this post on Zulip 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:

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

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

Thanks!

view this post on Zulip Notification Bot (May 25 2022 at 21:20):

Julien Puydt has marked this topic as resolved.

view this post on Zulip 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