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.)
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.
Yeah, I expected that, and checked: dune uses
-linkall, but it does not seem to bundle the
.cmxs from the deps.
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)
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)
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.
@Rodolphe Lepigre see the corresponding Coq bug.
-linkall is problematic before Coq 8.15 , as OCaml forbids doubly-linking modules .
So OCaml in fact (after 4.08) won't allow you to load two plugins that use yojson
in 8.16 Coq indeed does use Fl_dynload which can load dependencies
so for 8.15 you can:
Declare Ml Module
You can put the Yojson in its own Coq library, so you can use Require to handle the diamond to an extent
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
OK, I see. Thanks @Emilio Jesús Gallego Arias!
Some people automated this to generate the
Declare Ml Modules using ocamlfind
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:
It doesn't really matter unless you have a diamond dep path on yojson
Ah, so this would also break with Alectryon as usual, and would be fixed again in 8.16 :-)
afaik serapi and alectryon work already on 8.16rc1 (according to my ci)
Last updated: Feb 06 2023 at 00:03 UTC