diff options
| author | Enrico Tassi | 2014-12-26 15:51:57 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-12-26 16:00:31 +0100 |
| commit | 3f4af783a249aab22d0d772bf21a0d5284aba407 (patch) | |
| tree | bbe13c0f7b7374f0314cb5fdc1cb063a31238272 /test-suite/Makefile | |
| parent | 2919e4a927a4574a28012ae4ba9523e01fed1360 (diff) | |
new test for coqchk
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index a144d6a55b..45a2e20464 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -82,7 +82,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ interactive micromega $(COMPLEXITY) modules stm # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vi +SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vi coqchk ####################################################################### # Phony targets @@ -443,3 +443,20 @@ vi: $(patsubst %.v,%.vi.log,$(wildcard vi/*.v)) echo " $<...Error!"; \ fi; \ } > "$@" + +coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) + +%.chk.log:%.v + @echo "TEST $<" + $(HIDE){ \ + $(bincoqc) -R coqchk coqchk $* 2>&1 && \ + $(bincoqchk) -R coqchk coqchk -norec $(subst /,.,$*) 2>&1; \ + if [ $$? = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + else \ + echo $(log_failure); \ + echo " $<...Error!"; \ + fi; \ + } > "$@" + |