2 TEMP=`getopt -o c:d:m: -- "$@"`
4 matitac="`pwd`/matitac.opt"
6 matitadep="./matitadep.opt"
10 -d) libdir="$2"; shift 2 ;;
11 -c) matitac="$2"; shift 2 ;;
12 -m) devel="$2"; shift 2 ;;
14 *) echo "Usage: errors_bench [-c MATITAC_PATH] [-d LIBRARY_DIR] [-m MATITAMAKE_DEVEL]"; exit 1 ;;
17 if ! [ -d "$libdir" ] ; then
18 echo "Can't find library directory '$libdir'"
21 if ! [ -x "$matitac" ] ; then
22 echo "Can't find executable Matita compiler '$matitac'"
26 ma_s=$(find $libdir -name "*.ma" -type f)
27 sorted_ma_s=$($matitadep -order $ma_s)
29 log="bench_disamberrors.txt"
31 echo -e "# FILENAME\tOUTCOME\tEXPECTED_ERROR\tERRORS\tSPURIOUS_ERRORS" > $log
32 # format: tab-separated fields:
33 # FILENAME OUTCOME EXPECTED_ERROR ERRORS SPURIOUS_ERRORS
35 # OUTCOME is one of {"OK","KO","UNKNOWN(n)"}, n is an exit code
36 # EXPECTED_ERROR is FROM-TO, where FROM and TO are character counts
37 # ERRORS, same format as above (FROM-TO)
38 # SPURIOUS_ERRORS, same format as above (FROM-TO)
41 echo -e "$1\t$2\t$3\t$4\t$5" >> "$log"
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
51 tmp="bench_disamberrors.tmp"
52 $matitac $rotten_ma &> $tmp
54 if [ "$outcome" = 3 ] ; then
56 elif [ "$outcome" = 0 ] ; then
59 outcome="UNKNOWN($outcome)"
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' ')
64 for e in $raw_errors ; do
65 if ! [ -z "$errors" ] ; then errors="$errors," ; fi
68 raw_spurious_errors=$(grep '^*(Spurious?) Error at' $tmp | sed 's/:.*$//' | cut -f 4 -d' ')
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"
74 log_outcome $rotten_ma $outcome $supposed_error $errors $spurious_errors
78 echo "See $log for benchmark results"