Stream: Dune devs & users

Topic: How does coqc find plugin when called by dune?


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Rodolphe Lepigre (Apr 04 2024 at 14:37):

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.

view this post on Zulip Rodolphe Lepigre (Apr 04 2024 at 14:38):

So adding something like -I _build/install/default/lib typically helps.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Apr 04 2024 at 15:03):

the quoted error says it's using findlib not legacy

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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:

view this post on Zulip 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: May 25 2024 at 21:01 UTC