Stream: SerAPI

Topic: Not found libraries


view this post on Zulip Julien Puydt (Dec 24 2021 at 12:33):

I'm trying to get my hand in serapi again (not looking at licensing yet ; I wanted to see the technical side after packaging ppx-import), and I get a lot of complaints from dune not finding libraries (coq-core.plugins.ssrmatching, for instance) ; there is no META file from coq 8.14, so that might explain it...

view this post on Zulip Karl Palmskog (Dec 24 2021 at 12:50):

isn't the META file for Coq 8.14 generated by Dune?

view this post on Zulip Enrico Tassi (Dec 24 2021 at 13:24):

Hum, for 8.15 maybe, for 8.14 I'm afraid not.

view this post on Zulip Enrico Tassi (Dec 24 2021 at 13:24):

In any case there should be a META file (handwritten or generated)

view this post on Zulip Enrico Tassi (Dec 24 2021 at 13:25):

Not sure 8.14 had coq-core, maybe it's just coq.plugins.X

view this post on Zulip Karl Palmskog (Dec 24 2021 at 13:26):

It had coq-core alright: https://github.com/coq-community/aac-tactics/blob/v8.14/src/dune#L5

view this post on Zulip Julien Puydt (Dec 24 2021 at 15:56):

There's a /usr/lib/coq-core/META file, but I'm not sure it's found

view this post on Zulip Théo Zimmermann (Dec 24 2021 at 16:00):

Karl Palmskog said:

isn't the META file for Coq 8.14 generated by Dune?

Yes, I'm pretty sure it is.

view this post on Zulip Enrico Tassi (Dec 24 2021 at 20:25):

check it with ocamlfind printconf

view this post on Zulip Enrico Tassi (Dec 24 2021 at 20:25):

and ocamlfind query coq-core

view this post on Zulip Karl Palmskog (Dec 24 2021 at 20:26):

opam-based 8.14 install gives the following:

$ ocamlfind query coq-core
/path/to/.opam/4.13.1.coq814/lib/coq-core

So if the build follows the opam one (via Dune), there should be a META

view this post on Zulip Julien Puydt (Dec 24 2021 at 21:19):

Well, as I said, there's a /usr/lib/coq-core/META file -- so there is one -- the question is : why should tools find it?

view this post on Zulip Julien Puydt (Dec 24 2021 at 21:20):

(ocamlfind query coq-core doesn't find the package)

view this post on Zulip Gaëtan Gilbert (Dec 24 2021 at 21:21):

what does ocamlfind printconf say?

view this post on Zulip Karl Palmskog (Dec 24 2021 at 21:21):

$ ocamlfind printconf
Search path:
    /path/to/.opam/4.13.1.coq814/lib

view this post on Zulip Karl Palmskog (Dec 24 2021 at 21:22):

if you don't have /usr/lib in ocamlfind search path, it won't work for sure.

view this post on Zulip Julien Puydt (Dec 24 2021 at 21:25):

no, /usr/lib/ isn't there

view this post on Zulip Karl Palmskog (Dec 24 2021 at 21:27):

then I guess ocamlfind installation doesn't work as expected out of the box. In all opam installations of ocamlfind, it finds the local lib.

view this post on Zulip Julien Puydt (Dec 24 2021 at 21:30):

Hmmm... shouldn't it rather be on coq-core to get installed in /usr/lib/ocaml/ instead of /usr/lib ?

view this post on Zulip Karl Palmskog (Dec 24 2021 at 21:31):

if your Debian configuration mandates /usr/lib/ocaml, then sure. But it's not the default for OCaml or opam in general.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 25 2021 at 23:26):

Debian's dune should indeed install the libs in the right place, however maybe we are overriding --libdir in the makefiles

view this post on Zulip Emilio Jesús Gallego Arias (Dec 25 2021 at 23:26):

that's messy yet :( will be solved for 8.16 tho

view this post on Zulip Emilio Jesús Gallego Arias (Dec 25 2021 at 23:27):

I wrote most of the coq_dune patch the other day in the plane to spain

view this post on Zulip Emilio Jesús Gallego Arias (Dec 25 2021 at 23:27):

finally

view this post on Zulip Julien Puydt (Dec 26 2021 at 00:50):

I build using dune, I install using dune ; I don't think Makefile's are involved. If I don't use --libdir, everything is in /usr/lib/coq-core and /usr/lib/coq, so ocamlfind doesn't see the coq-core OCaml libs, but coq finds its prelude. If I use --libdir, I can get /usr/lib/ocaml/coq-core and that makes ocamlfind happy, but then there is also /usr/lib/ocaml/coq and coq doesn't find its prelude. I'm in either win-lose or lose-win, there's no win-win!


Last updated: Feb 06 2023 at 05:03 UTC