I’m trying to create a plugin that has dependencies on external OCaml packages. I am aware of the linking issues with this, but using dune I can compile my plugin with relative ease.
The problem occurs when I actually try to use my plugin. If I try to load the master .vo file of my plugin, I encounter ML loadpath errors. Coq cannot find the libraries I am referencing using Declare ML Module. This is not surprising, because during the build dune was managing the load path, but after compilation Coq’s load path is not updated. So I will have to do this myself in my opam package.
What I came up with is to use Opams subst feature, to automatically substitute the path of opams lib directory. I can then update the loadpath in a .v file using Add ML Path "%{lib}%/the-library-dir. Opam will automatically substitute %{lib}% with the correct directory.
However, unfortunately this does not work due to this bug. I’d like to know if other people have solved this problem before, and how.
Until a better solution is available (I understand this will involve findlib), there is actually a workaround: Use the subst solution presented above, but tell people to load the library using Load instead of Require.
This is indeed a bug that I hope to fix for Dune 2.8 , would you mind sharing an example project so I can be sure the fix works?
Actually that is a bit tricky because if the library is in scope, we have the right information to fix this [and I am curious as in this case it should already work], but once the lib is installed that info is lost. So even if not in the .vo, the info has to be stored somewhere.
Note that I’m assuming that you won’t want to use Add ML Path but something like (theories ) and (libraries ) so the dep information is available to the build system.
I’m actually linking with your SerAPI. The actual plugin is currently not really in a compilable state, but here is a proof of concept of what I’m doing: GitHub - LasseBlaauwbroek/serapi-example. This also includes my opam subst trick to set the correct paths. After you install this package using opam, you should be able to load the plugin using Load PrinterLoad.
Note that I’m assuming that you won’t want to use Add ML Path but something like (theories ) and (libraries ) so the dep information is available to the build system.
Yes ideally, I would like Dune to handle all of it. Currently I’m using both (libraries ) and Add ML Path/Declare ML Module.
Actually your current repos works for me, I only get coqdep warnings which are indeed a bug in coqdep related to coqdep requiring a .mlpack file to be present when looking for plugins. See https://github.com/coq/coq/issues/11026
I think we may be misunderstanding each other in some way. Let me respond in some detail to try to clear this up:
Actually your current repos works for me
It works for me too, but only due to the subst hack I am using. This is not a compilation issue, dune build works fine. The problem arises --after installation-- when doing From SerapiTest Require Import Printer. The only way I can make that work is to instead do Load PrinterLoad, which modifies the load path appropriately.
I only get coqdep warnings which are indeed a bug in coqdep related to coqdep requiring a .mlpack file to be present when looking for plugins
Yes, I get those too (unrelated to this issue though). Note that the repo does have a .mlpack file though. Or does it also need to be populated?
But indeed Dune is setting the OCaml-side -I flags correctly if you declare your deps in the (libraries ...) field of the (coq.theory ...) stanza.
Leaving those out actually does not seem to make any difference on my machine…
Oh, I see what you mean now, sorry. Indeed, at installation time there is nothing to keep this information in a good place yet. There are two planned fixes that will help:
loading plugins via findlib
storing Coq package metadata
First should be ready soon, second will take more time, but IMHO the findlib integration should solve this concrete case.