From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 6 Jan 2008 23:00:55 +0000 (+0000)
Subject: cleanup
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=8cd018c9a1bfb5539b046526a9d5108cf386c5b2

cleanup
---

diff --git a/matita/bench_disamberrors b/matita/bench_disamberrors
deleted file mode 100755
index 87ece78ee..000000000
--- a/matita/bench_disamberrors
+++ /dev/null
@@ -1,90 +0,0 @@
-#!/bin/bash
-#set -x
-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 ;;
-    -m) devel="$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|$2|$3|$4|$5" >> "$log"
-}
-
-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' ')
-    errors=""
-    spurious_errors=""
-    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 ! echo "$spurious_errors" | grep -q "$loc"; then
-            if ! [ -z "$spurious_errors" ] ; then spurious_errors="$spurious_errors," ; fi
-            spurious_errors="$spurious_errors$loc"
-          fi
-        else
-          loc=$(echo "$e" | sed 's/:.*$//' | cut -f 3 -d ' ')
-          if ! echo "$errors" | grep -q "$loc"; then
-            if ! [ -z "$errors" ] ; then errors="$errors," ; fi
-            errors="$errors$loc"
-          fi
-        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
-
-echo "See $log for benchmark results"
diff --git a/matita/bench_summary.py b/matita/bench_summary.py
deleted file mode 100755
index 32df4b017..000000000
--- a/matita/bench_summary.py
+++ /dev/null
@@ -1,75 +0,0 @@
-#!/usr/bin/python
-import sys
-
-stats = {}
-stats['total'] = []
-stats['precise'] = []
-stats['imprecise'] = []
-stats['false-positives'] = []
-stats['undetected'] = []
-
-for line in open(sys.argv[1]):
-    line = line.rstrip()
-    if line[0] == '#':
-        continue
-    cols = line.split('|')
-    name = cols[0]
-    if cols[1] != 'KO':
-        print "Warning: outcome of %s is %s, skipping it" % (name, cols[1])
-        continue
-    expected_error = cols[2]
-    real_errors = cols[3].split(',')
-    spurious_errors = cols[4].split(',')
-
-    stats['total'].append((name,real_errors))
-    if set([expected_error]) == set(real_errors):
-        if expected_error in spurious_errors:
-            stats['false-positives'].append((name,real_errors))
-        else:
-            stats['precise'].append((name,real_errors))
-    elif expected_error in real_errors:
-        if expected_error in spurious_errors:
-            stats['false-positives'].append((name,real_errors))
-        else:
-            stats['imprecise'].append((name,real_errors))
-    else:
-        if expected_error in spurious_errors:
-            stats['false-positives'].append((name,real_errors))
-        else:
-            stats['undetected'].append((name,real_errors))
-
-for field in ['undetected', 'imprecise', 'false-positives']:
-    print "===================="
-    print "%s:" % field
-    for name,_ in stats[field]:
-        print "  %s" % name
-
-def average(l):
-    if not(len(l)):
-        return "N/A"
-    else:
-        return "%6.1f" % (reduce(lambda acc,x: acc+x,l,0)/float(len(l)))
-
-def mymax(l):
-    if not(len(l)):
-        return 0
-    else:
-        return max(l)
-
-def format_stat(field):
-    global stats
-    lista = stats[field]
-    errors = map(lambda x: len(x[1]),lista)
-    locations = map(lambda x: len(set(x[1])),lista)
-    return r'%-15s & %6d & %6s & %6d & %6s & %6d & %6.1f\%% \\' % \
-            (field, len(lista), average(locations),mymax(locations),
-            average(errors),mymax(errors),float(len(lista)) /
-            len(stats['total']) * 100)
-
-print "\n"
-print format_stat('precise')
-print format_stat('imprecise')
-print format_stat('false-positives')
-print format_stat('undetected')
-print r'\hline'
-print format_stat('total')
diff --git a/matita/dep2dot.rb b/matita/dep2dot.rb
deleted file mode 100755
index 813b2afeb..000000000
--- a/matita/dep2dot.rb
+++ /dev/null
@@ -1,30 +0,0 @@
-#!/usr/bin/ruby -w
-# filter converting from .depend to .dot
-# tested on .depend generated by ocamldep
-# $Id$
-
-require 'set'
-
-edges = Set.new
-$stdin.each {|line|
-  target, deps = line.split(/\s*:\s*/)
-  while deps =~ /\\\s*$/  # deal with lines continued with trailing \
-    deps.sub!(/\s*\\\s*$/, '')
-    line = $stdin.readline
-    deps += ' ' + line.lstrip
-  end
-  sources, targets = target.split, deps.split
-  for src in sources
-    for tgt in targets	# ignore file extensions
-      src.sub!(/\.[^.]+/, '')
-      tgt.sub!(/\.[^.]+/, '')
-      edges << [src, tgt] unless src == tgt   # ignore self deps
-    end
-  end
-}
-puts 'digraph G {'
-for src, tgt in edges
-  print "\"#{src}\" -> \"#{tgt}\";\n"
-end
-puts '}'
-
diff --git a/matita/rottenize_lib b/matita/rottenize_lib
deleted file mode 100755
index da4667566..000000000
--- a/matita/rottenize_lib
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/bin/bash
-set -x
-make clean-rottened
-./rottener.opt -r library/