dune always rebuilds all coq files as soon as any dependency changes

[Janno]

Expected Behavior

Only leaf.vo gets rebuild.

Actual Behavior

All files get rebuilt, including other_root.vo (the added dependency) as well as root.v (the existing dependency).

Reproduction

• PR with a reproducing test:
  Add reproduction test case for #10149. #10150

The steps below can be used to reproduce exactly the behavior described above but the reproducing PR has a smaller test case that is better suited to debugging this.

1. Extract bug.zip
2. cd bug
3. dune build coq
4. echo "Require Import bug.other_root." >> coq/leaf.v
5. dune build coq

Specifications

• Version of dune (output of dune --version): 3.13.0, master
• Version of ocaml (output of ocamlc --version): 4.14.1
• Operating system (distribution and version): linux

Additional information

git bisect points to:

2876a55d2646cdd8fa130398f3fdfb7f8acdbd9f is the first bad commit
commit 2876a55d2646cdd8fa130398f3fdfb7f8acdbd9f
Author: Rudi Grinberg <me@rgrinberg.com>
Date:   Wed Dec 20 18:52:18 2023 -0600

    refactor: switch to new API for recording deps (#9552)
    
    Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

 src/dune_engine/action_builder.ml                  | 93 +++++++++++++++++-----
 src/dune_engine/action_builder.mli                 | 41 ++++++++--
 src/dune_engine/build_system.ml                    | 37 +++------
 src/dune_engine/build_system.mli                   |  3 +
 src/dune_engine/load_rules.ml                      | 47 +++++------
 src/dune_rules/action_builder.ml                   | 14 +---
 src/dune_rules/alias_builder.ml                    | 47 ++++-------
 .../test-cases/special_files.t/run.t               |  3 +-
 8 files changed, 164 insertions(+), 121 deletions(-)
bisect found first bad commit

The corresponding PR is #9552

CC @rlepigre

[ejgallego]

Thanks for the detailed bug report @Janno , I can reproduce in master.

[ejgallego]

Did some tracing in the coq side of rules, everything seems fine on this side:

deps_for _build/default/coq/leaf.vo: _build/default/coq/leaf.v _build/default/coq/root.vo
deps_for _build/default/coq/other_root.vo: _build/default/coq/other_root.v
deps_for _build/default/coq/root.vo: _build/default/coq/root.v

and after the edit, it becomes:

deps_for _build/default/coq/leaf.vo: _build/default/coq/leaf.v _build/default/coq/root.vo _build/default/coq/other_root.vo
deps_for _build/default/coq/other_root.vo: _build/default/coq/other_root.v
deps_for _build/default/coq/root.vo: _build/default/coq/root.v

[rlepigre]

Did some tracing in the coq side of rules, everything seems fine on this side:

Yeah, we did check the output of coqdep, and it looks as expected. It's like somehow the .*.theory.d is considered a dependency of all .v files implicitly. Maybe the dependencies API was misused before the refactoring commit that introduced the problem?

[ejgallego]

Indeed, the API has been changing a lot and is not very documented, so I'm indeed unsure we can really do what we want in Coq easily (and I wonder why it worked before).

The code looks too coupled in fact. Let me summarize what we are doing:

• Memo.t is the type for general computations, Action_builder.t is a helper to record dependencies into Memo.

First, we add a rule to generate coq/.bug.theory.d, the codep file, the rule is like this:

{ listing of all source files } --[coqdep]--> { coq/.bug.theory.d }

Then, we add the coqc rule, and indeed this could be problematic in the way we do it, the code looks like

let get_dep_map dir wrapper_name : Path.t list Dep_map.t Action_builder.t =
  let file = "$dir/.$wrapper_name.theory.d" in
  let* lines = Action_builder.lines_of file in
  build_map lines

let get_dep_map : (Dir.t * Coq_lib_name.t, Path.t list Dep_map.t) Action_builder.memo = ....

let deps_of file dir wrapper_name : unit Action_builder.t =
  let* dep_map = Action_builder.exec_memo get_dep_map (dir, wrapper_name) in
  let deps = Dep_map.find file in
  Action_builder.paths deps 

So, indeed, this is an action that will be re-run when the coqdep file has a different hash, and the calculation of the map is now memoized (see recent bug that for sure impacted your zero-builds big time).

But indeed I'm guessing that already the above code is adding the coqdep file as a hard dep to the full coqc action, as we do in the coqc rule:

let deps_of = deps_of file ... in
Action_builder.with_no_targets deps_of >>> Command.run coqc args

So indeed, this code admits the semantics we observe in this bug, where the coqc rule is triggered due to the dependency on the theory.d file.

I am thinking how to workaround this, an obvious way, but still not satisfactory, is to produce a .v.d file for each file, from the map.

This way, your coqdep update will rebuild all the .v.d files (which is fast, but still annoying), but the coqc rule would only register the dependency for the file, that in this case, would trigger a cutoff.

I guess in order to implement the true incremental Dep_map structure that we want, we'd need to use the engine a bit more fine grained, maybe using evaluate_and_collect_deps and / or creating a memo node per file?

I'll let experts (cc @rgrinberg @snowleopard ) comment tho.

[ejgallego]

I guess adding an extra memo node per file to keep the deps is fine. @rlepigre , in a sense what we need here is something like https://ocaml.org/p/incr_map/latest , but using Memo.t instead of Incremental.t.

[I didn't have time to look at incr_map yet, but our use case is the same, we maintain a map, we want to re-run only the consumers of the keys that changed]

[ejgallego]

Tried to implement the workaround of having one dep file per .v file, however I got a bit stuck on types:

https://github.com/ejgallego/dune/tree/gen_dep_per_file

Basically I forgot how to chain an map Action_builder.t (that reads the map) with an unit Action_build.With_targets.t that writes the result of Dep_map.find map key.

I guess I'm too tired today to look into this more, feel free to take over.

[ejgallego]

Indeed, I was a bit tired and didn't distinguish 'a t from 'a.

The branch is now functional, just needs a cleanup to be submitted as a PR; please test and report back.

[ejgallego]

I'm still quite puzzled about the commit you bisected tho. The change in semantics seems quite big if that's the case, tho I'd say that PR is more of bugfix then, for the semantics I have in mind.

[rlepigre]

Thanks a lot @ejgallego, I'll have a look when I have a minute.

[rlepigre]

@ejgallego sorry for the lag, but your patch does fix the regression, so thanks again.

How do we get that fixed properly though? Do you want to make an MR with this proposal?

[ejgallego]

I'd suggest you folks use this patch for now, it should be pretty safe.

I'd like to think about this and likely discuss with Dune devs as to be sure the new semantics are the intended one.

I was fully booked these two weeks, but next week looks more promising.

[Alizter]

This has unfortunately made dune unusable for Coq with 3.14 onwards. I will try to allocate some time to investigate the issue.

Did anybody manage to bisect where this was introduced?

[rlepigre]

Yes, we bisected it, and it is in the issue description. 😄

@ejgallego also has a fix that works for us at BedRock Systems (we're currently using a patched version of dune).

[ejgallego]

@Alizter indeed it seems that the way actions are run changed.

This is waiting on me being able to attend a Dune dev meeting as to discuss what is going on, but I think indeed we were relying on a Dune engine bug.

[ejgallego]

Feel free to take over my branch and submit the fix tho, I'm sorry I couldn't be more responsive on this.

[Alizter]

The culprit is this line:

dune/src/dune_rules/action_builder.ml

Lines 44 to 47 in 60b2a3c

	let contents p =
	let* () = Dep.file p |> Dep.Set.singleton |> Build_system.record_deps in
	of_memo (Build_system.read_file p)
	;;

Removing the recording of deps here fixes the issue.

[Alizter]

Here is a fix:

• stop recording deps in Action_builder.contents #10446