Julien Puydt (Dec 24 2021 at 12:33): 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...
Karl Palmskog (Dec 24 2021 at 12:50):isn't the META file for Coq 8.14 generated by Dune?
Enrico Tassi (Dec 24 2021 at 13:24):Hum, for 8.15 maybe, for 8.14 I'm afraid not.
Enrico Tassi (Dec 24 2021 at 13:24):In any case there should be a META file (handwritten or generated)
Enrico Tassi (Dec 24 2021 at 13:25):Not sure 8.14 had coq-core, maybe it's just coq.plugins.X
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
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
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.
Enrico Tassi (Dec 24 2021 at 20:25):check it with ocamlfind printconf
Enrico Tassi (Dec 24 2021 at 20:25):and ocamlfind query coq-core
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
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?
Julien Puydt (Dec 24 2021 at 21:20):(ocamlfind query coq-core doesn't find the package)
Gaëtan Gilbert (Dec 24 2021 at 21:21):what does ocamlfind printconf say?
Karl Palmskog (Dec 24 2021 at 21:21):$ ocamlfind printconf
Search path:
/path/to/.opam/4.13.1.coq814/lib
if you don't have /usr/lib in ocamlfind search path, it won't work for sure.
Julien Puydt (Dec 24 2021 at 21:25):no, /usr/lib/ isn't there
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.
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 ?
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.
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
Emilio Jesús Gallego Arias (Dec 25 2021 at 23:26):that's messy yet :( will be solved for 8.16 tho
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
Emilio Jesús Gallego Arias (Dec 25 2021 at 23:27):finally
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