summaryrefslogtreecommitdiff
path: root/test-suite/check
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/check')
-rwxr-xr-xtest-suite/check271
1 files changed, 5 insertions, 266 deletions
diff --git a/test-suite/check b/test-suite/check
index bed86c41..48a67449 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -1,272 +1,11 @@
#!/bin/sh
-# Automatic test of Coq
+MAKE="${MAKE:=make}"
if [ "$1" = -byte ]; then
- coqtop="../bin/coqtop.byte -boot -q -batch"
-else
- coqtop="../bin/coqtop -boot -q -batch"
+ export BEST=byte
fi
-command="$coqtop -top Top -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_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 l'analyseur syntaxique fournit par "coq-parser"
-# Elle fonctionne comme test_output
-test_parser() {
- if [ -d $1 ]; then
- for f in $1/*.v; do
- nbtests=`expr $nbtests + 1`
- printf " "$f"..."
- tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
- foutput=`dirname $f`/`basename $f .v`.out
- echo "parse_file 1 \"$f\"" | ../bin/coq-parser > $tmpoutput 2>&1
- perl -ne 'if(/Starting.*Parser Loop/){$printit = 1};print if $printit' \
- $tmpoutput 2>&1 | grep -i error > /dev/null
- if [ $? = 0 ] ; then
- echo "Error! (unexpected output)"
- else
- echo "Ok"
- nbtestsok=`expr $nbtestsok + 1`
- fi
- rm $tmpoutput
- done
- 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
-}
-
-# 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/shoulnotsucceed/*.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
-}
-
-# Programme principal
-
-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 "Parser tests"
-test_parser parser
-echo "Interactive tests"
-test_interactive interactive
-echo "Micromega tests"
-test_success micromega
-
-# 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