diff options
| author | herbelin | 2003-10-02 12:33:10 +0000 |
|---|---|---|
| committer | herbelin | 2003-10-02 12:33:10 +0000 |
| commit | 2a0403f5b4541d4a98cc93fce763f9b629fb15f7 (patch) | |
| tree | 836dcd9302ee9bf2d8f7adf5cf43ddb32d88013e | |
| parent | f0e992b2c538d513ea684475b58016ba1d088559 (diff) | |
Traduction des tests success et test en v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4514 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rwxr-xr-x | test-suite/check | 26 |
1 files changed, 19 insertions, 7 deletions
diff --git a/test-suite/check b/test-suite/check index 2c528eca02..aa6bef1ebc 100755 --- a/test-suite/check +++ b/test-suite/check @@ -3,6 +3,12 @@ # Automatic test of Coq if [ "$1" = -byte ]; then + command7="../bin/coqtop.byte -translate -q -batch -load-vernac-source" +else + command7="../bin/coqtop -translate -q -batch -load-vernac-source" +fi + +if [ "$1" = -byte ]; then command="../bin/coqtop.byte -q -batch -load-vernac-source" else command="../bin/coqtop -q -batch -load-vernac-source" @@ -18,12 +24,18 @@ test_succes() { 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` + $command7 $f > /dev/null 2>&1 + if [ $? = 0 ]; then + mv "$f"8 tmp8.v + $command tmp8.v > /dev/null 2>&1 + if [ $? = 0 ]; then + echo "Ok" + nbtestsok=`expr $nbtestsok + 1` + else + echo "V8 Error! (should be accepted)" + fi else - echo "Error! (should be accepted)" + echo "V7 Error! (should be accepted)" fi done } @@ -34,7 +46,7 @@ test_echec() { for f in $1/*.v; do nbtests=`expr $nbtests + 1` printf " "$f"..." - $command $f > /dev/null 2>&1 + $command7 $f > /dev/null 2>&1 if [ $? != 0 ]; then echo "Ok" nbtestsok=`expr $nbtestsok + 1` @@ -50,7 +62,7 @@ test_output() { nbtests=`expr $nbtests + 1` printf " "$f"..." tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` - $command $f | tail +3 > $tmpoutput 2>&1 + $command7 $f | tail +3 > $tmpoutput 2>&1 foutput=`dirname $f`/`basename $f .v`.out diff $tmpoutput $foutput > /dev/null if [ $? = 0 ]; then |