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 LOG=.__log
  45 DIFF=.__diff
  46
  47 export TIMEFORMAT="%2lR %2lU %2lS"
  48 for T in $TODO; do
  49   printf "$CLEANCOMPILER\t%-30s   " $T
  50   if [ "$TWICE" = "1" ]; then
  51     $CLEANER $T 1>/dev/null 2>/dev/null
  52     $COMPILER $T 1>/dev/null 2>/dev/null
  53   fi
  54   $CLEANER $T 1>/dev/null 2>/dev/null
  55   TIMES=`(time $COMPILER $T > $LOG 2>&1) 2>&1`
  56   RC=$?;
  57   cat $LOG >> $LOGFILE
  58   touch $DIFF
  59   if [ $EXPECTED = "FAIL" ]; then
  60    if [ $RC = 0 ]; then
  61      echo "The test was successful but it should have failed!" > $DIFF
  62      RC=1;
  63    else
  64      diff $LOG `basename $T .ma`.log > $DIFF
  65      RC=$?
  66      rm -f $LOG
  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 $DIFF
  76   exit $RC
  77 done