diff options
| -rw-r--r-- | test-suite/Makefile | 102 | ||||
| -rwxr-xr-x | test-suite/misc/deps-checksum.sh | 5 | ||||
| -rwxr-xr-x | test-suite/misc/deps-order.sh | 20 | ||||
| -rwxr-xr-x | test-suite/misc/exitstatus.sh | 7 | ||||
| -rwxr-xr-x | test-suite/misc/printers.sh | 3 | ||||
| -rwxr-xr-x | test-suite/misc/universes.sh | 8 |
6 files changed, 54 insertions, 91 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 5d3c11844..39ef05269 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -406,103 +406,23 @@ modules/%.vo: modules/%.v # Miscellaneous tests ####################################################################### -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 -# See bugs 2242, 2337, 2339 -deps-order: misc/deps-order.log -misc/deps-order.log: - @echo "TEST misc/deps-order" - $(HIDE){ \ - echo $(call log_intro,deps-order); \ - rm -f misc/deps/*/*.vo; \ - tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \ - $(coqdep) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 \ - | head -n 1 > $$tmpoutput; \ - diff -u misc/deps/deps.out $$tmpoutput 2>&1; R=$$?; times; \ - $(coqc) -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1; \ - $(coqc) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \ - $(coqtop) -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1; \ - S=$$?; times; \ - if [ $$R = 0 -a $$S = 0 ]; then \ - echo $(log_success); \ - echo " misc/deps-order...Ok"; \ - else \ - echo $(log_failure); \ - echo " misc/deps-order...Error! (unexpected order)"; \ - fi; \ - rm $$tmpoutput; \ - } > "$@" - -deps-checksum: misc/deps-checksum.log -misc/deps-checksum.log: - @echo "TEST misc/deps-checksum" - $(HIDE){ \ - echo $(call log_intro,deps-checksum); \ - rm -f misc/deps/*/*.vo; \ - $(coqc) -R misc/deps/A A misc/deps/A/A.v; \ - $(coqc) -R misc/deps/B A misc/deps/B/A.v; \ - $(coqc) -R misc/deps/B A misc/deps/B/B.v; \ - $(coqtop) -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v 2>&1; \ - if [ $$? = 0 ]; then \ - echo $(log_success); \ - echo " misc/deps-checksum...Ok"; \ - else \ - echo $(log_failure); \ - echo " misc/deps-checksum...Error!"; \ - fi; \ - } > "$@" - +misc: $(patsubst %.sh,%.log,$(wildcard misc/*.sh)) -# Sort universes for the whole standard library -EXPECTED_UNIVERSES := 4 # Prop is not counted -universes: misc/universes.log -misc/universes.log: misc/universes/all_stdlib.v - @echo "TEST misc/universes" - $(HIDE){ \ - $(coqc) -R misc/universes Universes misc/universes/all_stdlib 2>&1; \ - $(coqc) -R misc/universes Universes misc/universes/universes 2>&1; \ - mv universes.txt misc/universes; \ - N=`awk '{print $$3}' misc/universes/universes.txt | sort -u | wc -l`; \ - times; \ - if [ "$$N" -eq $(EXPECTED_UNIVERSES) ]; then \ - echo $(log_success); \ - echo " misc/universes...Ok ($(EXPECTED_UNIVERSES) universes)"; \ - else \ - echo $(log_failure); \ - echo " misc/universes...Error! ($$N/$(EXPECTED_UNIVERSES) universes)"; \ - fi; \ - } > "$@" - -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" +$(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) + @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqc) misc/exitstatus/illtyped.v 2>&1; R=$$?; times; \ - if [ $$R != 0 ]; then \ + export coqc="$(coqc)"; \ + export coqtop="$(coqtop)"; \ + export coqdep="$(coqdep)"; \ + export coqtopbyte="$(coqtopbyte)"; \ + "$<" 2>&1; R=$$?; times; \ + if [ $$R = 0 ]; then \ echo $(log_success); \ - echo " misc/exitstatus...Ok"; \ + echo " $<...Ok"; \ else \ echo $(log_failure); \ - echo " misc/exitstatus...Error!"; \ + echo " $<...Error!"; \ fi; \ } > "$@" diff --git a/test-suite/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh new file mode 100755 index 000000000..1e2afb754 --- /dev/null +++ b/test-suite/misc/deps-checksum.sh @@ -0,0 +1,5 @@ +rm -f misc/deps/*/*.vo +$coqc -R misc/deps/A A misc/deps/A/A.v +$coqc -R misc/deps/B A misc/deps/B/A.v +$coqc -R misc/deps/B A misc/deps/B/B.v +$coqtop -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh new file mode 100755 index 000000000..375b706f0 --- /dev/null +++ b/test-suite/misc/deps-order.sh @@ -0,0 +1,20 @@ +# Check that both coqdep and coqtop/coqc supports -R +# Check that both coqdep and coqtop/coqc takes the later -R +# See bugs 2242, 2337, 2339 +rm -f misc/deps/*/*.vo +tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` +$coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > $tmpoutput +diff -u misc/deps/deps.out $tmpoutput 2>&1 +R=$? +times +$coqc -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1 +$coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1 +$coqtop -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1 +S=$? +if [ $R = 0 -a $S = 0 ]; then + printf "coqdep and coqtop agree\n" + exit 0 +else + printf "coqdep and coqtop disagree\n" + exit 1 +fi diff --git a/test-suite/misc/exitstatus.sh b/test-suite/misc/exitstatus.sh new file mode 100755 index 000000000..cea1de862 --- /dev/null +++ b/test-suite/misc/exitstatus.sh @@ -0,0 +1,7 @@ +$coqtop -load-vernac-source misc/exitstatus/illtyped.v +N=$? +$coqc misc/exitstatus/illtyped.v +P=$? +printf "On ill-typed input, coqtop returned $N.\n" +printf "On ill-typed input, coqc returned $P.\n" +if [ $N = 1 -a $P = 1 ]; then exit 0; else exit 1; fi diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh new file mode 100755 index 000000000..c822d0eb3 --- /dev/null +++ b/test-suite/misc/printers.sh @@ -0,0 +1,3 @@ +printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep Unbound +if [ $? = 0 ]; then exit 1; else exit 0; fi + diff --git a/test-suite/misc/universes.sh b/test-suite/misc/universes.sh new file mode 100755 index 000000000..d87a86035 --- /dev/null +++ b/test-suite/misc/universes.sh @@ -0,0 +1,8 @@ +# Sort universes for the whole standard library +EXPECTED_UNIVERSES=4 # Prop is not counted +$coqc -R misc/universes Universes misc/universes/all_stdlib 2>&1 +$coqc -R misc/universes Universes misc/universes/universes 2>&1 +mv universes.txt misc/universes +N=`awk '{print $3}' misc/universes/universes.txt | sort -u | wc -l` +printf "Found %s/%s universes\n" $N $EXPECTED_UNIVERSES +if [ "$N" -eq $EXPECTED_UNIVERSES ]; then exit 0; else exit 1; fi |