diff options
| author | Enrico Tassi | 2014-12-10 11:40:23 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-12-10 11:40:29 +0100 |
| commit | b6296c62d391b789dd80e90209a3498f733ae10a (patch) | |
| tree | 15fc83e7e1c9efcb57efdefb59f8d438885a1761 | |
| parent | 745c4e69f5709cc56382b650bbb36b21d3ae0ede (diff) | |
test-suite: few tests for ".v -> .vi -> .vo" compilation chain
| -rw-r--r-- | test-suite/Makefile | 23 | ||||
| -rw-r--r-- | test-suite/vi/simple.v | 2 | ||||
| -rw-r--r-- | test-suite/vi/univ_constraints_statements.v | 2 |
3 files changed, 25 insertions, 2 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 7f6a8eb9e3..ccbb4a44b9 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -32,6 +32,7 @@ LIB := .. coqtop := $(BIN)coqtop -boot -q -batch -R prerequisite TestSuite bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite +bincoqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite command := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source coqc := $(coqtop) -compile @@ -81,7 +82,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ interactive micromega $(COMPLEXITY) modules stm # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide +SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vi ####################################################################### # Phony targets @@ -100,7 +101,7 @@ clean: rm -f trace lia.cache $(SHOW) "RM <**/*.stamp> <**/*.vo> <**/*.log>" $(HIDE)find . \( \ - -name '*.stamp' -o -name '*.vo' -o -name '*.log' \ + -name '*.stamp' -o -name '*.vo' -o -name '*.vi' -o -name '*.log' \ \) -print0 | xargs -0 rm -f distclean: clean @@ -139,6 +140,7 @@ summary: $(call summary_dir, "Module tests", modules); \ $(call summary_dir, "STM tests", stm); \ $(call summary_dir, "IDE tests", ide); \ + $(call summary_dir, "IDE tests", vi); \ 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`; \ @@ -424,3 +426,20 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) echo " $<...Error!"; \ fi; \ } > "$@" + +vi: $(patsubst %.v,%.vi.log,$(wildcard vi/*.v)) + +%.vi.log:%.v + @echo "TEST $<" + $(HIDE){ \ + $(bincoqc) -quick -R vi vi $* 2>&1 && \ + $(coqtop) -R vi vi -vi2vo $*.vi 2>&1 && \ + $(bincoqchk) -R vi vi $(subst /,.,$*) 2>&1; \ + if [ $$? = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + else \ + echo $(log_failure); \ + echo " $<...Error!"; \ + fi; \ + } > "$@" diff --git a/test-suite/vi/simple.v b/test-suite/vi/simple.v new file mode 100644 index 0000000000..407074c1e7 --- /dev/null +++ b/test-suite/vi/simple.v @@ -0,0 +1,2 @@ +Lemma simple : True. +Proof using. trivial. Qed. diff --git a/test-suite/vi/univ_constraints_statements.v b/test-suite/vi/univ_constraints_statements.v new file mode 100644 index 0000000000..bb6b95957d --- /dev/null +++ b/test-suite/vi/univ_constraints_statements.v @@ -0,0 +1,2 @@ +Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal -> Plemma -> Pgoal. +Proof using. intro H; rewrite H; trivial. Qed. |