Emilio Jesús Gallego Arias (Apr 12 2022 at 20:46): 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
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
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.
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
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.
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.
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).
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?
Emilio Jesús Gallego Arias (Apr 12 2022 at 20:51):also coqdep has some modes, so I dunno what is going on
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
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
Enrico Tassi (Apr 13 2022 at 08:21):coqdep -m META_FILE_NAME needs a meta file to translate the public name (e.g. coq-foo.plugin) to the .mlpack namecoqc needs to find coq-foo.META or coq-foo/META in a findlib path, and needs that META file to point to existing cmxs.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.
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
Enrico Tassi (Apr 13 2022 at 08:27):then the _build/default/META should depend on, say, _build/default/src/foo_plugin.cmxs
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
Enrico Tassi (Apr 13 2022 at 08:30):so coqc will wait for the META to exist as well
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.
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.
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.
Rudi Grinberg (May 10 2022 at 15:37):It will take me a bit of time to chew through all that.
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?
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}?
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?
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.
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/METAand this will spit the dependencyx.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?
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"
)
That is inside a plugins package inside the coq-core package
Ali Caglayan (May 10 2022 at 15:51):So you can look up the cmxs from the package name
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.cmxsbut dune currently writes a meta file which replicates the build layout, eglib/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.
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?
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
Ali Caglayan (May 10 2022 at 16:08):Maybe not .mlpack, but .mllib has the same name as ltac_plugin
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.
Ali Caglayan (May 10 2022 at 16:09):I am only guessing from observing the layout of the build.
Ali Caglayan (May 10 2022 at 16:10):For instance, I have
./_build/default/plugins/ltac/ltac_plugin.mllib
It's really the mllib and mlpack files that coqdep is after
Ali Caglayan (May 10 2022 at 16:11):I guess META is a way to guess those
Ali Caglayan (May 10 2022 at 16:12):ocamlfind reports the META file AFAIU
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
Ali Caglayan (May 10 2022 at 16:12):That is my understanding
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
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.
Ali Caglayan (May 10 2022 at 16:54):Here is the PR implementing findlib/META: https://github.com/coq/coq/pull/15220
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.
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:
libraries field of (coq.theory automatically 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
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?
Emilio Jesús Gallego Arias (May 11 2022 at 11:50):I think findlib get the deps from pulgins from META @Ali Caglayan
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
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?
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
Emilio Jesús Gallego Arias (May 11 2022 at 11:53):Dune has something equivalent, the sites plugin
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?
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
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.
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
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
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
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
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
Emilio Jesús Gallego Arias (May 11 2022 at 11:56):without breaking incremental build, let me summarize what happens now
Emilio Jesús Gallego Arias (May 11 2022 at 11:57):As of today what we do to setup the .vo rule is:
-I _build/default/plugins/ltac etc... flags for that_build/default/plugins/ltac/foo.cmxsDynload can see the cmxs too, eveyone is happy Emilio Jesús Gallego Arias (May 11 2022 at 11:58):What it happens with the new setup is this:
Emilio Jesús Gallego Arias (May 11 2022 at 11:59):Fl_dynload and this is the issue! Because now we need to put a lot of stuff in place in the _install directorySo 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?
Emilio Jesús Gallego Arias (May 11 2022 at 11:59):let me check
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
Emilio Jesús Gallego Arias (May 11 2022 at 12:02):So I'm unsure what's the problem then?
Emilio Jesús Gallego Arias (May 11 2022 at 12:03):is Dune just setting OCAMLPATH wrong?
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.
Enrico Tassi (May 11 2022 at 13:34):I mean, Fl_dynload.
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
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?
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
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 ?
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: Oct 13 2024 at 01:02 UTC