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?
That's pretty weird, maybe the symbols of coq-core were stripped incorrectly?
I suggest to try a (local) build of serapi using dune build -p coq-serapi
and then please paste the full _build/log
It's a 816-lines log!
Yes, put in in pastebin for examlpe
It is debug information, it is normal it is detailed
The log is 576k ; it's bigger than what is accepted in the pastebin sites I have tried until now
I cut the middle part here
Hopefully what you're interested in is the start & end.
Thanks, so it seems the symbols exported have been cleaned, as in https://bytemeta.vip/repo/ocaml/dune/issues/5559 right?
Where is the debian/rules
file for coq ?
The reason aac tactics is not failing is likely because coq makefile is not building the static object files
we could try that too, but I'd be good to understand what's going on frist
note that AAC tactics can be built with Dune, if you prefer
but the default build uses coq_makefile
Here is debian/rules ; and indeed it's stripping things... I don't know why
It doesn't seem to be a problem for other pieces of software.
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
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.
Good to hear, thanks for looking into this @Julien Puydt
Maybe we should get in touch with the OCaml Debian people, they are a bit busy
I think we should have something like dh_dune that should take care of all these complex policy stuff
and moreover, when dune gets support for debian-compatible install files
we can update that centrally
And I guess eventually you want the stripping for some of the binaries but not for the dev libs?
(IIUC as Emilio said above). But luckily this is just a space optimization
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...
@Julien Puydt dh_dune would be very useful for all the packages that follow a standard dune build
that's like 40% of opam
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...
yes, dh_dune should be part of dh-ocaml in the same way pybuild
is part of dh-python
I dunno what the good name for that would be
maybe dune_build ?
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...
actually if we manage to use dune as a standard build too for Coq
then dh_coq would only have to inspect dune's (theories fields to make the deps for the packages
I don't know... we do have some hack to compute a CoqABI and make the package depend on it, but:
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
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...
Does the ocaml ABI dep have something to do with "inconsistent assumtions" ?
Yes, that basically is, a md5 sum of the interfaces contents I think
Similar to Coq, plus Coq also does the checksums of the .vo files
Then why would Coq find inconsistent assumptions if the only change is not stripping *.a files? Does that do anything to the .vo?
Ok, I dived again in my tentative Debian package for coq-serapi ; what I'm lacking before I can upload it is:
That particular topic is closed, since now everything builds fine.
Thanks!
Julien Puydt has marked this topic as resolved.
I will fix the licensing ASAP, sorry for that problem
Last updated: May 31 2023 at 02:31 UTC