Stream: Dune devs & users

Topic: Plugin with extra OCaml dependencies


view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 12:53):

I'm playing around (on 8.16.1) with plugins and dependencies on external OCaml libraries, and I find myself once again stuck on how to make this work (this is related to https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Plugin.20depending.20on.20OCaml.20library). Basically, I have a plugin that depends on an installed OCaml library, say yojson, and I get the usual Dynlink error if I just try to Declare ML Module my plugin. So I was trying to manually handle the dependency, but declaring yojson itself as a plugin using one of the following lines.

Declare ML Module "yojson".
Declare ML Module "yojson:yojson".

However, none seem to work, and the declared module is not found.

*** Warning: in file yojson.v, declared ML module yojson has not been found!

Is there a known workaround for that? I could try to include yojson and its deps in my plugin's .cmxs, but that seems too big of a hack, and I'm not even sure how that would work with dune.

view this post on Zulip Gaëtan Gilbert (Feb 20 2023 at 13:00):

you need to use the findlib stuff, see https://coq.github.io/doc/master/refman/practical-tools/utilities.html#coq-makefile
(the "Projects that include plugins (i.e. .ml or .mlg OCaml source files) must have a META file" paragraph)

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 13:13):

But doesn't dune handle the whole META file bullshit for me?

view this post on Zulip Gaëtan Gilbert (Feb 20 2023 at 13:17):

maybe you need something like Declare ML Module "yojson.plugin".

view this post on Zulip Enrico Tassi (Feb 20 2023 at 13:18):

I really don't know if the legacy method is still needed by dune. The fix was scheduled for 2.9.x. Cc @Emilio Jesús Gallego Arias

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 13:21):

The funny thing is that yojson is a valid findlib package name, so I should be able to just do:

Declare ML Module "yojson".

But if I do, I get the error:

*** Error: in file "yojson.v". The name "yojson" is no longer a valid plugin
           name. Plugins should be loaded using their public name according
           to findlib, for example "package-name.foo" and not "foo_plugin".
           If you are using a buid system that does not yet support the new
           loading method (such as Dune) you must specify both the legacy and
           the findlib plugin name as in:
                 Declare ML Module "foo_plugin:package-name.foo".

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 13:21):

That's why I was trying to use "yojson:yojson": to force through that message.

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 13:22):

Gaëtan Gilbert said:

maybe you need something like Declare ML Module "yojson.plugin".

That won't help, that is not an exiting ocamlfind library.

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 13:23):

Enrico Tassi said:

I really don't know if the legacy method is still needed by dune. The fix was scheduled for 2.9.x. Cc Emilio Jesús Gallego Arias

It is still needed as far as I know.

view this post on Zulip Paolo Giarrusso (Feb 20 2023 at 13:23):

https://github.com/ocaml/dune/issues/5998#issuecomment-1273399569

view this post on Zulip Paolo Giarrusso (Feb 20 2023 at 13:23):

(Emilio confirming the problem, as of last year)

view this post on Zulip Gaëtan Gilbert (Feb 20 2023 at 13:25):

Rodolphe Lepigre said:

That's why I was trying to use "yojson:yojson": to force through that message.

The : forces legacy mode IIRC
To use findlib mode you need to have a . in your plugin name

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 13:25):

Damn, that is really broken. :frown:

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 14:09):

Dune has all the support needed to remove the legacy method, however the bug in coqdep means it doesn't work, the bug is open Coq upstream.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 14:13):

https://github.com/coq/coq/issues/16571

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 14:13):

So yup, there were quite a few TODOs with the code merged for findlib support, I don't have the cycles to look at that in the short term but happy to help if someone feels like tackling on that

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 14:17):

IIRC correctly the code in coqdep was easily seen as buggy w.r.t. the way paths are handled

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 14:17):

@Ali Caglayan isn't this documented in the dune documentation?

view this post on Zulip Gaëtan Gilbert (Feb 20 2023 at 14:17):

BTW I got confused but in your case I think yojson is not the plugin so you shouldn't do Declare ML Module with it
you only need to put the yojson dependency in your plugin's META

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 14:18):

@Gaëtan Gilbert if he's trying to use the legacy loading you want to pass the cmxs files of the deps tho

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 14:18):

But yes, otherwise you are correct

view this post on Zulip Ali Caglayan (Feb 20 2023 at 14:18):

It is not in the doc, but it should go here: https://dune.readthedocs.io/en/stable/coq.html#limitations

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 14:19):

There are many other sources of pain remaining in the build system, but I'm afraid it is pointless for people to work on them unless there is some higher-level project-wide coordination

view this post on Zulip Ali Caglayan (Feb 20 2023 at 14:20):

PMP got bit by the transitive deps of Declare ML not working recently when moving plugins around right?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 14:20):

@Ali Caglayan yes let's move the documentation from the issue to the docs

view this post on Zulip Ali Caglayan (Feb 20 2023 at 14:20):

Maybe we should focus on that first, I've seen like 4 different people complain

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 14:20):

the workaround has been detailed many times

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 14:20):

we should focus on fixing the coqdep bug, so then thigs will work out of the box

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 14:20):

and we can deprecate the legacy loading method for real

view this post on Zulip Ali Caglayan (Feb 20 2023 at 14:20):

Can you write the workaround in the doc too?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 14:21):

Yes, it is wirtten in the plugin template

view this post on Zulip Ali Caglayan (Feb 20 2023 at 14:21):

No I mean in the Dune doc

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 14:22):

I mean yes, we can take it from the existing palce

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 16:04):

I've had a look to the code, and I think I understand what is happening, but I'm not quite sure what the right fix is.
See https://github.com/coq/coq/issues/16571#issuecomment-1437244129.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 16:11):

the short summary @Rodolphe Lepigre is that it is Ok to depend on things that are in install

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 16:12):

in fact that has to work for installed theories, so in a sense, the choice that was made for plugins is that we always work with the installed layout

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 16:12):

that could be a concern as you run a bit more rules in the dune side, but IMVHO not a big deal, at least at the scale we are talking about

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 16:12):

This is the whole history about "runtime deps"

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 16:13):

for binaries, for example, dune setups a mock .bin dir under _build/$context

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 16:13):

That makes sense. However, is it a problem if the paths to the deps are absolute?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 16:13):

this is just so you can have private binaries in path, and indeed that is the main limitation in our system

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 16:13):

Rodolphe Lepigre said:

That makes sense. However, is it a problem if the paths to the deps are absolute?

Used to be a bug in Dune about that, not sure

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 16:14):

In principle there is no problem that I can see

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 16:14):

Tho we have some functions in the source code to turn absolute paths into relative if needed

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 16:14):

but usually for example yes, I think that dune registers stuff like ocaml as the full absolute path

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 16:15):

OK, because the path to the META is absolute, and I tried to fix the path to the .cmxs file, but I get something like:

$> dune build theories/Init/Ltac.vo
File "theories/dune", line 2, characters 0-588:
 2 | (coq.theory
 3 |  (name Coq)
 4 |  (package coq-stdlib)
....
28 |
29 |    coq-core.plugins.ssreflect
30 |    coq-core.plugins.derive))
Error: File unavailable:
/home/rodolphe/.../coq/_build/install/default/lib/coq-core/plugins/ltac/ltac_plugin.cmxs

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 16:15):

If we would like to have private plugins, that would require dune work, basically to setup a _build/$context/.lib dir with the right META layout

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 16:16):

(Using the setup from https://github.com/coq/coq/issues/16571.)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 16:16):

@Rodolphe Lepigre let's check the already open bug in dune

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 16:16):

https://github.com/ocaml/dune/issues/5833

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 16:18):

The bug is super confusing, we should clean it up, it is really a bug of the engine when absolute paths and symlinks are there

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 16:18):

@Rodolphe Lepigre we can be very pragmatic here, let's have coqdep turn such absolute paths into relative ones for now

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 16:18):

Dune has already a function to relativize paths vs a base directory, not sure if Coq has one

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 16:19):

OK, but to what directory should the paths be relative to then?

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 16:22):

It should be from the root of the coq.theory I guess? Which coqdep has no knowledge about if I understand correctly.

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 16:23):

Or maybe they should be relative to the CWD since coqdep is probably called from the right place by dune.

view this post on Zulip Ali Caglayan (Feb 20 2023 at 16:33):

coqdep is called from where the coq.theory is.

view this post on Zulip Ali Caglayan (Feb 20 2023 at 16:33):

In the _build/default dir

view this post on Zulip Ali Caglayan (Feb 20 2023 at 16:33):

If coqdep asks for things in the install dir, it will be reletivised to the correct place.

view this post on Zulip Ali Caglayan (Feb 20 2023 at 16:34):

Unforatuntely findlib outputs absolute dirs, but it shouldn't be an issue.

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 16:35):

Well, it is an issue because the CWD is under _build/default and the only reference we have (the META file) is under _build/install.
So I don't know how to fix this without using a dirty hack.

view this post on Zulip Gaëtan Gilbert (Feb 20 2023 at 16:42):

you find the common prefix and put enough ../ to get there from the current directory

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 16:46):

That's not good enough: the directory structure under _build/install is by section, whereas the directory structure under _build/default imitates the source tree. In the case of the Coq source tree I think you would get something that works, but we can't assume that the layout follows that discipline everywhere.

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 16:48):

Actually, even for the Coq source-tree that would not work, depending on how the different opam packages are organized.

view this post on Zulip Gaëtan Gilbert (Feb 20 2023 at 16:50):

I thought the question was how to turn /bla/bla/_build/install/bli/bli into ../install/bli/bli when the current directory is /bla/bla/_build/default? Why does it matter that the install and build layouts are different?

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 16:51):

There is more to it: we also need to fix the path to the .cmxs, and we want a path relative to _build/default.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 17:06):

Rodolphe Lepigre said:

There is more to it: we also need to fix the path to the .cmxs, and we want a path relative to _build/default.

The path of the cmxs has to be the one in _build/install

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 17:11):

OK, I can try to see if that works.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 17:15):

Indeed the build layout is hidden now at all for the plugins

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 17:16):

Findlib works exclusively over "install" setup

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 17:16):

Actually, no, sorry: that's the thing I already tried, by giving the absolute path to the .cmxs under _build/install. That fails with the error I gave above. Turning this into a relative path makes no sense I think.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 17:16):

so for Declare ML Module "foo" the deps have to be the plugin in the install path

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 17:16):

Rodolphe Lepigre said:

Actually, no, sorry: that's the thing I already tried, by giving the absolute path to the .cmxs under _build/install. That fails with the error I gave above. Turning this into a relative path makes no sense I think.

why not?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 17:17):

it is fine to call coqdep in _build/$context and emit a dep ../install/$context/lib/foo/bar.cmxs

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 17:17):

In fact we already do that for the meta file, and basically in Dune for install files

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 17:17):

So, you mean, if coqdep is run in _build/default/some/path/to/theory/ then I give the path ../../../../../install/lib/something/file.cmxs?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 17:18):

yup

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 17:18):

basically you call Path.relativize ~pwd file

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 17:18):

OK I thought that would be terrible (that's what I called a big hack earlier), but I can try. Thanks for clarifying what you meant!

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 17:19):

as to workaround the bug, this is done in many places in real world for example to have reproducible logs

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 17:19):

Maybe it is terrible, it seems fine to me, but I could be well missing something. What problem do you see?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 17:20):

Actually if you dump rules in Dune, you see many many ../../../../XD

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 17:20):

I dunno, the paths are hard to read, they do not seem canonical, and I fear dune will choke on them. But we'll see. :)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 17:20):

Dune does choke more on absolute paths actually

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 17:21):

Yeah, I've seen that. And on symlinks.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 17:21):

Actually the moment you gotta canonize paths you are in trouble in my experience

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 17:21):

(Actually, I found a bug with symlinks and dune coq top that I need to report.)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 17:21):

you destroy users expectations

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 17:22):

One of the nice things I learned about dune is that relative is good, _if you have the right path machinery to handle them_

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 17:23):

which means relative paths always come with the dir context associated to they can safely adapted on change of cwd

view this post on Zulip Rodolphe Lepigre (Feb 20 2023 at 17:41):

The approach works, I'll make an MR later or tomorrow. :party_ball:

view this post on Zulip Rodolphe Lepigre (Feb 21 2023 at 09:22):

See https://github.com/coq/coq/pull/17270.

view this post on Zulip Rodolphe Lepigre (Feb 21 2023 at 11:59):

I made some progress on supporting external OCaml dependencies, but there are some choices to make. The problem is that dune is only happy with relative paths if they are in the workspace. So, for instance, if I try to specify an external library (whose META and .cmxs is under the opam switch's library directory) then dune complains that the file is not in the workspace.

To solve this, I tried extending the syntax of Declare ML Module to accept something like Declare ML Module "external yojson", whose only effect is to give absolute paths instead of relative ones. But with that change, things seem to work as expected. I'm not sure this is what we want though.

view this post on Zulip Gaëtan Gilbert (Feb 21 2023 at 12:32):

this is wrong
if using findlib you should not Declare ML Module for yojson, it should be implicit from your plugin's dependencies
if not using findlib then you should just need to have the cmxs in the paths searched by Coq (ie -I)

view this post on Zulip Rodolphe Lepigre (Feb 21 2023 at 12:57):

Indeed, that's what I would expect as well. But I'm not quite sure how to get there.

view this post on Zulip Gaëtan Gilbert (Feb 21 2023 at 13:05):

can you show your current plugin code?

view this post on Zulip Rodolphe Lepigre (Feb 22 2023 at 02:04):

Gaëtan Gilbert said:

can you show your current plugin code?

While trying to minimize my code, I realized that I can actually use findlib in the intended way, and that things seem to work as I expect them to. We were using the legacy syntax because the findlib one used to be broken with dune, and I did not realize that this was fixed...


Last updated: Apr 14 2024 at 09:39 UTC