Rodolphe Lepigre (Feb 27 2024 at 13:13): Rodolphe Lepigre (Feb 27 2024 at 13:13):FYI @Janno and I found a pretty bad bug in dune 3.13.0 and above, that leads to all Coq files being compiled as soon as any (even unrelated) dependency changes (see https://github.com/ocaml/dune/issues/10149). We managed to identify the commit introducing the regression, but I'm not familiar enough with how dependencies are collected to quickly fix it. Any help would be appreciated.
Emilio Jesús Gallego Arias (Feb 27 2024 at 14:53):Indeed that's a tricky one, the Dune API has changed so much since the first Coq dune code, I'm unsure what the semantics of some parts are.
Moreover I'm suprised you didn't observe this regression already on https://github.com/ocaml/dune/pull/7048 .
I hope we can resolve it soon tho, see my comment on the issue.
Note that also you may want to backport https://github.com/ocaml/dune/pull/10116
Rodolphe Lepigre (Feb 27 2024 at 14:58):Yeah, I hope this can be fixed quickly: we really want the new (dynamic_include ..) stanza. It'd be a shame to have to roll back to 3.12.2.
Rodolphe Lepigre (Feb 27 2024 at 14:59):Maybe the easiest fix would be to go back to calling coqdep per file, as I think you suggested? (Or at least to generate independent files.)
Rodolphe Lepigre (Feb 27 2024 at 15:00):(Yeah, we were thinking of backporting those.)
Rodolphe Lepigre (Feb 27 2024 at 15:01):Emilio Jesús Gallego Arias said:
Moreover I'm suprised you didn't observe this regression already on https://github.com/ocaml/dune/pull/7048 .
I don't think the regression was there after this MR, right?
Emilio Jesús Gallego Arias (Feb 27 2024 at 15:01):I think for now we want to get some feedback from Andrey and Rudi, a fixup is pretty easy tho if you need something now.
Emilio Jesús Gallego Arias (Feb 27 2024 at 15:02):Rodolphe Lepigre said:
Emilio Jesús Gallego Arias said:
Moreover I'm suprised you didn't observe this regression already on https://github.com/ocaml/dune/pull/7048 .
I don't think the regression was there after this MR, right?
Depends on the semantics we assume for Action_builder , indeed it is puzzling the regression happen in that commit bisect, we need more info from the engine folks.
Rodolphe Lepigre (Feb 27 2024 at 15:02):We don't need something right now, but we'll definitely need something in the next couple of days.
Emilio Jesús Gallego Arias (Feb 27 2024 at 15:05):It may require more time upstream, so meanwhile you can try this solution:
setup_theory_rules add a new setup_per_file_rules.file.v.d file with the result of Dep_map.find Emilio Jesús Gallego Arias (Feb 27 2024 at 15:05):so this will add N write file overhead to a build where the file listing changes
Emilio Jesús Gallego Arias (Feb 27 2024 at 15:05):where N = number of files in the theory
Emilio Jesús Gallego Arias (Feb 27 2024 at 15:05):but still on linux, that should be pretty minimal
Emilio Jesús Gallego Arias (Feb 27 2024 at 15:06):Let me know if you have any question about the above fix
Rodolphe Lepigre (Feb 27 2024 at 15:06):OK thanks, I'll see if I can give it a go in the next couple of days.
Emilio Jesús Gallego Arias (Feb 27 2024 at 15:06):So instead of the two current rules:
{ list of sources } ---[coqdep]---> { .foo.d.v }
{ .foo.d.v } ---[build_map]---> { dep_map } ---[find]---> { dep files } ---[coqc]---> { .vo }
we have 3 rules
Emilio Jesús Gallego Arias (Feb 27 2024 at 15:08):so things factor thru the new file rule:
{ .foo.v.d } ---[ build_map } ----> { dep_map } ---[find] ---{ file.v.d }
I've written the code anyways, let me push the branch.
Ali Caglayan (Apr 20 2024 at 12:36):FTR this turned out to be a bug introduced during unrelated refactoring in Action_builder.contents. This is an internal API that is used to read contents of a file and pipe them along to generate actions. The previous semantics before the refactoring was that files could be read, but there was no dependency on the files itself generated. This allowed for coqdep to output a file and other Coq related actions to be generated without actually depending on the output of coqdep as a file, but rather being contents aware. Same content = same rules. This was broken unintenionally in the refactoring leading to a spurious dependency being declared on files being read. This meant that every time the output of coqdep changed, the entire project got rebuilt.
I submitted a fix here once I noticed the root cause of this issue: https://github.com/ocaml/dune/pull/10446
It is a very subtle bug, in that we might be the only consumer of that API so a sensible looking change didn't have an affect on anything else. Coq is tested in the Dune test suite, but obviously we can't test every possible behaviour so nobody (in Dune) noticed this since 3.13.
I'm going to advocate for this to be backported to all affected Dune versions. These are currently 3.13, 3.14 and 3.15.
Rodolphe Lepigre (Apr 20 2024 at 12:39):Great work, thanks a lot @Ali Caglayan!
Emilio Jesús Gallego Arias (Apr 22 2024 at 11:26):Thanks a lot @Ali Caglayan , I'm glad we could look into this; I'm on holidays now and indeed lacking time lately due to some reorganization of my work tasks.
Emilio Jesús Gallego Arias (Apr 22 2024 at 11:33):I still wonder tho about the current semantics of contents, IMHO the current documentation is a bit ambigous, it would be good to note that it doesn't record a dep on file.
Emilio Jesús Gallego Arias (Apr 22 2024 at 11:33):But now that I think of it, it is maybe likely obvious?
Emilio Jesús Gallego Arias (Apr 22 2024 at 11:33):I guess we can think of cases where people could expect either semantics
Ali Caglayan (Apr 22 2024 at 12:45):We are the only really serious user of contents so I think adding a comment in the API explicitly stating that this does not record the file as a dependency would be the correct thing to do.
Ali Caglayan (Apr 22 2024 at 12:45):If there is a reason to expect the other semantics, then the correct gadget should be added to action_builder.
Emilio Jesús Gallego Arias (Apr 25 2024 at 13:09):I agree. This stuff is very subtle! I get myself confused about the semantics all the time, but indeed, the non-recording semantics are the right ones.
Last updated: Oct 13 2024 at 01:02 UTC