From: Stefano Zacchiroli Date: Wed, 5 Dec 2007 15:26:53 +0000 (+0000) Subject: dump result table in \TeX format X-Git-Tag: make_still_working~5725 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=71c784aa955e97b1adacde508a9bd764bf6a7a31;p=helm.git dump result table in \TeX format --- diff --git a/helm/software/matita/bench_summary.py b/helm/software/matita/bench_summary.py index d16f9a25d..080972ec5 100755 --- 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'