raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
begin
nitpick_params [verbose, card = 1\<midarrow>6, unary_ints, max_potential = 0,
- sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
subsection {* Curry in a Hurry *}
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
begin
nitpick_params [verbose, card = 1\<midarrow>8, max_potential = 0,
- sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
primrec rot where
"rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Mon Apr 04 09:32:50 2011 +0200
@@ -13,7 +13,7 @@
begin
nitpick_params [verbose, max_potential = 0, sat_solver = MiniSat_JNI,
- max_threads = 1, timeout = 120]
+ max_threads = 1, timeout = 240]
typedecl guest
typedecl key
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
begin
nitpick_params [verbose, card = 1\<midarrow>8, unary_ints,
- sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
inductive p1 :: "nat \<Rightarrow> bool" where
"p1 0" |
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
begin
nitpick_params [verbose, card = 1\<midarrow>5, bits = 1,2,3,4,6,
- sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
lemma "Suc x = x + 1"
nitpick [unary_ints, expect = none]
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Apr 04 09:32:50 2011 +0200
@@ -18,7 +18,7 @@
chapter {* 3. First Steps *}
nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
- timeout = 60]
+ timeout = 240]
subsection {* 3.1. Propositional Logic *}
--- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
begin
nitpick_params [verbose, card = 10, max_potential = 0, sat_solver = MiniSat_JNI,
- max_threads = 1, timeout = 60]
+ max_threads = 1, timeout = 240]
lemma "x = (case u of () \<Rightarrow> y)"
nitpick [expect = genuine]
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
begin
nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
- sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
record point2d =
xc :: int
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
begin
nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
- sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
lemma "P \<and> Q"
apply (rule conjI)
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
begin
nitpick_params [verbose, card = 4, sat_solver = MiniSat_JNI, max_threads = 1,
- timeout = 60]
+ timeout = 240]
fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
"f1 a b c d e = a + b + c + d + e"
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Apr 04 09:32:50 2011 +0200
@@ -12,7 +12,7 @@
begin
nitpick_params [verbose, card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1,
- timeout = 60]
+ timeout = 240]
typedef three = "{0\<Colon>nat, 1, 2}"
by blast
@@ -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 = 240, expect = none]
+nitpick [card = 1, unary_ints, max_potential = 0, expect = none]
by (rule Zero_int_def_raw)
lemma "Abs_list (Rep_list a) = a"
--- a/src/HOL/Predicate_Compile_Examples/Examples.thy Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Examples.thy Mon Apr 04 09:32:50 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 {* Formal Languages *}
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Sun Apr 03 11:40:32 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Mon Apr 04 09:32:50 2011 +0200
@@ -2,7 +2,7 @@
imports "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
begin
-declare [[values_timeout = 240.0]]
+declare [[values_timeout = 480.0]]
subsection {* Basic predicates *}