dump result table in \TeX format

diff --git a/helm/software/matita/bench_summary.py b/helm/software/matita/bench_summary.py
index d16f9a25d4ae869b93edbaa8bdf7294673b7a694..080972ec559b7251b60ff814f306d01779c5580f 100755 (executable)
--- a/helm/software/matita/bench_summary.py
+++ b/helm/software/matita/bench_summary.py
@@ -16,7 +16,7 @@ for line in open(sys.argv[1]):
     cols = line.split('|')
     name = cols[0]
     if cols[1] != 'KO':
-        print >> sys.stderr, "Warning: outcome is %s" % cols[1]
+        print "Warning: outcome of %s is %s, skipping it" % (name, cols[1])
         continue
     stats['total'] += 1
     expected_error = cols[2]
@@ -46,18 +46,30 @@ for field in ['undetected', 'imprecise', 'mistakes', 'half-mistakes']:
     print "%s:" % field
     for name in stats[field]:
         print "  %s" % name
+
+def get_stat(field):
+    global stats
+    return (stat, float(stat) / stats['total'] * 100)
+
+def format_stat(field):
+    global stats
+    if isinstance(stats[field], int):
+        stat = stats[field]
+    else:
+        stat = len(stats[field])
+    return r'%-15s & %6d & %6.1f\%% \\' % (field, stat,
+            float(stat) / stats['total'] * 100)
+
 print "\n"
-print 'precise:\t%3d' % len(stats['precise'])
-print 'imprecise:\t%3d' % len(stats['imprecise'])
-print 'half-mistakes:\t%3d' % len(stats['half-mistakes'])
-print 'mistakes:\t%3d' % len(stats['mistakes'])
-print 'undetected:\t%3d' % len(stats['undetected'])
-print 'TOTAL:\t\t%3d' % stats['total'], "\n"
-
-print 'average spurious errors no: ', float(stats['spurious']['tot']) / len(stats['precise'])
-
-#for field, value in stats.iteritems():
-#    if field == 'spurious':
-#        value['avg'] = float(value['tot']) / stats['precise']
-#    print "%s: %s" % (field, value)
+print format_stat('precise')
+print format_stat('imprecise')
+print format_stat('half-mistakes')
+print format_stat('mistakes')
+print format_stat('undetected')
+print r'\hline'
+print format_stat('total')
+print r'\\'
+print r'%-15s & %6.1f & \\' % ('spurious avg',
+        float(stats['spurious']['tot']) / len(stats['precise']))
+print r'\hline'