Stream: Dune devs & users

Topic: too much coqdep


view this post on Zulip Gaëtan Gilbert (Oct 27 2021 at 12:13):

dune runs coqdep more than I would expect
I'm guessing that it thinks foo.v.d depends on the contents of all visible .v files, where it should be the contents of foo.v and the list of existing other files

view this post on Zulip Paolo Giarrusso (Oct 27 2021 at 14:08):

it's annoying, and I'm not sure why it's run once per file instead of globally, but the dependencies seem "right"...

view this post on Zulip Paolo Giarrusso (Oct 27 2021 at 14:08):

adding foo.v if you require foo from somewhere can change the result, no?

view this post on Zulip Gaëtan Gilbert (Oct 27 2021 at 14:12):

but modifying a required file once it's added doesn't change the result

view this post on Zulip Paolo Giarrusso (Oct 27 2021 at 14:12):

yes, I agree that dune's doing a pretty coarse approximation, but I don't think dune lets you express the dependency you want..

view this post on Zulip Paolo Giarrusso (Oct 27 2021 at 14:15):

also, has coqdep become deterministic suddenly? I thought that was still a work-in-progress.

view this post on Zulip Paolo Giarrusso (Oct 27 2021 at 14:17):

and I _hope_ dune doesn't let you depend on the order of directory entries (which is the source of non-determinism) — while I don't have a vote, if I had one, I'd say that's a WONTFIX: compilers should sort their file listings if they care.

view this post on Zulip Paolo Giarrusso (Oct 27 2021 at 14:30):

Paolo Giarrusso said:

also, has coqdep become deterministic suddenly? I thought that was still a work-in-progress.

_Maybe_ yes, as of today/8.15: https://github.com/coq/coq/pull/14718.

view this post on Zulip Rudi Grinberg (Oct 27 2021 at 17:11):

I think @Emilio Jesús Gallego Arias did it intentionally this way. FWIW we run ocamldep once per ocaml source in dune’s ocaml rules

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 09:03):

This is indeed a bug or missing optimization, Gaëtan is right

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 09:03):

would be great to fix this, by the way I already have a tree to call coqdep only once for theory

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 09:04):

So we have two problems with the current implementation:

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 09:05):

The reason I implemented the more granular call setup was due to maybe hoping we would indeed be able to do like ocamldep modules

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 09:05):

so actually we drop the dependency on .v files

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 09:05):

maybe we can do it

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 09:06):

but as of today that behavior is really non-optimal

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 09:09):

Actually it is a bit more subtle than that, now we depend before we call coqdep, on the contents of all files

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 09:09):

but it is tricky to define only "existence"

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 09:09):

as we may have generated files

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 09:09):

and that is one thing Dune does very well, managing generated .v files

view this post on Zulip Gaëtan Gilbert (Oct 28 2021 at 09:19):

Emilio Jesús Gallego Arias said:

not in incremental builds though

The reason I implemented the more granular call setup was due to maybe hoping we would indeed be able to do like ocamldep modules

should be pretty easy, we just have to pick an output format that can represent From

view this post on Zulip Emilio Jesús Gallego Arias (Oct 28 2021 at 14:50):

indeed maybe we can improve coqdep now enough so Dune can resolve From ... from its side


Last updated: Jan 30 2023 at 18:04 UTC