Add new directory for pre-compilation of files needed for further tests.

Application to the test of notation import from within a section.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11652 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 17 insertions, 0 deletions

diff --git a/test-suite/check b/test-suite/check
index 47960e98d5..68a4b0e384 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -9,6 +9,7 @@ else
 fi
 
 command="$coqtop -top Top -load-vernac-source"
+coqc="$coqtop -compile"
 
 # on compte le nombre de tests et de succès
 nbtests=0
@@ -234,8 +235,24 @@ test_features () {
     done
 }
 
+# Compile in advance files needed for tests involving a "Require"
+prepare_tests () {
+    files=`/bin/ls -1 $1/*.v 2> /dev/null`
+    for f in $files; do 
+	printf "    "$f"..."
+	$coqc $1/`basename $f .v` > /dev/null 2>&1 
+	if [ $? != 0 ]; then
+	    echo "could not be prepared"
+        else 
+	    echo "correctly prepared"
+        fi
+    done
+}
+
 # Programme principal
 
+echo "Preparing tests"
+prepare_tests prerequisite
 echo "Success tests"
 test_success success
 echo "Failure tests"