From 4aa525b1b33e3a383ace9cff83f899d97e58fd83 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 9 Dec 2000 00:09:58 +0000
Subject: tests automatiques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1082 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile                        |  7 ++++++
 test-suite/check                | 55 +++++++++++++++++++++++++++++++++++++++++
 test-suite/failure/illtype1.v   |  1 +
 test-suite/failure/positivity.v |  1 +
 test-suite/failure/redef.v      |  2 ++
 test-suite/success/Check.v      |  7 ++++++
 6 files changed, 73 insertions(+)
 create mode 100755 test-suite/check
 create mode 100644 test-suite/failure/illtype1.v
 create mode 100644 test-suite/failure/positivity.v
 create mode 100644 test-suite/failure/redef.v
 create mode 100644 test-suite/success/Check.v

diff --git a/Makefile b/Makefile
index 0bb9c113ef..0881dbcae8 100644
--- a/Makefile
+++ b/Makefile
@@ -205,6 +205,13 @@ parsing: $(PARSING)
 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 0000000000..f415604fdd
--- /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 0000000000..3f6206c766
--- /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 0000000000..09025197c7
--- /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 0000000000..0c821906e0
--- /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 0000000000..2c9fc7ada8
--- /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.
-- 
cgit v1.2.3