Only errors from passes 4 and 6 are kept.

diff --git a/helm/software/matita/bench_disamberrors b/helm/software/matita/bench_disamberrors
index 2ff61fe3673c3226a46444b5cf114dda93a21ed3..aaad052c7924b5c66b5d0b7147f47bcc853e9e88 100755 (executable)
--- a/helm/software/matita/bench_disamberrors
+++ b/helm/software/matita/bench_disamberrors
@@ -1,4 +1,5 @@
 #!/bin/bash
+#set -x
 TEMP=`getopt -o c:d:m: -- "$@"`
 libdir="`pwd`/library"
 matitac="`pwd`/matitac.opt"
@@ -38,7 +39,7 @@ echo -e "# FILENAME\tOUTCOME\tEXPECTED_ERROR\tERRORS\tSPURIOUS_ERRORS" > $log
 #   SPURIOUS_ERRORS, same format as above (FROM-TO)
 log_outcome ()
 {
-  echo -e "$1\t$2\t$3\t$4\t$5" >> "$log"
+  echo -e "$1|$2|$3|$4|$5" >> "$log"
 }
 
 for ma in $sorted_ma_s ; do
@@ -59,18 +60,25 @@ for ma in $sorted_ma_s ; do
       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
+    error_pass=""
+    error_loc=""
+    while read e ; do
+      if echo "$e" | grep -q "Error at" && [ -n "$error_pass" ] ; then
+        # this is an error location line
+        if echo "$e" | grep -q "Spurious" ; then
+          loc=$(echo "$e" | sed 's/:.*$//' | cut -f 4 -d ' ')
+          if ! [ -z "$spurious_errors" ] ; then spurious_errors="$spurious_errors," ; fi
+          spurious_errors="$spurious_errors$loc"
+        else
+          loc=$(echo "$e" | sed 's/:.*$//' | cut -f 3 -d ' ')
+          if ! [ -z "$errors" ] ; then errors="$errors," ; fi
+          errors="$errors$loc"
+        fi
+      fi
+      error_pass=$(echo "$e" | grep "during phases " | sed 's/:.*$//' | cut -f 6 -d' ' | grep "4\|6")
+    done < $tmp
     log_outcome $rotten_ma $outcome $supposed_error $errors $spurious_errors
   done
 done