Skip to content

Commit

Permalink
[test-suite] Fix dependencies of modules/ files
Browse files Browse the repository at this point in the history
Fixes #12582

The previous code said that `Nat.v.log` (and therefore `Nat.vo`) should
be rebuilt anytime `Nat.v.log` is older than `plik.v.vo`, and also says
that `plik.v.log` (and therefore `plik.vo`) should be rebuilt anytime
`plik.v.log` is older than `Nat.vo`.  This is circular, and results in
`make` considering all of the `modules/` tests out-of-date on any fresh
run.

(cherry picked from commit 9690b13)
  • Loading branch information
JasonGross authored and Zimmi48 committed Jun 29, 2020
1 parent 7fd7a81 commit 734fd00
Show file tree
Hide file tree
Showing 2 changed files with 13 additions and 1 deletion.
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
- **Fixed:**
Running ``make`` in ``test-suite/`` twice (or more) in a row will no longer
rebuild the ``modules/`` tests on subsequent runs, if they have not been
modified in the meantime (`#12583 <https://github.com/coq/coq/pull/12583>`_,
fixes `#12582 <https://github.com/coq/coq/issues/12582>`_, by Jason Gross).
9 changes: 8 additions & 1 deletion test-suite/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -629,7 +629,14 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG
} > "$@"

# Additional dependencies for module tests
$(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.vo
COMMON_MODULE_DEPENDENCIES := modules/plik.v modules/Nat.v
# We exclude Nat.v.log and plik.v.log because these log files do not
# depend on having the corresponding .vo files built first, and we end
# up with pseudo-cyclic build rules if we don't exclude them (See
# COQBUG(https://github.com/coq/coq/issues/12582)). Additionally, we
# impose order-only dependencies to ensure that we won't rebuild the
# .vo files in the .log target after we've already built them.
$(addsuffix .log,$(filter-out $(COMMON_MODULE_DEPENDENCIES),$(wildcard modules/*.v))): %.v.log: $(COMMON_MODULE_DEPENDENCIES:.v=.vo) | $(COMMON_MODULE_DEPENDENCIES:.v=.v.log)
modules/%.vo: modules/%.v
$(HIDE)$(coqc) -R modules Mods $<

Expand Down

0 comments on commit 734fd00

Please sign in to comment.