diff options
| author | Hugo Herbelin | 2016-10-24 11:44:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-10-24 11:48:36 +0200 |
| commit | 1d769e02b3baba54246c942fe116abaf850892db (patch) | |
| tree | e4da7895f3065c5f3d26c2da56b0d420ca28ea44 | |
| parent | 80d5779409bf33fbe5043275b96775a5f04a3b2c (diff) | |
Fix 6d5fe92e to #5150 (missing dependencies in test suite) was a bit too strong.
New fix. A bit less consistent with the spirit of this Makefile as we
list prerequisite files explicitly, but avoid to redo subsystems at
each call to "make" as with previous fix.
Other solutions from experts are welcome.
| -rw-r--r-- | test-suite/Makefile | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 8500ef1b3d..491b16960e 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -84,6 +84,9 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk +PREREQUISITELOG = prerequisite/admit.v.log \ + prerequisite/make_local.v.log prerequisite/make_notation.v.log + ####################################################################### # Phony targets ####################################################################### @@ -221,7 +224,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \ @@ -253,7 +256,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -267,7 +270,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite fi; \ } > "$@" -$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite +$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -289,7 +292,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite rm $$tmpoutput; \ } > "$@" -$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -307,7 +310,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite # the .v file with exactly two digits after the dot. The reference for # time is a 6120 bogomips cpu. ifneq (,$(bogomips)) -$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -338,7 +341,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite endif # Ideal-features tests -$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v prerequisite +$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ |