raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.
authorkrauss
Mon Apr 04 09:32:50 2011 +0200 (2011-04-04)
changeset 4220802513eb26eb7
parent 42207 2bda5eddadf3
child 42210 8de8c38d503b
child 42211 9e2673711c77
raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.
src/HOL/Nitpick_Examples/Core_Nits.thy
src/HOL/Nitpick_Examples/Datatype_Nits.thy
src/HOL/Nitpick_Examples/Hotel_Nits.thy
src/HOL/Nitpick_Examples/Induct_Nits.thy
src/HOL/Nitpick_Examples/Integer_Nits.thy
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Nitpick_Examples/Pattern_Nits.thy
src/HOL/Nitpick_Examples/Record_Nits.thy
src/HOL/Nitpick_Examples/Refute_Nits.thy
src/HOL/Nitpick_Examples/Special_Nits.thy
src/HOL/Nitpick_Examples/Typedef_Nits.thy
src/HOL/Predicate_Compile_Examples/Examples.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
     1.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
     1.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  begin
     1.5  
     1.6  nitpick_params [verbose, card = 1\<midarrow>6, unary_ints, max_potential = 0,
     1.7 -                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
     1.8 +                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
     1.9  
    1.10  subsection {* Curry in a Hurry *}
    1.11  
     2.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
     2.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
     2.3 @@ -12,7 +12,7 @@
     2.4  begin
     2.5  
     2.6  nitpick_params [verbose, card = 1\<midarrow>8, max_potential = 0,
     2.7 -                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
     2.8 +                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
     2.9  
    2.10  primrec rot where
    2.11  "rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
     3.1 --- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
     3.2 +++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
     3.3 @@ -13,7 +13,7 @@
     3.4  begin
     3.5  
     3.6  nitpick_params [verbose, max_potential = 0, sat_solver = MiniSat_JNI,
     3.7 -                max_threads = 1, timeout = 120]
     3.8 +                max_threads = 1, timeout = 240]
     3.9  
    3.10  typedecl guest
    3.11  typedecl key
     4.1 --- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
     4.2 +++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4  begin
     4.5  
     4.6  nitpick_params [verbose, card = 1\<midarrow>8, unary_ints,
     4.7 -                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
     4.8 +                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
     4.9  
    4.10  inductive p1 :: "nat \<Rightarrow> bool" where
    4.11  "p1 0" |
     5.1 --- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
     5.2 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
     5.3 @@ -12,7 +12,7 @@
     5.4  begin
     5.5  
     5.6  nitpick_params [verbose, card = 1\<midarrow>5, bits = 1,2,3,4,6,
     5.7 -                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
     5.8 +                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
     5.9  
    5.10  lemma "Suc x = x + 1"
    5.11  nitpick [unary_ints, expect = none]
     6.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
     6.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
     6.3 @@ -18,7 +18,7 @@
     6.4  chapter {* 3. First Steps *}
     6.5  
     6.6  nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
     6.7 -                timeout = 60]
     6.8 +                timeout = 240]
     6.9  
    6.10  subsection {* 3.1. Propositional Logic *}
    6.11  
     7.1 --- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
     7.2 +++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
     7.3 @@ -12,7 +12,7 @@
     7.4  begin
     7.5  
     7.6  nitpick_params [verbose, card = 10, max_potential = 0, sat_solver = MiniSat_JNI,
     7.7 -                max_threads = 1, timeout = 60]
     7.8 +                max_threads = 1, timeout = 240]
     7.9  
    7.10  lemma "x = (case u of () \<Rightarrow> y)"
    7.11  nitpick [expect = genuine]
     8.1 --- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
     8.2 +++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
     8.3 @@ -12,7 +12,7 @@
     8.4  begin
     8.5  
     8.6  nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
     8.7 -                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
     8.8 +                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
     8.9  
    8.10  record point2d =
    8.11    xc :: int
     9.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
     9.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
     9.3 @@ -12,7 +12,7 @@
     9.4  begin
     9.5  
     9.6  nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
     9.7 -                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
     9.8 +                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
     9.9  
    9.10  lemma "P \<and> Q"
    9.11  apply (rule conjI)
    10.1 --- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
    10.2 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
    10.3 @@ -12,7 +12,7 @@
    10.4  begin
    10.5  
    10.6  nitpick_params [verbose, card = 4, sat_solver = MiniSat_JNI, max_threads = 1,
    10.7 -                timeout = 60]
    10.8 +                timeout = 240]
    10.9  
   10.10  fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
   10.11  "f1 a b c d e = a + b + c + d + e"
    11.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sun Apr 03 11:40:32 2011 +0200
    11.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon Apr 04 09:32:50 2011 +0200
    11.3 @@ -12,7 +12,7 @@
    11.4  begin
    11.5  
    11.6  nitpick_params [verbose, card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1,
    11.7 -                timeout = 60]
    11.8 +                timeout = 240]
    11.9  
   11.10  typedef three = "{0\<Colon>nat, 1, 2}"
   11.11  by blast
   11.12 @@ -159,7 +159,7 @@
   11.13  by (rule Rep_Nat_inverse)
   11.14  
   11.15  lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
   11.16 -nitpick [card = 1, unary_ints, max_potential = 0, timeout = 240, expect = none]
   11.17 +nitpick [card = 1, unary_ints, max_potential = 0, expect = none]
   11.18  by (rule Zero_int_def_raw)
   11.19  
   11.20  lemma "Abs_list (Rep_list a) = a"
    12.1 --- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Sun Apr 03 11:40:32 2011 +0200
    12.2 +++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Mon Apr 04 09:32:50 2011 +0200
    12.3 @@ -2,7 +2,7 @@
    12.4  imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
    12.5  begin
    12.6  
    12.7 -declare [[values_timeout = 240.0]]
    12.8 +declare [[values_timeout = 480.0]]
    12.9  
   12.10  section {* Formal Languages *}
   12.11  
    13.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Sun Apr 03 11:40:32 2011 +0200
    13.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Mon Apr 04 09:32:50 2011 +0200
    13.3 @@ -2,7 +2,7 @@
    13.4  imports "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
    13.5  begin
    13.6  
    13.7 -declare [[values_timeout = 240.0]]
    13.8 +declare [[values_timeout = 480.0]]
    13.9  
   13.10  subsection {* Basic predicates *}
   13.11