Enrico Tassi (Nov 18 2021 at 14:15): Enrico Tassi (Nov 18 2021 at 14:15):I'm working on using findlib to load plugins and I have this problem:
dune build coq-core.install && dune build coq-stdlib.install # OK
dune build coq-core.install coq-stdlib.install # FAIL
dune build coq-core.install coq-stdlib.install; dune build coq-core.install coq-stdlib.install # OK
The problem is that in spite of coq-stdlib having a coq.theory stanza with (libraries coq-core.plugins.foo), dune does not wait for the META files of these libraries to be installed before compiling the Coq theory, and hence plugins cannot be loaded.
@Rudi Grinberg is there a way to make a target depend on the META file being installed?
@Emilio Jesús Gallego Arias mentioned this problem here and there, but I've never understood if there is a known workaround for it.
Rudi Grinberg (Nov 18 2021 at 15:03):Why does it need the META to be installed if the plugin is in the same workspace?
Rudi Grinberg (Nov 18 2021 at 15:05):But to answer your question, you have two options:
(deps (package coq-core))%{lib:coq-core:META}.The issue with 2. is that this only adds a dependency on just the META, which means that the files listed in the META might not be built. In any case, I'm not sure either of these will be useful to you, because the coq rule in question might be defined by dune so you can't really add a dependency to it.
Enrico Tassi (Nov 18 2021 at 15:51):Hum, not that I re-run the test I see my analysis was wrong. The META file is probably there, but not the (symlink) installed file it talks about.
I get cannot find file /home/gares/COQ/dynlink-w-findlib/_build/install/default/lib/coq-core/plugins/ltac/ltac_plugin.cmxs in search path from findlib, but when dune stops, the file is actually there.
This is what I see:
...
ocamlc doc/plugin_tutorial/tuto2/src/.tuto2_plugin.objs/byte/tuto2_plugin__Persistent_counter.{cmo,cmt}
ocamlc doc/plugin_tutorial/tuto2/src/.tuto2_plugin.objs/byte/tuto2_plugin__G_tuto2.{cmi,cmo,cmt}
coqc theories/Init/.Notations.aux,theories/Init/Notations.{glob,vo}
File "./theories/Init/Ltac.v", line 11, characters 0-42:
Error:
Dynlink error: cannot find file /home/gares/COQ/dynlink-w-findlib/_build/install/default/lib/coq-core/plugins/ltac/ltac_plugin.cmxs in search path
ocamlopt doc/plugin_tutorial/tuto2/src/.tuto2_plugin.objs/native/tuto2_plugin__Persistent_counter.{cmx,o}
ocamlc plugins/ssrmatching/.ssrmatching_plugin.objs/byte/ssrmatching_plugin__Ssrmatching.{cmo,cmt}
ocamlc doc/plugin_tutorial/tuto3/src/.tuto3_plugin.objs/byte/tuto3_plugin__Tuto_tactic.{cmo,cmt}
ocamlc doc/plugin_tutorial/tuto3/src/.tuto3_plugin.objs/byte/tuto3_plugin__Construction_game.{cmo,cmt}
ocamlc doc/plugin_tutorial/tuto3/src/.tuto3_plugin.objs/byte/tuto3_plugin__G_tuto3.{cmi,cmo,cmt}
ocamlopt doc/plugin_tutorial/tuto3/src/.tuto3_plugin.objs/native/tuto3_plugin__Tuto_tactic.{cmx,o}
ocamlopt doc/plugin_tutorial/tuto3/src/.tuto3_plugin.objs/native/tuto3_plugin__Construction_game.{cmx,o}
ocamlc plugins/micromega/.zify_plugin.objs/byte/zify_plugin__G_zify.{cmi,cmo,cmt}
ocamlc plugins/micromega/.zify_plugin.objs/byte/zify_plugin__Zify.{cmo,cmt}
ocamlc dev/.top_printers.objs/byte/top_printers.{cmo,cmt}
ocamlopt plugins/ssrmatching/.ssrmatching_plugin.objs/native/ssrmatching_plugin__Ssrmatching.{cmx,o}
ocamlopt dev/.top_printers.objs/native/top_printers.{cmx,o}
ocamlc plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__G_micromega.{cmo,cmt}
ocamlopt plugins/micromega/.micromega_plugin.objs/native/micromega_plugin__Itv.{cmx,o}
ocamlopt plugins/micromega/.micromega_plugin.objs/native/micromega_plugin__G_micromega.{cmx,o}
ocamlc plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Itv.{cmo,cmt}
ocamlc plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Sos_types.{cmo,cmt}
ocamlc plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Sos.{cmi,cmti}
ocamlc plugins/micromega/.micromega_plugin.objs/byte/micromega_plugin__Certificate.{cmi,cmti}
ocamlopt plugins/micromega/.micromega_plugin.objs/native/micromega_plugin__Sos_types.{cmx,o}
ocamlopt plugins/ltac/ltac_plugin.{a,cmxa}
...
So this seems a bug in the rules given by coq.theory. I mean, coq-core.plugins.ltac is the library made of the target built in the very last line, but the coqc line failing up in the log depends on that library (it is part of the coq.theory which lists coq-core.plugins.ltac as a library).
Sorry for the wrong diagnostic.
Gaëtan Gilbert (Nov 18 2021 at 15:55):coqdep still needs to say /bla/Ltac.vo: /bli/ltac_plugin.cmxs since that's how dune gets the dependency
Emilio Jesús Gallego Arias (Nov 18 2021 at 16:21):It may be worth trying to use the site's plugin feature directly, indeed access to plugins from the build context is the main reason François deprecated the findlib support in favor of the latter
Enrico Tassi (Nov 18 2021 at 18:03):thanks Gaëtan, I think you found the bug
Enrico Tassi (Nov 19 2021 at 15:07):Thanks to the hint of Gaetan I could compile Coq, but things are still shaky, and now I can see the bug about META.
If I do
dune build theories/Init/Ltac.vo
...
ocamlopt plugins/ltac/ltac_plugin.cmxs
File "./theories/Init/Ltac.v", line 11, characters 0-42:
Error:
Dynlink error: coq-core.plugins.ltac not found in:
/home/gares/COQ/dynlink-w-findlib/_build/install/default/lib
/home/gares/.opam/4.09.1/lib
and indeed find . -name META finds nothing. So I think I should make the coq.theory stanza generate a rule which depends on foo/META if it depends on a library foo.*. @Emilio Jesús Gallego Arias can you point me to the code I should change in the sources of dune?
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:12):I am not sure @Enrico Tassi that will be enough, maybe François Bobot could comment more [but he's not in this zulip], the way findlib works requires a full setup of the findlib database which is quite tricky to have while in build layout mode; that could work tho, but it may have a large impact on incrementality as META file is not per-plugin
My feeling is that you will end up reimplementing sites if you try to fix that, so maybe we would be better off trying out sites, and waiting a bit until the feature is stable.
The rules for coq-theory are defined here mainly https://github.com/ocaml/dune/blob/main/src/dune_rules/coq_rules.ml#L250
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:12):setup_ml_deps
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:13):It is a pity I didn't have time to resurrect coq_dune yet, that would have make your experiments much easier
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:13):But I'm fully booked until Dec 10th :( :(
Enrico Tassi (Nov 19 2021 at 15:14):Thanks for the pointer, I'll look at it.
Enrico Tassi (Nov 19 2021 at 15:15):But I here see https://github.com/ocaml/dune/blob/163168cae9f3419bcafc026ec0209c797b99f9d9/src/dune_rules/coq_rules.ml#L256 that the .ml code of dune mentions the name of a coq sub library. This does not look very sound to me, if we rename it or move it we break dune
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:17):That's for native, we could make this configurable
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:17):native support is still experimental
Gaëtan Gilbert (Nov 19 2021 at 15:19):not sure if we can depend on stuff in _build/install while building
we may need to have some special code for -boot mode
Enrico Tassi (Nov 19 2021 at 15:21):what I don't get is why coq-stlib does not depend on the fully built package coq-core. It seems like shooting yourself in the foot for what, 3 seconds? (it depends on all the plugins, so...)
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:22):Gaëtan Gilbert said:
not sure if we can depend on stuff in _build/install while building
we may need to have some special code for -boot mode
You can, it is just a bit of layering "violation", you would like the install rules to be self-contained
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:23):Enrico Tassi said:
what I don't get is why coq-stlib does not depend on the fully build package coq-core. It seems like shooting yourself in the foot for what, 3 seconds
?
I didn't measure, but it makes sense that dune takes the dependencies coqdep says
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:23):having dune build theories/Prelude.vo build a full package seems like a pretty poor implementation to me
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:24):why should that build a lot of unrelated plugins
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:24):?
Enrico Tassi (Nov 19 2021 at 15:24):that would not work, prelude in coq-stdlib
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:24):Enrico Tassi said:
that would not work, prelude in coq-stdlib
what do you mean? That works fine now
Enrico Tassi (Nov 19 2021 at 15:25):it is not a lot of unrelated plugins, it is 10 ml files
Enrico Tassi (Nov 19 2021 at 15:26):and if they are not part of "core", well then they should be moved elsewhere.
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:26):also if I update for example ssreflect, with your proposal the full stdlib has to be built
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:26):that seems pretty poor incremental behavior to me
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:27):very unfortunately what I discover is that findlib won't work well for us, we need something like sites
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:27):it didn't work for Frama-C either, so that's why Bobot [original author of findlib.dynload support in Dune] wrote sites
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:28):actually findlib.dynload in Dune is deprecated, Bobot told me, at least in his view
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:28):I use it for serapi and is very cool, but hits some limitations for example in our case
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:28):the moment your plugins are not terminal objects of the build DAG, you are in pain
Enrico Tassi (Nov 19 2021 at 15:30):I can use sites, I don't care what to use, but the doc says it is experimental
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:32):We should talk with François, but it seems to me that maybe that's a better path
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:32):we can wait a bit for that to stabilize, we can live a bit more with the lack of dep loading IMO
Emilio Jesús Gallego Arias (Nov 19 2021 at 15:34):if that works for us out of the box that's a big time saver
Rudi Grinberg (Nov 19 2021 at 17:20):Dune 3 is now feature frozen, but I would have liked this feature to graduate from experimental for 3.0
Rudi Grinberg (Nov 19 2021 at 17:21):It's of course best to ask Francois.
Emilio Jesús Gallego Arias (Nov 19 2021 at 17:21):Yeah it needs more testing, but we are not in a rush
Emilio Jesús Gallego Arias (Nov 19 2021 at 17:22):IMO, see latest fixes by PIerre-Yves
Emilio Jesús Gallego Arias (Nov 19 2021 at 17:22):if we get a tree in Coq with the feature
Emilio Jesús Gallego Arias (Nov 19 2021 at 17:22):we will get some testing, and we can then make it optional for a bit
Rudi Grinberg (Nov 19 2021 at 17:23):I rewrote docs the for this feature because I thought it was so cool and deserved more adoption. Glad to see you're making use of it
Enrico Tassi (Nov 19 2021 at 19:28):how much sites are dune specific for plugins? Because we do have plugins that don't use dune. For findlib, it's just a text file to be put in the right place. Do site need something like this?
Emilio Jesús Gallego Arias (Nov 19 2021 at 20:51):sites requires dune, but also findlib.dynload is pretty hard to use unless you use dune I think
Emilio Jesús Gallego Arias (Nov 19 2021 at 20:51):plugins not using dune can just use the regular loading mech
Enrico Tassi (Nov 19 2021 at 21:36):using dynload for the main program is tricky without dune, but coq uses it. for a plugin it is trivial, although coq_makefile does not generate it for you yet
Emilio Jesús Gallego Arias (Nov 22 2021 at 09:44):Actually I think I got confused on something I said before, as Rudi mentioned, the META file doesn't depend on the plugins, so you can indeed have good incrementality then, but you need to inject both the meta dep and the particular plugin transitive chain dep for each output of coqdep coq.plugin.foo
Emilio Jesús Gallego Arias (Nov 22 2021 at 09:45):So maybe that's not so bad after all, other than findlib not being aware of build layout, but we need to ask François to see what problem he had with this because I think there was still a problem and this is why he did the sites plugin stuff
Enrico Tassi (Nov 22 2021 at 13:30):I tried to learn more about sites looking that the PR which introduced it, and the header says the dependency has to be on the package, so maybe I'm misunderstanding it, but it could just be the same WRT incrementality. Is there an easy way to check these dependencies? (I'm not familiar with the code base)
Emilio Jesús Gallego Arias (Nov 22 2021 at 15:04):You can dump the rules and main has some nice stuff for debugging, but IMHO the best is to ask Francois, that stuff is subtle as there is a database involved
Emilio Jesús Gallego Arias (Nov 22 2021 at 15:04):so it is not just a file to file dependency, but the database has to be right
Last updated: Jun 04 2023 at 22:30 UTC