From 4aa525b1b33e3a383ace9cff83f899d97e58fd83 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
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
---
 test-suite/check | 55 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 55 insertions(+)
 create mode 100755 test-suite/check

(limited to 'test-suite/check')

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 %"
+
+
+
-- 
cgit v1.2.3