diff options
| -rwxr-xr-x | test-suite/check | 283 |
1 files changed, 5 insertions, 278 deletions
diff --git a/test-suite/check b/test-suite/check index 1206e16b5a..48a6744900 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 |