# HG changeset patch
# User bulwahn
# Date 1301645900 -7200
# Node ID b065186597e3e0043aaff29ae7e28c33e0af1a4f
# Parent  f6bc441fbf19e95827fe53072a87af1c5fbdc3d7# Parent  b4f4ed5b8586ab6c71e271e9def236c2dcaf3279
merged

diff -r f6bc441fbf19 -r b065186597e3 Admin/mira.py
--- a/Admin/mira.py	Fri Apr 01 09:20:59 2011 +0200
+++ b/Admin/mira.py	Fri Apr 01 10:18:20 2011 +0200
@@ -63,10 +63,10 @@
     def to_secs(h, m, s):
         return (int(h) * 60 + int(m)) * 60 + int(s)
     pat = r'Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time'
-    pat2 = r'Timing (\S+) \((\d+) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time\)'
+    pat2 = r'Timing (\S+) \((\d+) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time, factor (\d+\.\d+)\)'
     t = dict((name, {'elapsed': to_secs(eh,em,es), 'cpu': to_secs(ch,cm,cs)})
              for name, eh, em, es, ch, cm, cs in re.findall(pat, logdata))
-    for name, threads, elapsed, cpu, gc in re.findall(pat2, logdata):
+    for name, threads, elapsed, cpu, gc, factor in re.findall(pat2, logdata):
 
         if name not in t:
             t[name] = {}
@@ -75,6 +75,7 @@
         t[name]['elapsed_inner'] = elapsed
         t[name]['cpu_inner'] = cpu
         t[name]['gc'] = gc
+        t[name]['factor'] = factor
 
     return t
 
diff -r f6bc441fbf19 -r b065186597e3 src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Apr 01 09:20:59 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Apr 01 10:18:20 2011 +0200
@@ -159,7 +159,7 @@
 by (rule Rep_Nat_inverse)
 
 lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
-nitpick [card = 1, unary_ints, max_potential = 0, timeout = 120, expect = none]
+nitpick [card = 1, unary_ints, max_potential = 0, timeout = 240, expect = none]
 by (rule Zero_int_def_raw)
 
 lemma "Abs_list (Rep_list a) = a"
diff -r f6bc441fbf19 -r b065186597e3 src/HOL/Predicate_Compile_Examples/Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Fri Apr 01 09:20:59 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Fri Apr 01 10:18:20 2011 +0200
@@ -2,6 +2,8 @@
 imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
 begin
 
+declare [[values_timeout = 240.0]]
+
 section {* Formal Languages *}
 
 subsection {* General Context Free Grammars *}
diff -r f6bc441fbf19 -r b065186597e3 src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Fri Apr 01 09:20:59 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Fri Apr 01 10:18:20 2011 +0200
@@ -2,7 +2,7 @@
 imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
 begin
 
-declare [[values_timeout = 240.0]]
+declare [[values_timeout = 480.0]]
 
 section {* Specialisation Examples *}