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