diff options
| author | Maxime Dénès | 2019-04-25 14:09:42 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-05-07 10:02:56 +0200 |
| commit | 9779c0bf4945693bfd37b141e2c9f0fea200ba4d (patch) | |
| tree | 26f563e3ad9562bdeb67efe8ff55be5de7fc55e2 /test-suite/Makefile | |
| parent | 392d40134c9cd7dee882e31da96369dd09fbbb45 (diff) | |
Integrate build and documentation of Ltac2
Since Ltac2 cannot be put under the stdlib logical root (some file names
would clash), we move it to the `user-contrib` directory, to avoid adding
another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego.
Thanks to @Zimmi48 for the thorough documentation review and the
numerous suggestions.
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 ba591ede20..94011447d7 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -99,7 +99,7 @@ INTERACTIVE := interactive UNIT_TESTS := unit-tests VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ - coqdoc ssr arithmetic + coqdoc ssr arithmetic ltac2 # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS) @@ -181,6 +181,7 @@ summary: $(call summary_dir, "tools/ tests", tools); \ $(call summary_dir, "Unit tests", unit-tests); \ $(call summary_dir, "Machine arithmetic tests", arithmetic); \ + $(call summary_dir, "Ltac2 tests", ltac2); \ 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`; \ @@ -319,7 +320,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v } > "$@" ssr: $(wildcard ssr/*.v:%.v=%.v.log) -$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithmetic/*.v)): %.v.log: %.v $(PREREQUISITELOG) +$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithmetic/*.v ltac2/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ opts="$(if $(findstring modules/,$<),-R modules Mods)"; \ |