diff options
| author | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
| commit | c70412ec8b0bb34b7a5607c07d34607a147d834c (patch) | |
| tree | 0cc6cd76a8f70dfd2f5b55b0db96db4de2ff07a2 /test-suite/Makefile | |
| parent | 720ee2730684cc289cef588482323d177e0bea59 (diff) | |
| parent | 191e253d1d1ebd6c76c63b3d83f4228e46196a6e (diff) | |
Merge PR #6914: Primitive integers
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index cafc9a744c..68acb6f04d 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -95,7 +95,7 @@ INTERACTIVE := interactive UNIT_TESTS := unit-tests VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ - coqdoc ssr + coqdoc ssr arithmetic # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS) @@ -176,6 +176,7 @@ summary: $(call summary_dir, "Coqdoc tests", coqdoc); \ $(call summary_dir, "tools/ tests", tools); \ $(call summary_dir, "Unit tests", unit-tests); \ + $(call summary_dir, "Machine arithmetic tests", arithmetic); \ nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \ nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \ nb_tests=`expr $$nb_success + $$nb_failure`; \ @@ -308,7 +309,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v $(HIDE)$(coqchk) -norec TestSuite.$(shell basename $< .v) > $(shell dirname $<)/$(shell basename $< .v).chk.log 2>&1 ssr: $(wildcard ssr/*.v:%.v=%.v.log) -$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG) +$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithmetic/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ opts="$(if $(findstring modules/,$<),-R modules Mods)"; \ |