Adrian Dapprich (Dec 09 2020 at 13:21): Adrian Dapprich (Dec 09 2020 at 13:21):Hello, I'm currently writing a plugin for Coq and right now I'm having a problem with making my ocaml code available to Coq. I'm using ocaml 4.11.1 and coq 8.12.1 from opam and dune to compile my project.
The problem seems to be that Coq cannot find certain libraries that I used in my ocaml code. I was following the coq-plugin-template (https://github.com/ejgallego/coq-plugin-template) where it shows how make Coq discover external libraries like z3 but I could not reproduce what's written in the readme there.
When I follow the directions in the readme, Coq is able to find the z3ml.cmxs but then it appears Coq cannot find any transitively required libraries (concretely z3 uses some module Q for rational numbers which Coq cannot find). I had the same experience when I tried to load my plugin which uses the standard library replacement Base and ocamlgraph.
So have I been missing something described in the coq-plugin-template or is there a better way than described how I can make Coq discover the external ocaml libraries that I use?
Adrian Dapprich (Dec 09 2020 at 13:24):like, should I rather use a _CoqPorject which seems to be used sometimes?
Enrico Tassi (Dec 09 2020 at 13:24):This is a current limitation of dune/coq.
If you use coq_makefile you can link extra code via findlib quite easily, see: https://github.com/LPCIC/coq-elpi/blob/master/Makefile.coq.local#L1
Enrico Tassi (Dec 09 2020 at 13:26):This way the extra code is linked to your plugin. This approach has the drawback that if you load two plugins with a common dep, the dep is loaded twice, which is unsafe. But at least you can build and load your plugin.
Enrico Tassi (Dec 09 2020 at 13:27):The right solution is link findlib (or something similar) into Coq, and have it do the job of a loader. But we are not there yet.
Adrian Dapprich (Dec 09 2020 at 13:33):ah okay that's unfortunate, then I will try it without dune. afaiu the normal way is then to write a _CoqProject with all my ocaml sources + loader.v, use coq_makefile to generate a Makefile and then add my packages to the CAMLPKGS env var there, correct?
Enrico Tassi (Dec 09 2020 at 13:53):yes
Emilio Jesús Gallego Arias (Dec 09 2020 at 14:01):You can also link the external libraries using dune + linkall, however that won't work well both in coq_makefile or dune due to recent OCaml versions forbidding double-linking
Emilio Jesús Gallego Arias (Dec 09 2020 at 14:04):See https://dune.readthedocs.io/en/stable/advanced-topics.html?highlight=cmxa#building-an-ad-hoc-cmxs on how to build your custom cmxs with linkall for example
Emilio Jesús Gallego Arias (Dec 09 2020 at 14:04):however that doesn't integrate fully seamlessly with (coq.theory yet
Enrico Tassi (Dec 09 2020 at 14:13):@Emilio Jesús Gallego Arias can you provide a pointer to an example?
@Adrian Dapprich you also need to craft at .mlpack file listing all your modules, the full doc is inside the Coq reference manual: https://coq.inria.fr/refman/practical-tools/utilities.html#building-a-coq-project-with-coq-makefile
Emilio Jesús Gallego Arias (Dec 09 2020 at 14:32):@gares sure, let me craft an example for example for Elpi that IIRC had the same problem; but I hope we can address this problem soon by properly allowing Coq to locate plugins with findlib [so things work in OCaml >= 4.08]
Enrico Tassi (Dec 09 2020 at 16:25):For Coq-Elpi you have already a patch: https://github.com/LPCIC/coq-elpi/pull/82/files#diff-89dcf9a56d39ea34f1baeb3a03af39e2753429508913492aaf53e3d1697bdf46R21
but I though you were suggesting one could just add -linkall inside the dune file (since @Adrian Dapprich is already on dune, it would have been the simplest fix)
Last updated: Apr 19 2024 at 15:02 UTC