Stream: Dune devs & users

Topic: META file generation


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Rudi Grinberg (Nov 18 2021 at 15:05):

But to answer your question, you have two options:

  1. You can depend on the installed artifacts of the package (deps (package coq-core))
  2. Or on the META file directly: %{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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Nov 18 2021 at 18:03):

thanks Gaëtan, I think you found the bug

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 19 2021 at 15:12):

setup_ml_deps

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 19 2021 at 15:13):

But I'm fully booked until Dec 10th :( :(

view this post on Zulip Enrico Tassi (Nov 19 2021 at 15:14):

Thanks for the pointer, I'll look at it.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 19 2021 at 15:17):

That's for native, we could make this configurable

view this post on Zulip Emilio Jesús Gallego Arias (Nov 19 2021 at 15:17):

native support is still experimental

view this post on Zulip 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

view this post on Zulip 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...)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 19 2021 at 15:24):

why should that build a lot of unrelated plugins

view this post on Zulip Emilio Jesús Gallego Arias (Nov 19 2021 at 15:24):

?

view this post on Zulip Enrico Tassi (Nov 19 2021 at 15:24):

that would not work, prelude in coq-stdlib

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Nov 19 2021 at 15:25):

it is not a lot of unrelated plugins, it is 10 ml files

view this post on Zulip Enrico Tassi (Nov 19 2021 at 15:26):

and if they are not part of "core", well then they should be moved elsewhere.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 19 2021 at 15:26):

that seems pretty poor incremental behavior to me

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Rudi Grinberg (Nov 19 2021 at 17:21):

It's of course best to ask Francois.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 19 2021 at 17:21):

Yeah it needs more testing, but we are not in a rush

view this post on Zulip Emilio Jesús Gallego Arias (Nov 19 2021 at 17:22):

IMO, see latest fixes by PIerre-Yves

view this post on Zulip Emilio Jesús Gallego Arias (Nov 19 2021 at 17:22):

if we get a tree in Coq with the feature

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 19 2021 at 20:51):

plugins not using dune can just use the regular loading mech

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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: Feb 04 2023 at 02:03 UTC