helm/software/matita/bench_disamberrors

   1 #!/bin/bash
   2 TEMP=`getopt -o c:d:m: -- "$@"`
   3 libdir="`pwd`/library"
   4 matitac="`pwd`/matitac.opt"
   5 devel="library"
   6 matitadep="./matitadep.opt"
   7 eval set -- "$TEMP"
   8 while true ; do
   9   case "$1" in
  10     -d) libdir="$2"; shift 2 ;;
  11     -c) matitac="$2"; shift 2 ;;
  12     --) shift; break ;;
  13      *) echo "Usage: errors_bench [-c MATITAC_PATH] [-d LIBRARY_DIR] [-m MATITAMAKE_DEVEL]"; exit 1 ;;
  14   esac
  15 done
  16 if ! [ -d "$libdir" ] ; then
  17   echo "Can't find library directory '$libdir'"
  18   exit 2
  19 fi
  20 if ! [ -x "$matitac" ] ; then
  21   echo "Can't find executable Matita compiler '$matitac'"
  22   exit 2
  23 fi
  24
  25 ma_s=$(find $libdir -name "*.ma" -type f)
  26 sorted_ma_s=$($matitadep -order $ma_s)
  27
  28 log="bench_disamberrors.txt"
  29 rm -f "$log"
  30 echo -e "# FILENAME\tOUTCOME\tEXPECTED_ERROR\tERRORS\tSPURIOUS_ERRORS" > $log
  31 # format: tab-separated fields:
  32 #   FILENAME OUTCOME EXPECTED_ERROR ERRORS SPURIOUS_ERRORS
  33 # field descriptions:
  34 #   OUTCOME is one of {"OK","KO","UNKNOWN(n)"}, n is an exit code
  35 #   EXPECTED_ERROR is FROM-TO, where FROM and TO are character counts
  36 #   ERRORS, same format as above (FROM-TO)
  37 #   SPURIOUS_ERRORS, same format as above (FROM-TO)
  38 log_outcome ()
  39 {
  40   echo -e "$1\t$2\t$3\t$4\t$5" >> "$log"
  41 }
  42
  43 sorted_ma_s="datatypes/compare.ma logic/connectives.ma higher_order_defs/relations.ma"
  44 for ma in $sorted_ma_s ; do
  45   mo=`echo $ma | sed 's/\.ma$/.mo/'`
  46   make -C $libdir $mo # ensure deps for $mo have been built
  47   rotten_mas=$(ls $libdir/$ma.*.rottened)
  48   for rotten_ma in $rotten_mas ; do
  49     rotten_ma=$(echo $rotten_ma | sed s@^$(pwd)/@@)  # prettier names
  50     echo "$rotten_ma ..."
  51     tmp="bench_disamberrors.tmp"
  52     $matitac $rotten_ma &> $tmp
  53     outcome=$?
  54     if [ "$outcome" = 3 ] ; then
  55       outcome="KO"
  56     elif [ "$outcome" = 0 ] ; then
  57       outcome="OK"
  58     else
  59       outcome="UNKNOWN($outcome)"
  60     fi
  61     supposed_error=$(grep ^error-at: $rotten_ma | cut -f 2 -d' ')
  62     raw_errors=$(grep '^*Error at' $tmp | sed 's/:.*$//' | cut -f 3 -d' ')
  63     errors=""
  64     for e in $raw_errors ; do
  65       if ! [ -z "$errors" ] ; then errors="$errors," ; fi
  66       errors="$errors$e"
  67     done
  68     raw_spurious_errors=$(grep '^*(Spurious?) Error at' $tmp | sed 's/:.*$//' | cut -f 4 -d' ')
  69     spurious_errors=""
  70     for e in $raw_spurious_errors ; do
  71       if ! [ -z "$spurious_errors" ] ; then spurious_errors="$spurious_errors," ; fi
  72       spurious_errors="$spurious_errors$e"
  73     done
  74     log_outcome $rotten_ma $outcome $supposed_error $errors $spurious_errors
  75   done
  76 done
  77
  78 echo "See $log for benchmark results"