# HG changeset patch
# User krauss
# Date 1303804217 -7200
# Node ID 8a33a5596ba89ffaa578e595926c6942bcab9891
# Parent  593289343c7d6d0e7d1420ba1aa1cf0c0c6123c1
mutabelle reports: parse results out of log file

diff -r 593289343c7d -r 8a33a5596ba8 Admin/mira.py
--- a/Admin/mira.py	Sat Apr 23 19:41:53 2011 +0200
+++ b/Admin/mira.py	Tue Apr 26 09:50:17 2011 +0200
@@ -265,8 +265,12 @@
     except IOError:
         mutabelle_log = ''
 
+    mutabelle_data = dict(
+        (tool, {'counterexample': c, 'no_counterexample': n, 'timeout': t, 'error': e})
+        for tool, c, n, t, e in re.findall(r'(\S+)\s+: C: (\d+) N: (\d+) T: (\d+) E: (\d+)', log))
+
     return (return_code == 0 and mutabelle_log != '', extract_isabelle_run_summary(log),
-      {'timing': extract_isabelle_run_timing(log)},
+      {'mutabelle_results': {theory: mutabelle_data}},
       {'log': log, 'mutabelle_log': mutabelle_log}, None)
 
 @configuration(repos = [Isabelle], deps = [(HOL, [0])])