diff options
| -rw-r--r-- | Makefile | 7 | ||||
| -rwxr-xr-x | test-suite/check | 55 | ||||
| -rw-r--r-- | test-suite/failure/illtype1.v | 1 | ||||
| -rw-r--r-- | test-suite/failure/positivity.v | 1 | ||||
| -rw-r--r-- | test-suite/failure/redef.v | 2 | ||||
| -rw-r--r-- | test-suite/success/Check.v | 7 |
6 files changed, 73 insertions, 0 deletions
@@ -206,6 +206,13 @@ pretyping: $(PRETYPING) toplevel: $(TOPLEVEL) ########################################################################### +# tests +########################################################################### + +check: + cd test-suite; ./check + +########################################################################### # theories and states ########################################################################### diff --git a/test-suite/check b/test-suite/check new file mode 100755 index 000000000..f415604fd --- /dev/null +++ b/test-suite/check @@ -0,0 +1,55 @@ +#!/bin/sh + +# Automatic test of Coq + +command="../bin/coqtop.opt -q -batch -load-vernac-source" + +# on compte le nombre de tests et de succès +nbtests=0 +nbtestsok=0 + +# La fonction suivante teste le compilateur sur des fichiers qu'il doit +# accepter +test_succes() { + for f in $1/*.v; do + nbtests=`expr $nbtests + 1` + printf " "$f"..." + $command $f > /dev/null 2>&1 + if [ $? = 0 ]; then + echo "Ok" + nbtestsok=`expr $nbtestsok + 1` + else + echo "Error! (should be accepted)" + fi + done +} + +# La fonction suivante teste le compilateur sur des fichiers qu'il doit +# refuser +test_echec() { + for f in $1/*.v; do + nbtests=`expr $nbtests + 1` + printf " "$f"..." + $command $f > /dev/null 2>&1 + if [ $? != 0 ]; then + echo "Ok" + nbtestsok=`expr $nbtestsok + 1` + else + echo "Error! (should be rejected)" + fi + done +} + +# Programme principal + +echo "Success tests" +test_succes success +echo "Failure tests" +test_echec failure + +pourcentage=`expr 100 \* $nbtestsok / $nbtests` +echo +echo "$nbtestsok tests passed over $nbtests, i.e. $pourcentage %" + + + diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v new file mode 100644 index 000000000..3f6206c76 --- /dev/null +++ b/test-suite/failure/illtype1.v @@ -0,0 +1 @@ +Check (S S). diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v new file mode 100644 index 000000000..09025197c --- /dev/null +++ b/test-suite/failure/positivity.v @@ -0,0 +1 @@ +Inductive t:Set := c: (t -> nat) -> t. diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v new file mode 100644 index 000000000..0c821906e --- /dev/null +++ b/test-suite/failure/redef.v @@ -0,0 +1,2 @@ +Definition toto := Set. +Definition toto := Set. diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v new file mode 100644 index 000000000..2c9fc7ada --- /dev/null +++ b/test-suite/success/Check.v @@ -0,0 +1,7 @@ +(* Compiling the theories allows to test parsing and typing but not printing *) +(* This file tests that pretty-printing does not fail *) +(* Test of exact output is not specified *) + +Check O. +Check S. +Check nat. |