Rodolphe Lepigre (Jun 21 2022 at 12:07): 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.)
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.
Enrico Tassi (Jun 21 2022 at 12:54): 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.
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)
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)
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.
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 .
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
Emilio Jesús Gallego Arias (Jun 21 2022 at 13:31):in 8.16 Coq indeed does use Fl_dynload which can load dependencies
Emilio Jesús Gallego Arias (Jun 21 2022 at 13:32):so for 8.15 you can:
Declare Ml Module 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
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
Rodolphe Lepigre (Jun 21 2022 at 13:34):OK, I see. Thanks @Emilio Jesús Gallego Arias!
Emilio Jesús Gallego Arias (Jun 21 2022 at 13:41):Some people automated this to generate the Declare Ml Modules using ocamlfind
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:
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
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 :-)
Enrico Tassi (Jun 22 2022 at 06:02):afaik serapi and alectryon work already on 8.16rc1 (according to my ci)
Last updated: May 31 2023 at 16:01 UTC