Stream: Coq devs & plugin devs

Topic: Plugin depending on OCaml library


view this post on Zulip Rodolphe Lepigre (Jun 21 2022 at 12:07):

Hi there! I'm having some trouble finding how to compile a plugin that depends on some external OCaml library (in my case yojson). Are there examples of plugins somewhere that do something like that? In my case, I'm building the plugin and Coq code with dune, and I end up with a Dynlink error saying that some symbol in yojson is not defined. How would you typically let Coq know that it needs to also load yojson.cmxs and from where? (I'm working on 8.15.2.)

view this post on Zulip Enrico Tassi (Jun 21 2022 at 12:54):

Hum, I use that in elpi, but I use coq_makefile. Before 8.16 you need -linkall, unfortunately. I don't know what dune does.

view this post on Zulip Enrico Tassi (Jun 21 2022 at 12:54):

https://github.com/LPCIC/coq-elpi/blob/2a511a7edb9ebecad52f094111abd9c0c4187f7c/Makefile.coq.local#L1

view this post on Zulip Rodolphe Lepigre (Jun 21 2022 at 12:55):

Yeah, I expected that, and checked: dune uses -linkall, but it does not seem to bundle the .cmxs from the deps.

view this post on Zulip Enrico Tassi (Jun 21 2022 at 12:55):

Starting from 8.16 plugins are loaded via findlib, so no need to -linkall since that loading machinery is recursive (it loads the deps written in the META file)

view this post on Zulip Enrico Tassi (Jun 21 2022 at 12:56):

There is a PR on coq-elpi adding dune support. I don't know if it works, but it may give you hints. (I'm not even considering dune before 8.16 is out)

view this post on Zulip Rodolphe Lepigre (Jun 21 2022 at 12:56):

Thanks for the link, I'll try a coq_makefile version to make sure there is not another problem, I would have expected dune to work here.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2022 at 13:30):

@Rodolphe Lepigre see the corresponding Coq bug. -linkall is problematic before Coq 8.15 , as OCaml forbids doubly-linking modules .

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2022 at 13:30):

So OCaml in fact (after 4.08) won't allow you to load two plugins that use yojson

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2022 at 13:31):

in 8.16 Coq indeed does use Fl_dynload which can load dependencies

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2022 at 13:32):

so for 8.15 you can:

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2022 at 13:33):

You can put the Yojson in its own Coq library, so you can use Require to handle the diamond to an extent

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2022 at 13:34):

Last bit in 8.15 and below, is that you need to pass -I yojson_path to coqc, of course. This should be done using ocamlfind

view this post on Zulip Rodolphe Lepigre (Jun 21 2022 at 13:34):

OK, I see. Thanks @Emilio Jesús Gallego Arias!

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2022 at 13:41):

Some people automated this to generate the Declare Ml Modules using ocamlfind

view this post on Zulip Rodolphe Lepigre (Jun 21 2022 at 13:47):

I actually considered adding a dummy Coq module, but I thought it was a bit too crazy. But I guess I'll end up doing that. :laughter_tears:

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2022 at 14:12):

It doesn't really matter unless you have a diamond dep path on yojson

view this post on Zulip Paolo Giarrusso (Jun 22 2022 at 03:25):

Ah, so this would also break with Alectryon as usual, and would be fixed again in 8.16 :-)

view this post on Zulip Enrico Tassi (Jun 22 2022 at 06:02):

afaik serapi and alectryon work already on 8.16rc1 (according to my ci)


Last updated: Dec 07 2023 at 17:01 UTC