--- 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
--- 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"
--- 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 *}
--- 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 *}