Stream: Dune devs & users

Topic: Extra Dependency


view this post on Zulip Enrico Tassi (Dec 29 2023 at 17:56):

I'm trying to port elpi to dune but I'm having hard times making Extra Dependency work.
My understanding is that a file which is not .v nor .ml is not copied in the source tree inside _build, so coqdep does not find it (and emits a warning that the extra dep was not found).
Is there a way to force dune to copy non .v files inside _build? I'm trying with copy_files but that does not count as a dependency so the files are only copied if needed. I did manage by writing a custom rule to generate the .v file, which depends on the extra dependency, but that defeats the purpose of the Extra Dependency thing.
Is Extra Dependency expected to work under dune?

view this post on Zulip Enrico Tassi (Dec 29 2023 at 18:03):

https://github.com/ocaml/dune/issues/7091

view this post on Zulip Enrico Tassi (Dec 29 2023 at 18:05):

Apparently it is a known issue opened since February

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 21:52):

Yep. IIRC, ignoring coqdep's warning "works" for installed files, but of course it's not satisfactory

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 21:53):

BTW, we should understand when and how Extra Dependency is supposed to work from the workspace to installed files

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 21:53):

@Emilio Jesús Gallego Arias @Ali Caglayan BTW, why does dune run coqdep after copying files into _build?

view this post on Zulip Enrico Tassi (Dec 29 2023 at 21:54):

you mean, "why doesn't"

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 21:54):

I don't think so?

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 21:55):

Dune copies a hardcoded list of files into _build, then runs coqdep. I'm asking/suggesting to first run coqdep, and then copy files and their deps

view this post on Zulip Enrico Tassi (Dec 29 2023 at 21:55):

sorry, I misunderstood. It runs it inside the _build directory, so after copying some stuff there

view this post on Zulip Emilio Jesús Gallego Arias (Dec 29 2023 at 21:55):

Paolo Giarrusso said:

Emilio Jesús Gallego Arias Ali Caglayan BTW, why does dune run coqdep after copying files into _build?

That's a core design choice of Dune, rules can only execute on the _build dir (or in a sandbox).

A copy_file rule is added for each source file impliclty.

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 21:56):

But is this design choice a good one here?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 29 2023 at 21:56):

I think so.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 29 2023 at 21:57):

coqdep choice of emitting deps conditionally is not robust at all IMHO (usually racy, more problems can be understood)

view this post on Zulip Emilio Jesús Gallego Arias (Dec 29 2023 at 21:58):

But again you face the problem of a higher coupling: if you let the build system resolve modules (as in OCaml), you can really optimize a lot of stuff (and run build much more parallely), however this requires adding language-specific resoltion knowlegde to the build system.

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 21:59):

When you say "conditional", would you want coqdep to emit deps from A to B even when B does not exist?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 29 2023 at 22:00):

Yes. Imagine for example that B is generated

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 22:00):

We've talked about this in the past, and it could help here

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 22:00):

*would

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 22:00):

Somebody said it was like ocamldep -modules, I remember the issue

view this post on Zulip Emilio Jesús Gallego Arias (Dec 29 2023 at 22:01):

If you need to generate B before computing the deps for A, then you have a barrier with real-world impact.

Anyways, the solution of extra_sources is pretty easy to implement

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 22:01):

What if the extra dependency is into user-contrib?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 29 2023 at 22:02):

Paolo Giarrusso said:

Somebody said it was like ocamldep -modules, I remember the issue

Yes exactly. It's been a while, but IIRC, Jane Street people had to implement -modules because they were hitting real problems with build times. Coq inherited the OCaml design (ocamldep without -modules)

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 22:02):

Hm, probably my last question should be separate.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 29 2023 at 22:02):

Paolo Giarrusso said:

What if the extra dependency is into user-contrib?

What's the problem with that? Dune doesn't own user-contrib, so nothing has to be done (if Coq can resolve stuff correctly tho)

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 22:03):

I suspect the last assumption doesn't hold well

view this post on Zulip Paolo Giarrusso (Dec 29 2023 at 22:03):

But let me set that aside because I don't remember well

view this post on Zulip Enrico Tassi (Dec 29 2023 at 22:18):

To me the only design decision which is wrong is that dune assumes it can always compute dependencies correctly, hence it provides no way to override deps in corner cases. I did hit this problem with ocamldep and the approximation it does because of open and now again for coqdep. It would be trivial to say that a .v file has more deps than computed, and it would allow me to switch to dune now, waiting for the corner case of Extra Deps to be supported directly. The only workaround I found is to "generate" the .v file with a custom rule (where I can tell the deps), but that is ugly, since the .v file is not a .v anymore, hence I can't open it with my editor...

view this post on Zulip Ali Caglayan (Dec 30 2023 at 16:00):

I'm willing to implement a solution if we can agree on a design for the feature. Do we want an "extra_sources" field for the theory stanza?

view this post on Zulip Ali Caglayan (Dec 30 2023 at 16:00):

This would make sure the files needed by Extra Deps and Load are available when building the theory.

view this post on Zulip Ali Caglayan (Dec 30 2023 at 17:23):

Here is a PR for extra_sources https://github.com/ocaml/dune/pull/9591. Please test it out if you can, if anything doesn't work the way you expect then let me know.

view this post on Zulip Ali Caglayan (Dec 30 2023 at 17:23):

Once others such as @Emilio Jesús Gallego Arias have had a look and agree on the design I'll add some doucmentaiton and push it through for Dune 3.13.

view this post on Zulip Paolo Giarrusso (Dec 30 2023 at 19:57):

Yeah, we seemed to have converged on extra_sources last time in #7091, and it seems necessary in general; coqdep -modules would save some cases but it's a much larger change

view this post on Zulip Emilio Jesús Gallego Arias (Jan 10 2024 at 14:55):

Enrico Tassi said:

To me the only design decision which is wrong is that dune assumes it can always compute dependencies correctly,

Dune doesn't assume this, so it can hardly be a "wrong design decision". Dune is a generic build engine and will use as deps whatever is present in the rules. Obviously, if you pass incorrect deps you get strange (or unsound) builds.

hence it provides no way to override deps in corner cases. I did hit this problem with ocamldep and the approximation it does because of open and now again for coqdep.

It would be easy to update the OCaml rule generation code to do this, however no one so far as worked on it, as indeed, having to speficy deps manually is not very useful for the typical project that contains 100s of modules. Fixing ocamldep is a better solution, however most users are happy with the current status so there wasn't a lot of work on that.

It would be trivial to say that a .v file has more deps than computed, and it would allow me to switch to dune now, waiting for the corner case of Extra Deps to be supported directly.

If the dep computation is not correct, it seems to me a more sensible strategy to fix the dep computation.

@Ali Caglayan , thanks for the PR, actually I think this issue is a bit different than just adding extra deps, as elpi files are actually handle by the loadpath code!

I will continue in the PR


Last updated: May 25 2024 at 21:01 UTC