Use the Makefile in test-suite/check

The output format is preserved, but not the dynamics (results are
showed all at once at the end).  This script could be removed
altogether once the main Makefile (and daily bench) are fixed.

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

1 files changed, 5 insertions, 278 deletions

diff --git a/test-suite/check b/test-suite/check
index 1206e16b5..48a674490 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -1,284 +1,11 @@
 #!/bin/sh
 
-# Automatic test of Coq
+MAKE="${MAKE:=make}"
 
 if [ "$1" = -byte ]; then
-  coqtop="../bin/coqtop.byte -boot -q -batch -I prerequisite"
-  bincoqc="../bin/coqc -byte -I prerequisite"
-else
-  coqtop="../bin/coqtop -boot -q -batch -I prerequisite"
-  bincoqc="../bin/coqc -I prerequisite"
+  export BEST=byte
 fi
 
-command="$coqtop -top Top -load-vernac-source"
-coqc="$coqtop -compile"
-
-# 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_success() {
-    for f in $1/*.v; do 
-	nbtests=`expr $nbtests + 1`
-	printf "    "$f"..."
-	$command $f $2 > /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_failure() {
-    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
-}
-
-# La fonction suivante teste la sortie des fichiers qu'elle exécute 
-test_output() {
-    for f in $1/*.v; do 
-	nbtests=`expr $nbtests + 1`
-	printf "    "$f"..."
-        tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
-	$command $f 2>&1 | grep -v "Welcome to Coq" | grep -v "Skipping rcfile loading" > $tmpoutput
-        foutput=`dirname $f`/`basename $f .v`.out
-        diff $tmpoutput $foutput > /dev/null 2>&1
-	if [ $? = 0 ]; then 
-	    echo "Ok"
-	    nbtestsok=`expr $nbtestsok + 1`
-        else 
-	    echo "Error! (unexpected output)"
-        fi 
-        rm $tmpoutput
-    done
-}
-
-# 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
-}
-
-# La fonction suivante teste en interactif 
-# It expects a line "(* Expected time < XXX.YYs *)" in the .v file 
-# with exactly two digits after the dot
-# The reference for time is a 6120 bogomips cpu
-test_complexity() {
-    if [ -f /proc/cpuinfo ]; then
-	if grep -q bogomips /proc/cpuinfo; then # i386, ppc
-	    bogomips=`sed -n -e "s/bogomips.*: \([0-9]*\).*/\1/p" /proc/cpuinfo | head -1`
-	elif grep -q Cpu0Bogo /proc/cpuinfo; then # sparc
-	    bogomips=`sed -n -e "s/Cpu0Bogo.*: \([0-9]*\).*/\1/p" /proc/cpuinfo | head -1`
-	elif grep -q BogoMIPS /proc/cpuinfo; then # alpha
-	    bogomips=`sed -n -e "s/BogoMIPS.*: \([0-9]*\).*/\1/p" /proc/cpuinfo | head -1`
-	fi
-    fi
-    if [ "$bogomips" = "" ]; then
-	echo "    cannot run complexity tests (no bogomips found)"
-    else
-      for f in $1/*.v; do 
-        nbtests=`expr $nbtests + 1`
-        printf "    "$f"..."
-        # extract effective user time
-        res=`$command $f 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`
-        if [ $? != 0 ]; then
-	  echo "Error! (should be accepted)"
-        elif [ "$res" = "" ]; then
-          echo "Error! (couldn't find a time measure)"
-        else
-          # express effective time in centiseconds
-          res=`echo "$res"00 | sed -n -e "s/\([0-9]*\)\.\([0-9][0-9]\).*/\1\2/p"`
-          # find expected time * 100
-          exp=`sed -n -e "s/(\*.*Expected time < \([0-9]\).\([0-9][0-9]\)s.*\*)/\1\2/p" $f`
-          ok=`expr \( $res \* $bogomips \) "<" \( $exp \* 6120 \)`
-          if [ "$ok" = 1 ]; then
-              echo "Ok"
-              nbtestsok=`expr $nbtestsok + 1`
-          else
-              echo "Error! (should run faster)"
-          fi
-        fi
-      done
-    fi
-}
-
-test_bugs () {
-    # Process verifications concerning submitted bugs. A message is
-    # printed for all opened bugs (still active or seems to be closed).
-    # For closed bugs that behave as expected, no message is printed
-
-    # All files are assumed to have <# of the bug>.v as a name
-
-    echo "Testing opened bugs..."
-    # We first test opened bugs that should not succeed
-    files=`/bin/ls -1 $1/opened/shouldnotsucceed/*.v 2> /dev/null`
-    for f in $files; do 
-	nbtests=`expr $nbtests + 1`
-	printf "    "$f"..."
-	$command $f $2 > /dev/null 2>&1 
-	if [ $? = 0 ]; then
-	    echo "still active"
-	    nbtestsok=`expr $nbtestsok + 1`
-        else 
-	    echo "Error! (bug seems to be closed, please check)"
-        fi 
-    done
-
-    # And opened bugs that should not fail
-    files=`/bin/ls -1 $1/opened/shouldnotfail/*.v 2> /dev/null`
-    for f in $files; do 
-	nbtests=`expr $nbtests + 1`
-	printf "    "$f"..."
-	$command $f > /dev/null 2>&1
-	if [ $? != 0 ]; then 
-	    echo "still active"
-	    nbtestsok=`expr $nbtestsok + 1`
-        else 
-	    echo "Error! (bug seems to be closed, please check)"
-        fi 
-    done
-
-    echo "Testing closed bugs..."
-    # Then closed bugs that should succeed
-    files=`/bin/ls -1 $1/closed/shouldsucceed/*.v 2> /dev/null`
-    for f in $files; do 
-	nbtests=`expr $nbtests + 1`
-	printf "    "$f"..."
-	$command $f $2 > /dev/null 2>&1 
-	if [ $? = 0 ]; then
-	    echo "Ok"
-	    nbtestsok=`expr $nbtestsok + 1`
-        else 
-	    echo "Error! (bug seems to be opened, please check)"
-        fi 
-    done
-
-
-    # At last, we test closed bugs that should fail
-    files=`/bin/ls -1 $1/closed/shouldfail/*.v 2> /dev/null`
-    for f in $files; 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! (bug seems to be opened, please check)"
-        fi 
-    done
-    
-}
-
-test_features () {
-    # Process verifications concerning submitted bugs. A message is
-    # printed for all opened bugs (still active or seem to be closed.
-    # For closed bugs that behave as expected, no message is printed
-
-    echo "Testing wishes..."
-    files=`/bin/ls -1 $1/*.v 2> /dev/null`
-    for f in $files; do 
-	nbtests=`expr $nbtests + 1`
-	printf "    "$f"..."
-	$command $f $2 > /dev/null 2>&1 
-	if [ $? != 0 ]; then
-	    echo "still wished"
-	    nbtestsok=`expr $nbtestsok + 1`
-        else 
-	    echo "Good news! (wish seems to be granted, please check)"
-        fi
-    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
-}
-
-test_misc () {
-    # Non-standard features
-
-    # Test xml compilation
-    nbtests=`expr $nbtests + 1`
-    printf "    xml..."
-    COQ_XML_LIBRARY_ROOT=misc/xml $bincoqc -xml misc/berardi_test > /dev/null 2>&1
-    if [ ! -d misc/xml ]; then
-        printf "failed\n"
-    else
-        printf "apparently ok\n"
-	nbtestsok=`expr $nbtestsok + 1`
-        rm -r misc/xml
-    fi
-}
-
-# Programme principal
-
-echo "Preparing tests"
-prepare_tests prerequisite
-echo "Success tests"
-test_success success
-echo "Failure tests"
-test_failure failure
-echo "Bugs tests"
-test_bugs bugs
-echo "Output tests"
-test_output output
-echo "Interactive tests"
-test_interactive interactive
-echo "Micromega tests"
-test_success micromega
-echo "Miscellaneous tests"
-test_misc
-
-# We give a chance to disable the complexity tests which may cause
-# random build failures on build farms
-if [ -z "$COQTEST_SKIPCOMPLEXITY" ]; then
-  echo "Complexity tests"
-  test_complexity complexity
-else
-  echo "Skipping complexity tests"
-fi
-
-echo "Module tests"
-$coqtop -compile modules/Nat
-$coqtop -compile modules/plik
-test_success modules "-I modules -impredicative-set"
-echo "Ideal-features tests"
-test_features ideal-features
-
-pourcentage=`expr 100 \* $nbtestsok / $nbtests`
-echo
-echo "$nbtestsok tests passed over $nbtests, i.e. $pourcentage %"
+${MAKE} clean > /dev/null 2>&1
+${MAKE} all > /dev/null 2>&1
+cat summary.log