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?

like, should I rather use a _CoqPorject which seems to be used sometimes?

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

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.

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.

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?

yes

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

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

however that doesn't integrate fully seamlessly with `(coq.theory`

yet

@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

@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]

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: Dec 01 2023 at 06:01 UTC