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
it's annoying, and I'm not sure why it's run once per file instead of globally, but the dependencies seem "right"...
adding foo.v
if you require foo
from somewhere can change the result, no?
but modifying a required file once it's added doesn't change the result
yes, I agree that dune
's doing a pretty coarse approximation, but I don't think dune
lets you express the dependency you want..
also, has coqdep
become deterministic suddenly? I thought that was still a work-in-progress.
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.
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.
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
This is indeed a bug or missing optimization, Gaëtan is right
would be great to fix this, by the way I already have a tree to call coqdep only once for theory
So we have two problems with the current implementation:
The reason I implemented the more granular call setup was due to maybe hoping we would indeed be able to do like ocamldep
modules
so actually we drop the dependency on .v files
maybe we can do it
but as of today that behavior is really non-optimal
Actually it is a bit more subtle than that, now we depend before we call coqdep, on the contents of all files
but it is tricky to define only "existence"
as we may have generated files
and that is one thing Dune does very well, managing generated .v files
Emilio Jesús Gallego Arias said:
- coqdep is called once per .v file, would be more efficient to call ti once
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
indeed maybe we can improve coqdep now enough so Dune can resolve From ...
from its side
Last updated: Oct 13 2024 at 01:02 UTC