Stream: Dune devs & users

Topic: Dune and plugins in 8.16


view this post on Zulip Emilio Jesús Gallego Arias (Apr 12 2022 at 20:46):

Hi folks, I'm creating this topic to keep track of the needed changes for Dune to support Coq new findlib-based plugin loader.

We had some discussion and even a small patch to support that, but I lost track of that, IMHO it would be good if we could open an issue in the dune repos describing the problem, and adding a test case. Having the test case would be super useful as the fix is likely just a one-line change to add a dep in rules.

cc @Enrico Tassi @Ali Caglayan

view this post on Zulip Ali Caglayan (Apr 12 2022 at 20:47):

Are you talking about: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/.E2.9C.94.20Plugins.20with.20shared.20code

view this post on Zulip Emilio Jesús Gallego Arias (Apr 12 2022 at 20:47):

Dune already knows the libraries a (coq.theory ...) depends upon, so all that we need is to add the right dependency to the META file, however, we had an issue in the sense that the generated META file in build was incorrect. It is not clear we can easily depend on things in the install layout, we should, but it is better if we cold live with a dep to the build layout. Worst case we may have to generate a different META file for us / tweak something in the layout.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 12 2022 at 20:48):

Ali Caglayan said:

Are you talking about: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/.E2.9C.94.20Plugins.20with.20shared.20code

Not exactly, I'm talking about Dune not adding the dependency to the META file properly for 8.16

view this post on Zulip Emilio Jesús Gallego Arias (Apr 12 2022 at 20:49):

As of now, when plugins are required for a Coq theory, Dune relies on coqdep to track the .cmxs file, but the (libraries ...) field in coq-theory is used to pass the right -I flags to Coq.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 12 2022 at 20:50):

With the new setup, I'm not exactly sure what needs to be in place when the Declare ML Module is called so findlib is happy.

view this post on Zulip Ali Caglayan (Apr 12 2022 at 20:50):

IIANM coqdep reports the location of the META file when you have a Declare ML Module but I believe findlib gives an absolute path (idk if this is a problem in general for dune).

view this post on Zulip Emilio Jesús Gallego Arias (Apr 12 2022 at 20:51):

It should not be, however I'm not sure we want this to happen?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 12 2022 at 20:51):

also coqdep has some modes, so I dunno what is going on

view this post on Zulip Emilio Jesús Gallego Arias (Apr 12 2022 at 20:52):

coqdep has some modes where it outputs the file, some where it doesn't

view this post on Zulip Emilio Jesús Gallego Arias (Apr 12 2022 at 20:52):

the code was a bit strange, so I lost track, I think Enrico knows better what is missing

view this post on Zulip Enrico Tassi (Apr 13 2022 at 08:21):

The META file generated by dune is OK and is in scope (since dune exports OCAMLPATH) but points to the installed cmxs, and IIRC dune rules cannot make a build target depend on an installed target (I don't recall the source of this info, so I may be wrong). This kind of dep is usually expressed, if I'm not mistaken, as a dependency on a package, rather than a file, but this does not work if the package contains both the plugin and some files which needs it. This is what sites does, IIRC.

There is now a -I flag to tell coqc where to look for META files.

I don't know what the easiest path would be. IMO putting in scope a META file pointing to non-existing files is a bug in dune.
IMO the meta file should become in-scope only when installed, and its installation should depend on the installation of the files in points to.
Then since we call coqdep -m META, we would delay calling any coq tool until the library is in place, since that rule depends on the META file which is installed only once things are set.

view this post on Zulip Enrico Tassi (Apr 13 2022 at 08:26):

so, to me, exprting OCAMLPATH=_build/default/ is the first problem, it should point to _build/install/default/lib

view this post on Zulip Enrico Tassi (Apr 13 2022 at 08:27):

then the _build/default/META should depend on, say, _build/default/src/foo_plugin.cmxs

view this post on Zulip Enrico Tassi (Apr 13 2022 at 08:29):

and the rule for getting a .d out of a .v should get the extra dependency -m _build/default/META and this will spit the dependency x.vo : x.v _build/default/META

view this post on Zulip Enrico Tassi (Apr 13 2022 at 08:30):

so coqc will wait for the META to exist as well

view this post on Zulip Enrico Tassi (Apr 13 2022 at 08:30):

once eveything is installed, for other packages needing coq-foo, then the META found would we be the installed one.

view this post on Zulip Enrico Tassi (Apr 13 2022 at 08:33):

there is only one little caveat I can see, that is that the installed META file and the one in build tree are usually different, but dune does not follow the standard (fndlib doc). In particular the installed layout should be lib/foo/META lib/foo/plugin.cmxs but dune currently writes a meta file which replicates the build layout, eg lib/foo/src/plugin.cmxs.

This problem is also present in coq_makefile, which solved it by stripping directory = "./src" like directives from the META when installing it. In dune installation is usually a symlink. I don't know if this can be changed.

view this post on Zulip Enrico Tassi (Apr 13 2022 at 08:34):

Note that findlib doc says that the installed layout of libs should be flat, and I believe dune does not follow the advice.

view this post on Zulip Rudi Grinberg (May 10 2022 at 15:37):

It will take me a bit of time to chew through all that.

view this post on Zulip Rudi Grinberg (May 10 2022 at 15:37):

coqdep -m META_FILE_NAME needs a meta file to translate the public name (e.g. coq-foo.plugin) to the .mlpack name
How does this mapping work? Is it specified somewhere in the META?

view this post on Zulip Rudi Grinberg (May 10 2022 at 15:40):

The META file generated by dune is OK and is in scope (since dune exports OCAMLPATH) but points to the installed cmxs, and IIRC dune rules cannot make a build target depend on an installed target (I don't recall the source of this info, so I may be wrong). This kind of dep is usually expressed, if I'm not mistaken, as a dependency on a package, rather than a file, but this does not work if the package contains both the plugin and some files which needs it. This is what sites does, IIRC.

Don't we have %{libexec:lib:lib.cmxs}?

view this post on Zulip Rudi Grinberg (May 10 2022 at 15:41):

I don't know what the easiest path would be. IMO putting in scope a META file pointing to non-existing files is a bug in dune.

That definitely seems wrong to me as well. Is there a bug report/test case for this?

view this post on Zulip Rudi Grinberg (May 10 2022 at 15:42):

Enrico Tassi said:

so, to me, exprting OCAMLPATH=_build/default/ is the first problem, it should point to _build/install/default/lib

Who is exporting _build/default/? As far as I can know, dune only exports the install directory as you've pointed out.

view this post on Zulip Rudi Grinberg (May 10 2022 at 15:46):

Enrico Tassi said:

and the rule for getting a .d out of a .v should get the extra dependency -m _build/default/META and this will spit the dependency x.vo : x.v _build/default/META

To clarify: to depend on a plugin we need to depend on the META that defines it and all the of the files in that META. Isn't that an over-approximation? a META might contain more than one plugin or other OCaml libraries. What about private plugins?

view this post on Zulip Ali Caglayan (May 10 2022 at 15:50):

Rudi Grinberg said:

coqdep -m META_FILE_NAME needs a meta file to translate the public name (e.g. coq-foo.plugin) to the .mlpack name

How does this mapping work? Is it specified somewhere in the META?

Here is what the part in the META file for core-core.plugins.ltac looks like:

  package "ltac" (
    directory = "ltac"
    version = "dev"
    description = "Coq's LTAC tactic language"
    requires = "coq-core.stm"
    archive(byte) = "ltac_plugin.cma"
    archive(native) = "ltac_plugin.cmxa"
    plugin(byte) = "ltac_plugin.cma"
    plugin(native) = "ltac_plugin.cmxs"
  )

view this post on Zulip Ali Caglayan (May 10 2022 at 15:51):

That is inside a plugins package inside the coq-core package

view this post on Zulip Ali Caglayan (May 10 2022 at 15:51):

So you can look up the cmxs from the package name

view this post on Zulip Rudi Grinberg (May 10 2022 at 15:53):

Enrico Tassi said:

there is only one little caveat I can see, that is that the installed META file and the one in build tree are usually different, but dune does not follow the standard (fndlib doc). In particular the installed layout should be lib/foo/META lib/foo/plugin.cmxs but dune currently writes a meta file which replicates the build layout, eg lib/foo/src/plugin.cmxs.

Dune does not do that as far as I can see. Dune install the META into $switch/lib/$lib/META and the cmxs into $switch/lib/$lib/$main_module.cmxs I don't see any src directories.

view this post on Zulip Rudi Grinberg (May 10 2022 at 15:54):

Enrico Tassi said:

Note that findlib doc says that the installed layout of libs should be flat, and I believe dune does not follow the advice.

Should it be flat even for sub libraries? Where do you expect the META for foo.bar to exist for example?

view this post on Zulip Rudi Grinberg (May 10 2022 at 15:55):

Ali Caglayan said:

Rudi Grinberg said:

coqdep -m META_FILE_NAME needs a meta file to translate the public name (e.g. coq-foo.plugin) to the .mlpack name

How does this mapping work? Is it specified somewhere in the META?

Here is what the part in the META file for core-core.plugins.ltac looks like:

  package "ltac" (
    directory = "ltac"
    version = "dev"
    description = "Coq's LTAC tactic language"
    requires = "coq-core.stm"
    archive(byte) = "ltac_plugin.cma"
    archive(native) = "ltac_plugin.cmxa"
    plugin(byte) = "ltac_plugin.cma"
    plugin(native) = "ltac_plugin.cmxs"
  )

I don't see any .mlpack here though

view this post on Zulip Ali Caglayan (May 10 2022 at 16:08):

Maybe not .mlpack, but .mllib has the same name as ltac_plugin

view this post on Zulip Ali Caglayan (May 10 2022 at 16:09):

So if you want the .mllib file associated to coq-core.plugins.ltac, then you can find it by finding ltac_plugin.cma in some directory, and you would expect .mllib to be there too.

view this post on Zulip Ali Caglayan (May 10 2022 at 16:09):

I am only guessing from observing the layout of the build.

view this post on Zulip Ali Caglayan (May 10 2022 at 16:10):

For instance, I have

./_build/default/plugins/ltac/ltac_plugin.mllib

view this post on Zulip Ali Caglayan (May 10 2022 at 16:11):

It's really the mllib and mlpack files that coqdep is after

view this post on Zulip Ali Caglayan (May 10 2022 at 16:11):

I guess META is a way to guess those

view this post on Zulip Ali Caglayan (May 10 2022 at 16:12):

ocamlfind reports the META file AFAIU

view this post on Zulip Ali Caglayan (May 10 2022 at 16:12):

So in order to find plugins, you pass the lib name to ocamlfind, it gives you the META with the probably name of mllib

view this post on Zulip Ali Caglayan (May 10 2022 at 16:12):

That is my understanding

view this post on Zulip Rudi Grinberg (May 10 2022 at 16:19):

Btw, we have a sites extension that's designed for things like these mlpack files: https://dune.readthedocs.io/en/stable/sites.html

view this post on Zulip Rudi Grinberg (May 10 2022 at 16:22):

Actually, it's not exactly the same and I'm not sure you can make use of it.

view this post on Zulip Ali Caglayan (May 10 2022 at 16:54):

Here is the PR implementing findlib/META: https://github.com/coq/coq/pull/15220

view this post on Zulip Enrico Tassi (May 10 2022 at 20:36):

Yes, we had a call with F. Bobot and the conclusion was that sites would not just work for us, it should be summarized in the PR header.

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 11:09):

Let me see if I understand things correctly and we can make progress on this:

So it is this last point I don't know how to make it work. And indeed, it is not possible to implement it properly in the sense that if you have a private plugin for example, what happens? Even assuming all the plugins are gonna be public (which is not a best practice)

Even so, I think that Dune's current setup for the build doesn't allow us to fully setup a working findlib env in _build/$context

So @Enrico Tassi @Rudi Grinberg , what do you think?

It seems to me that maybe the best solution is a kind of 3rd-way one, in which dune does the translation of findlib to .cmxs files, including transitive deps (this is already done) , however we will need the META to have the dependency information ready. I dunno.

I'm on holidays now, but we could do a small example (without Coq) where a private dune binary just uses findlib to dynload some deps, this would make us understand better how to best setup a working findlib in the build layout

view this post on Zulip Ali Caglayan (May 11 2022 at 11:18):

I still don't understand why we need META at all tho. If findlib can work out enough to make a META file, then surely we can get that info directly too?

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 11:50):

I think findlib get the deps from pulgins from META @Ali Caglayan

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 11:50):

what do you mean "to make a meta file" , META files are really information built by hand, in Dune they are derived from the (libraries) field

view this post on Zulip Ali Caglayan (May 11 2022 at 11:51):

Right so if dune is making META files then why do we need to read them again?

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 11:52):

because we are not using Dune's site plugin code, but findlib which is independent

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 11:53):

Dune has something equivalent, the sites plugin

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 11:54):

the thing is that findlib doesn't seem flexible enought for what we wanna do, but maybe patching findlib could be the quickest way?

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 11:54):

people would love to have something like we are tying to do in Coq working

view this post on Zulip Ali Caglayan (May 11 2022 at 11:54):

OK so coqdep sees a Declare ML Module foo.plugin, uses findlib to resolve this to an actual plugin name.

view this post on Zulip Ali Caglayan (May 11 2022 at 11:54):

coq.theory also calls coqdep which ends up breaking things because the META doesn't exist yet

view this post on Zulip Ali Caglayan (May 11 2022 at 11:55):

but if dune already knows how to turn a plugin name into a library whatever, then can't we patch coqdep and dune to handle this case

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 11:55):

@Ali Caglayan coqdep is not the problem, it is what coqc does when it finds that

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 11:55):

@Ali Caglayan exactly, this is what we do now, what I don't know how to do is to get things OK for Fl_dynload to work

view this post on Zulip Enrico Tassi (May 11 2022 at 11:56):

yes, but the meta is there. it points to non existing files, but coqdep does not care

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 11:56):

without breaking incremental build, let me summarize what happens now

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 11:57):

As of today what we do to setup the .vo rule is:

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 11:58):

What it happens with the new setup is this:

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 11:59):

So indeed the META file in build is pointing out to things that don't exists, but I'm unsure they can be filled up by dune?

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 11:59):

let me check

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 12:01):

well so actually the _build/default/META.coq-core does point out to the right locations

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 12:02):

So I'm unsure what's the problem then?

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 12:03):

is Dune just setting OCAMLPATH wrong?

view this post on Zulip Enrico Tassi (May 11 2022 at 13:34):

First, the META.coq-core is generated before the .cmxs are in place. So coqc does not find them.

view this post on Zulip Enrico Tassi (May 11 2022 at 13:34):

I mean, Fl_dynload.

view this post on Zulip Enrico Tassi (May 11 2022 at 13:37):

dune builds the cmxs before running coqc I guess (if coqdep is called right, the deps are there), but then coqc does not find them

view this post on Zulip Enrico Tassi (May 11 2022 at 13:39):

well so actually the _build/default/META.coq-core does point out to the right locations

which locations?

view this post on Zulip Enrico Tassi (May 11 2022 at 13:40):

note that the META file in _build/install and _build/default are the same (a symlink) but the file layout is different IIRC

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 14:18):

Mmm, the layout should work tho, if findlib uses the file in _build/default , so I guess what dune should do is just to pass -I build/default/ to coqc ?

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 14:19):

I can test this with the coq_dune branch, but indeed, the rest should work as coqdep will make sure for example _build/default/plugins/ltac/ltac_plugin.cmxs is built. So we only need to tell findlib to use that one


Last updated: Feb 04 2023 at 02:03 UTC