(hackish) scripts for testing spurious disambiguation error criteria

diff --git a/helm/software/matita/bench_disamberrors b/helm/software/matita/bench_disamberrors
new file mode 100755 (executable)
index 0000000..8a5f071
--- /dev/null
+++ b/helm/software/matita/bench_disamberrors
@@ -0,0 +1,78 @@
+#!/bin/bash
+TEMP=`getopt -o c:d:m: -- "$@"`
+libdir="`pwd`/library"
+matitac="`pwd`/matitac.opt"
+devel="library"
+matitadep="./matitadep.opt"
+eval set -- "$TEMP"
+while true ; do
+  case "$1" in
+    -d) libdir="$2"; shift 2 ;;
+    -c) matitac="$2"; shift 2 ;;
+    --) shift; break ;;
+     *) echo "Usage: errors_bench [-c MATITAC_PATH] [-d LIBRARY_DIR] [-m MATITAMAKE_DEVEL]"; exit 1 ;;
+  esac
+done
+if ! [ -d "$libdir" ] ; then
+  echo "Can't find library directory '$libdir'"
+  exit 2
+fi
+if ! [ -x "$matitac" ] ; then
+  echo "Can't find executable Matita compiler '$matitac'"
+  exit 2
+fi
+
+ma_s=$(find $libdir -name "*.ma" -type f)
+sorted_ma_s=$($matitadep -order $ma_s)
+
+log="bench_disamberrors.txt"
+rm -f "$log"
+echo -e "# FILENAME\tOUTCOME\tEXPECTED_ERROR\tERRORS\tSPURIOUS_ERRORS" > $log
+# format: tab-separated fields:
+#   FILENAME OUTCOME EXPECTED_ERROR ERRORS SPURIOUS_ERRORS
+# field descriptions:
+#   OUTCOME is one of {"OK","KO","UNKNOWN(n)"}, n is an exit code
+#   EXPECTED_ERROR is FROM-TO, where FROM and TO are character counts
+#   ERRORS, same format as above (FROM-TO)
+#   SPURIOUS_ERRORS, same format as above (FROM-TO)
+log_outcome ()
+{
+  echo -e "$1\t$2\t$3\t$4\t$5" >> "$log"
+}
+
+sorted_ma_s="datatypes/compare.ma logic/connectives.ma higher_order_defs/relations.ma"
+for ma in $sorted_ma_s ; do
+  mo=`echo $ma | sed 's/\.ma$/.mo/'`
+  make -C $libdir $mo # ensure deps for $mo have been built
+  rotten_mas=$(ls $libdir/$ma.*.rottened)
+  for rotten_ma in $rotten_mas ; do
+    rotten_ma=$(echo $rotten_ma | sed s@^$(pwd)/@@)  # prettier names
+    echo "$rotten_ma ..."
+    tmp="bench_disamberrors.tmp"
+    $matitac $rotten_ma &> $tmp
+    outcome=$?
+    if [ "$outcome" = 3 ] ; then
+      outcome="KO"
+    elif [ "$outcome" = 0 ] ; then
+      outcome="OK"
+    else
+      outcome="UNKNOWN($outcome)"
+    fi
+    supposed_error=$(grep ^error-at: $rotten_ma | cut -f 2 -d' ')
+    raw_errors=$(grep '^*Error at' $tmp | sed 's/:.*$//' | cut -f 3 -d' ')
+    errors=""
+    for e in $raw_errors ; do
+      if ! [ -z "$errors" ] ; then errors="$errors," ; fi
+      errors="$errors$e"
+    done
+    raw_spurious_errors=$(grep '^*(Spurious?) Error at' $tmp | sed 's/:.*$//' | cut -f 4 -d' ')
+    spurious_errors=""
+    for e in $raw_spurious_errors ; do
+      if ! [ -z "$spurious_errors" ] ; then spurious_errors="$spurious_errors," ; fi
+      spurious_errors="$spurious_errors$e"
+    done
+    log_outcome $rotten_ma $outcome $supposed_error $errors $spurious_errors
+  done
+done
+
+echo "See $log for benchmark results"

diff --git a/helm/software/matita/rottenize_lib b/helm/software/matita/rottenize_lib
new file mode 100755 (executable)
index 0000000..da46675
--- /dev/null
+++ b/helm/software/matita/rottenize_lib
@@ -0,0 +1,4 @@
+#!/bin/bash
+set -x
+make clean-rottened
+./rottener.opt -r library/