diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-08 17:19:22 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-10 09:54:41 +0200 |
commit | 7f17e151c0a2666263d3854c064acdfea29edf53 (patch) | |
tree | 847498081e2126d2f56e99823c4b367d7ce37e36 | |
parent | 5e690404233e6c772c1d5ddc52142edf474953ac (diff) |
Adding tests for testing exit status and #use"include".
-rw-r--r-- | test-suite/.csdp.cache | bin | 89077 -> 89077 bytes | |||
-rw-r--r-- | test-suite/Makefile | 30 | ||||
-rw-r--r-- | test-suite/misc/exitstatus/illtyped.v | 1 |
3 files changed, 30 insertions, 1 deletions
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache Binary files differindex ba85286dd..b99d80e95 100644 --- a/test-suite/.csdp.cache +++ b/test-suite/.csdp.cache diff --git a/test-suite/Makefile b/test-suite/Makefile index c10cd4ed4..779f5455a 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -33,6 +33,7 @@ LIB := $(shell cd ..; pwd) coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite bincoqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite +coqtopbyte := $(BIN)coqtop.byte command := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source coqc := $(coqtop) -compile @@ -405,7 +406,7 @@ modules/%.vo: modules/%.v # Miscellaneous tests ####################################################################### -misc: misc/deps-order.log misc/universes.log misc/deps-checksum.log +misc: misc/deps-order.log misc/universes.log misc/deps-checksum.log misc/printers.log misc/exitstatus.log # Check that both coqdep and coqtop/coqc supports -R # Check that both coqdep and coqtop/coqc takes the later -R @@ -477,6 +478,33 @@ misc/universes.log: misc/universes/all_stdlib.v misc/universes/all_stdlib.v: cd .. && $(MAKE) test-suite/$@ +misc/printers.log: + @echo "TEST printers" + $(HIDE){ \ + echo $(call log_intro,$<); \ + printf "Drop. #use\"include\";; #quit;;" | $(coqtopbyte) 2>&1 | grep Unbound; R=$$?; times; \ + if [ $$R != 0 ]; then \ + echo $(log_success); \ + echo " misc/printers...Ok"; \ + else \ + echo $(log_failure); \ + echo " misc/printers...Error!"; \ + fi; \ + } > "$@" + +misc/exitstatus.log: + @echo "TEST exitstatus" + $(HIDE){ \ + echo $(call log_intro,$<); \ + $(coqc) misc/exitstatus/illtyped.v 2>&1; R=$$?; times; \ + if [ $$R != 0 ]; then \ + echo $(log_success); \ + echo " misc/exitstatus...Ok"; \ + else \ + echo $(log_failure); \ + echo " misc/exitstatus...Error!"; \ + fi; \ + } > "$@" # IDE : some tests of backtracking for coqtop -ideslave diff --git a/test-suite/misc/exitstatus/illtyped.v b/test-suite/misc/exitstatus/illtyped.v new file mode 100644 index 000000000..df6bbb389 --- /dev/null +++ b/test-suite/misc/exitstatus/illtyped.v @@ -0,0 +1 @@ +Check S S. |