Skip to content

Commit

Permalink
[3.15] Backport #10446 (#10450)
Browse files Browse the repository at this point in the history
* Add reproduction test case for #10149.

Signed-off-by: Rodolphe Lepigre <[email protected]>
Signed-off-by: Ali Caglayan <[email protected]>

* stop recording deps in Action_builder.contents

PR #9552 changed the semantics of Action_builder.contents so that it
records a dependency. The Coq rules were relying on the previous
behaviour of not recording a dependency in order to generate a build
plan. This caused issue #10149 to appear.

This PR fixes #10149 by removing the dependency being recorded in
Action_builder.contents matching the previous semantics.

Signed-off-by: Ali Caglayan <[email protected]>

---------

Signed-off-by: Rodolphe Lepigre <[email protected]>
Signed-off-by: Ali Caglayan <[email protected]>
Co-authored-by: Rodolphe Lepigre <[email protected]>
Co-authored-by: Ali Caglayan <[email protected]>
  • Loading branch information
3 people authored Apr 23, 2024
1 parent d48eef9 commit e258ed1
Show file tree
Hide file tree
Showing 3 changed files with 20 additions and 6 deletions.
2 changes: 2 additions & 0 deletions doc/changes/10446.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
- Fix a bug where Coq projects were being rebuilt from scratch each time the
dependency graph changed. (#10446, fixes #10149, @alizter)
7 changes: 1 addition & 6 deletions src/dune_rules/action_builder.ml
Original file line number Diff line number Diff line change
Expand Up @@ -37,12 +37,7 @@ let paths ps = deps (Dep.Set.of_files ps)
let path_set ps = deps (Dep.Set.of_files_set ps)
let dyn_paths paths = dyn_deps (paths >>| fun (x, paths) -> x, Dep.Set.of_files paths)
let dyn_paths_unit paths = dyn_deps (paths >>| fun paths -> (), Dep.Set.of_files paths)

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

let contents p = of_memo (Build_system.read_file p)
let lines_of p = contents p >>| String.split_lines

let read_sexp p =
Expand Down
17 changes: 17 additions & 0 deletions test/blackbox-tests/test-cases/coq/no-rebuild-on-dep-change.t
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
$ echo "(coq.theory (name bug) (mode vo))" > dune
$ echo "(lang dune 3.12)" > dune-project
$ echo "(using coq 0.8)" >> dune-project
$ touch root.v leaf.v
$ dune build
$ find _build -name "*.vo" | sort
_build/default/leaf.vo
_build/default/root.vo
$ echo "Require Import bug.root." >> leaf.v

This test makes sure that a full rebuild is not triggered when the output of
coqdep is changed.

This is as expected:
$ dune build --display=short
coqdep .bug.theory.d
coqc leaf.{glob,vo}

0 comments on commit e258ed1

Please sign in to comment.