From bd1b7790419099bf311039f2ab6abff35e08f8d3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 2 Nov 2005 07:10:11 +0000
Subject: Ajout tests interactifs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7489 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/check | 25 ++++++++++++++++++++++++-
 1 file changed, 24 insertions(+), 1 deletion(-)

diff --git a/test-suite/check b/test-suite/check
index df41fff6e1..d8f7960003 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -11,7 +11,13 @@ fi
 if [ "$1" = -byte ]; then
   command="../bin/coqtop.byte -no-vm -q -batch -load-vernac-source"
 else
-  command="../bin/coqtop -q -batch -load-vernac-source"
+  command="../bin/coqtop -no-vm -q -batch -load-vernac-source"
+fi
+
+if [ "$1" = -byte ]; then
+  coqtop="../bin/coqtop.byte -no-vm -q -batch"
+else
+  coqtop="../bin/coqtop -no-vm -q -batch"
 fi
 
 # on compte le nombre de tests et de succès
@@ -128,6 +134,21 @@ test_parser() {
     fi
 }
 
+# La fonction suivante teste en interactif 
+test_interactive() {
+    for f in $1/*.v; do 
+	nbtests=`expr $nbtests + 1`
+	printf "    "$f"..."
+	$coqtop < $f > /dev/null 2>&1
+	if [ $? = 0 ]; then 
+	    echo "Ok"
+	    nbtestsok=`expr $nbtestsok + 1`
+        else 
+	    echo "Error! (should be accepted)"
+        fi 
+    done
+}
+
 # Programme principal
 
 echo "Output tests"
@@ -138,6 +159,8 @@ echo "Failure tests"
 test_failure failure
 echo "Parser tests"
 test_parser parser
+echo "Interactive tests"
+test_interactive interactive
 pourcentage=`expr 100 \* $nbtestsok / $nbtests`
 echo
 echo "$nbtestsok tests passed over $nbtests, i.e. $pourcentage %"
-- 
cgit v1.2.3