Li-yao (Apr 03 2024 at 21:33): Li-yao (Apr 03 2024 at 21:33):In _build/log I see coqc given options like
coqc -I plugin -Q src QuickChick src/QuickChick.v
yet when I run that command by hand I get
File "./src/QuickChick.v", line 4, characters 0-42:
Error:
Findlib error: coq-quickchick.plugin not found in:
plugin/
... (omitted a 100 more paths)
What part of the config am I missing?
And for context, I am trying to make a _CoqProject so that I can edit coq files in my repository after running dune build
so I got:
-I _build/default/plugin
-Q src QuickChick
but then I get the above error.
Ali Caglayan (Apr 04 2024 at 13:56):Depends where you are running that command from. If it is from _build/default then it would probably work the same as long as the plugin has been built
Li-yao (Apr 04 2024 at 14:02):I tried running that command inside _build/default/, still that error.
$ ls -R
dune-project plugin theories
./plugin:
dune foo.mlg myplugin.mlpack
./theories:
dune Q.v
$ dune build
$ cd _build/default/
$ rm -f theories/Q.glob
$ coqc -I plugin -Q theories Foo theories/Q.v # fails with Findlib error
The plugins are looked for using findlib, and dune runs in an environment with an extended OCAMLPATH which includes something like _build/install/default/lib I believe.
Rodolphe Lepigre (Apr 04 2024 at 14:38):So adding something like -I _build/install/default/lib typically helps.
Emilio Jesús Gallego Arias (Apr 04 2024 at 15:00):Also note that Dune will ensure the META file for the plugin is in place before calling coqdep, then the dep is directly to the .cmxs file.
Emilio Jesús Gallego Arias (Apr 04 2024 at 15:02):@Li-yao , to answer concretely your question, coqc will call findlib to try to locate your plugin, or if you used the legacy method, it will look for the .cmxs file iterating on the directories given by -I
Gaëtan Gilbert (Apr 04 2024 at 15:03):the quoted error says it's using findlib not legacy
Li-yao (Apr 04 2024 at 15:36):Yes, in my attempt -I plugin is the path to the plugin, and it still doesn't find it.
Rodolphe Lepigre (Apr 04 2024 at 19:14):The only workaround that I found to get dune to work with plugins loaded with findlib method is to generate some empty dummy.v in the theory using the plugin, with a dependency on the opam package providing the plugin. It works fine for us, but means that plugins need to go into separate packages.
The kind of rule I use is typically of the form:
(include_subdirs qualified)
(coq.theory
(name my.theory)
(package my_theories)
...)
(rule
(targets dummy.v)
(deps (package my_plugin))
(action (with-stdout-to %{targets} (echo "(* Generated file *)"))))
Somehow, depending on the package defining the plugin, instead of just the plugin, enforces that files are in place under _build/default/install/lib, which is what is expect for findlib to locate the plugins.
Li-yao (Apr 04 2024 at 19:21):Oh I misread _build/install/default/lib. Adding that path to coqc indeed works! Now to figure out what's different about that directory. (That seems to be the META file.)
Emilio Jesús Gallego Arias (Apr 04 2024 at 19:53):@Rodolphe Lepigre it should not be necessary to do these hoops anymore, please open a bug if you can.
Li-yao (Apr 04 2024 at 19:59):how does Coq know whether to use the findlib method or the old one to find a plugin? It just tries both?
Rodolphe Lepigre (Apr 04 2024 at 21:02):@Emilio Jesús Gallego Arias I agree it should not be necessary, but it is. :sweat_smile:
Rodolphe Lepigre (Apr 04 2024 at 21:06):@Li-yao the loading method is selected in the string passed to Declare ML Module, depending on whether you just give a findlib path, or a path and something else separated with : (if I remember correctly). The findlib method is the way to go if you have complex OCaml deps, and the legacy method is deprecated (thought it has not been removed yet as far as I know).
Last updated: Oct 13 2024 at 01:02 UTC