From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 4 Dec 2007 14:12:14 +0000 (+0000)
Subject: Only errors from passes 4 and 6 are kept.
X-Git-Tag: make_still_working~5737
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e3e848ee1a8d171eeff3b6382131eaf5968ad05d;p=helm.git

Only errors from passes 4 and 6 are kept.
---

diff --git a/helm/software/matita/bench_disamberrors b/helm/software/matita/bench_disamberrors
index 2ff61fe36..aaad052c7 100755
--- 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