helm/matita/scripts/do_tests.sh

   1 #!/bin/bash
   2
   3 OK="\e[32mOK\e[0m"
   4 FAIL="\e[31mFAIL\e[0m"
   5
   6 if [ "$1" = "-no-color" ]; then
   7   shift
   8   OK="OK"
   9   FAIL="FAIL"
  10 fi
  11 if [ "$1" = "-twice" ]; then
  12   shift
  13   TWICE=1
  14 fi
  15
  16 COMPILER=$1
  17 shift
  18 CLEANCOMPILER=`echo $COMPILER | cut -d ' ' -f 1`
  19 CLEANER=$1
  20 shift
  21 LOGFILE=$1
  22 shift
  23 EXPECTED=$1
  24 shift
  25 TODO="$@"
  26
  27 if [ -z "$COMPILER" -o -z "$CLEANER" -o -z "$LOGFILE" -o -z "$EXPECTED" -o -z "$TODO" ]; then
  28   echo
  29   echo "usage: "
  30   echo "  do_tests.sh [-no-color] [-twice] ./compiler ./cleaner logfile expected_result test.ma ..."
  31   echo
  32   echo "options:  "
  33   echo "  -no-color Do not use vt100 colors"
  34   echo "  -twice    Run each test twice but show only the second run times"
  35   echo
  36   echo "If expected_result is OK the result will be OK if the test compiles."
  37   echo "Otherwise if expected_result is FAIL the result will be OK if the test"
  38   echo "does not compile and the generated output is equal to test.log."
  39   echo "The value of the DO_TESTS_EXTRA evironment variable"
  40   echo "will be appended to each line."
  41   exit 1
  42 fi
  43
  44
  45 export TIMEFORMAT="%2lR %2lU %2lS"
  46 for T in $TODO; do
  47   TT=`echo $T | sed s?/?.?`
  48   LOG=__log_$TT
  49   DIFF=__diff_$TT
  50   printf "$CLEANCOMPILER\t%-30s   " $T
  51   if [ "$TWICE" = "1" ]; then
  52     $CLEANER $T 1>/dev/null 2>/dev/null
  53     $COMPILER $T 1>/dev/null 2>/dev/null
  54   fi
  55   $CLEANER $T 1>/dev/null 2>/dev/null
  56   TIMES=`(time $COMPILER $T > $LOG 2>&1) 2>&1`
  57   RC=$?;
  58   cat $LOG >> $LOGFILE
  59   touch $DIFF
  60   if [ $EXPECTED = "FAIL" ]; then
  61    if [ $RC = 0 ]; then
  62      echo "The test was successful but it should have failed!" > $DIFF
  63      RC=1;
  64    else
  65      diff $LOG `basename $T .ma`.log > $DIFF
  66      RC=$?
  67    fi
  68   fi
  69   if [ $RC = 0 ]; then
  70     printf "$OK\t$TIMES\t$DO_TESTS_EXTRA\n"
  71   else
  72     printf "$FAIL\t$TIMES\t$DO_TESTS_EXTRA\n";
  73     cat $DIFF
  74   fi
  75   #rm -f $LOG
  76   #rm -f $DIFF
  77   exit $RC
  78 done