Rodolphe Lepigre (Feb 20 2023 at 12:53): 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.
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)
Rodolphe Lepigre (Feb 20 2023 at 13:13):But doesn't dune handle the whole META file bullshit for me?
Gaëtan Gilbert (Feb 20 2023 at 13:17):maybe you need something like Declare ML Module "yojson.plugin".
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
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".
That's why I was trying to use "yojson:yojson": to force through that message.
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.
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.
Paolo Giarrusso (Feb 20 2023 at 13:23):https://github.com/ocaml/dune/issues/5998#issuecomment-1273399569
Paolo Giarrusso (Feb 20 2023 at 13:23):(Emilio confirming the problem, as of last year)
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
Rodolphe Lepigre (Feb 20 2023 at 13:25):Damn, that is really broken. :frown:
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.
Emilio Jesús Gallego Arias (Feb 20 2023 at 14:13):https://github.com/coq/coq/issues/16571
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
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
Emilio Jesús Gallego Arias (Feb 20 2023 at 14:17):@Ali Caglayan isn't this documented in the dune documentation?
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
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
Emilio Jesús Gallego Arias (Feb 20 2023 at 14:18):But yes, otherwise you are correct
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
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
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?
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
Ali Caglayan (Feb 20 2023 at 14:20):Maybe we should focus on that first, I've seen like 4 different people complain
Emilio Jesús Gallego Arias (Feb 20 2023 at 14:20):the workaround has been detailed many times
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
Emilio Jesús Gallego Arias (Feb 20 2023 at 14:20):and we can deprecate the legacy loading method for real
Ali Caglayan (Feb 20 2023 at 14:20):Can you write the workaround in the doc too?
Emilio Jesús Gallego Arias (Feb 20 2023 at 14:21):Yes, it is wirtten in the plugin template
Ali Caglayan (Feb 20 2023 at 14:21):No I mean in the Dune doc
Emilio Jesús Gallego Arias (Feb 20 2023 at 14:22):I mean yes, we can take it from the existing palce
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.
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
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
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
Emilio Jesús Gallego Arias (Feb 20 2023 at 16:12):This is the whole history about "runtime deps"
Emilio Jesús Gallego Arias (Feb 20 2023 at 16:13):for binaries, for example, dune setups a mock .bin dir under _build/$context
Rodolphe Lepigre (Feb 20 2023 at 16:13):That makes sense. However, is it a problem if the paths to the deps are absolute?
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
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
Emilio Jesús Gallego Arias (Feb 20 2023 at 16:14):In principle there is no problem that I can see
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
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
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
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
Rodolphe Lepigre (Feb 20 2023 at 16:16):(Using the setup from https://github.com/coq/coq/issues/16571.)
Emilio Jesús Gallego Arias (Feb 20 2023 at 16:16):@Rodolphe Lepigre let's check the already open bug in dune
Emilio Jesús Gallego Arias (Feb 20 2023 at 16:16):https://github.com/ocaml/dune/issues/5833
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
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
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
Rodolphe Lepigre (Feb 20 2023 at 16:19):OK, but to what directory should the paths be relative to then?
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.
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.
Ali Caglayan (Feb 20 2023 at 16:33):coqdep is called from where the coq.theory is.
Ali Caglayan (Feb 20 2023 at 16:33):In the _build/default dir
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.
Ali Caglayan (Feb 20 2023 at 16:34):Unforatuntely findlib outputs absolute dirs, but it shouldn't be an issue.
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.
Gaëtan Gilbert (Feb 20 2023 at 16:42):you find the common prefix and put enough ../ to get there from the current directory
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.
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.
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?
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.
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
Rodolphe Lepigre (Feb 20 2023 at 17:11):OK, I can try to see if that works.
Emilio Jesús Gallego Arias (Feb 20 2023 at 17:15):Indeed the build layout is hidden now at all for the plugins
Emilio Jesús Gallego Arias (Feb 20 2023 at 17:16):Findlib works exclusively over "install" setup
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.
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
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
.cmxsunder_build/install. That fails with the error I gave above. Turning this into a relative path makes no sense I think.
why not?
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
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
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?
Emilio Jesús Gallego Arias (Feb 20 2023 at 17:18):yup
Emilio Jesús Gallego Arias (Feb 20 2023 at 17:18):basically you call Path.relativize ~pwd file
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!
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
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?
Emilio Jesús Gallego Arias (Feb 20 2023 at 17:20):Actually if you dump rules in Dune, you see many many ../../../../XD
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. :)
Emilio Jesús Gallego Arias (Feb 20 2023 at 17:20):Dune does choke more on absolute paths actually
Rodolphe Lepigre (Feb 20 2023 at 17:21):Yeah, I've seen that. And on symlinks.
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
Rodolphe Lepigre (Feb 20 2023 at 17:21):(Actually, I found a bug with symlinks and dune coq top that I need to report.)
Emilio Jesús Gallego Arias (Feb 20 2023 at 17:21):you destroy users expectations
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_
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
Rodolphe Lepigre (Feb 20 2023 at 17:41):The approach works, I'll make an MR later or tomorrow. :party_ball:
Rodolphe Lepigre (Feb 21 2023 at 09:22):See https://github.com/coq/coq/pull/17270.
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.
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)
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.
Gaëtan Gilbert (Feb 21 2023 at 13:05):can you show your current plugin code?
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: Jun 03 2023 at 15:31 UTC