summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Sun, 19 Dec 2010 11:48:42 +0100 | |

changeset 41278 | 8e1cde88aae6 |

parent 41277 | 1369c27c6966 |

child 41279 | e0400b05a62c |

added a timestamp to Nitpick in verbose mode for debugging purposes;
turn on verbose mode for the examples

--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Sun Dec 19 00:13:25 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Sun Dec 19 11:48:42 2010 +0100 @@ -11,7 +11,7 @@ imports Main begin -nitpick_params [card = 1\<midarrow>6, unary_ints, max_potential = 0, +nitpick_params [verbose, card = 1\<midarrow>6, unary_ints, max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] subsection {* Curry in a Hurry *}

--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Sun Dec 19 00:13:25 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Sun Dec 19 11:48:42 2010 +0100 @@ -11,7 +11,7 @@ imports Main begin -nitpick_params [card = 1\<midarrow>8, max_potential = 0, +nitpick_params [verbose, card = 1\<midarrow>8, max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] primrec rot where

--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Sun Dec 19 00:13:25 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Sun Dec 19 11:48:42 2010 +0100 @@ -12,8 +12,8 @@ imports Main begin -nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, - timeout = 120] +nitpick_params [verbose, max_potential = 0, sat_solver = MiniSat_JNI, + max_threads = 1, timeout = 120] typedecl guest typedecl key

--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Sun Dec 19 00:13:25 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Sun Dec 19 11:48:42 2010 +0100 @@ -11,8 +11,8 @@ imports Main begin -nitpick_params [card = 1\<midarrow>8, unary_ints, sat_solver = MiniSat_JNI, - max_threads = 1, timeout = 60] +nitpick_params [verbose, card = 1\<midarrow>8, unary_ints, + sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] inductive p1 :: "nat \<Rightarrow> bool" where "p1 0" |

--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Sun Dec 19 00:13:25 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Sun Dec 19 11:48:42 2010 +0100 @@ -11,7 +11,7 @@ imports Nitpick begin -nitpick_params [card = 1\<midarrow>5, bits = 1,2,3,4,6, +nitpick_params [verbose, card = 1\<midarrow>5, bits = 1,2,3,4,6, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] lemma "Suc x = x + 1"

--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Sun Dec 19 00:13:25 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Sun Dec 19 11:48:42 2010 +0100 @@ -17,7 +17,8 @@ chapter {* 3. First Steps *} -nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] +nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1, + timeout = 60] subsection {* 3.1. Propositional Logic *}

--- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy Sun Dec 19 00:13:25 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy Sun Dec 19 11:48:42 2010 +0100 @@ -11,7 +11,7 @@ imports Main begin -nitpick_params [card = 10, max_potential = 0, sat_solver = MiniSat_JNI, +nitpick_params [verbose, card = 10, max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] lemma "x = (case u of () \<Rightarrow> y)"

--- a/src/HOL/Nitpick_Examples/Record_Nits.thy Sun Dec 19 00:13:25 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Sun Dec 19 11:48:42 2010 +0100 @@ -11,7 +11,7 @@ imports Main begin -nitpick_params [card = 1\<midarrow>6, max_potential = 0, +nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] record point2d =

--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Sun Dec 19 00:13:25 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Sun Dec 19 11:48:42 2010 +0100 @@ -11,7 +11,7 @@ imports Main begin -nitpick_params [card = 1\<midarrow>6, max_potential = 0, +nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] lemma "P \<and> Q"

--- a/src/HOL/Nitpick_Examples/Special_Nits.thy Sun Dec 19 00:13:25 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Sun Dec 19 11:48:42 2010 +0100 @@ -11,7 +11,7 @@ imports Main begin -nitpick_params [card = 4, sat_solver = MiniSat_JNI, max_threads = 1, +nitpick_params [verbose, card = 4, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where

--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Sun Dec 19 00:13:25 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Sun Dec 19 11:48:42 2010 +0100 @@ -11,7 +11,7 @@ imports Complex_Main begin -nitpick_params [card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1, +nitpick_params [verbose, card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] typedef three = "{0\<Colon>nat, 1, 2}"

--- a/src/HOL/Tools/Nitpick/nitpick.ML Sun Dec 19 00:13:25 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sun Dec 19 11:48:42 2010 +0100 @@ -246,6 +246,8 @@ "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n else "goal")) [Logic.list_implies (assm_ts, orig_t)])) + val _ = print_v (enclose "Timestamp: " "." o Date.fmt "%H:%M:%S" + o Date.fromTimeLocal o Time.now) val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False}) else orig_t val tfree_table =