added a timestamp to Nitpick in verbose mode for debugging purposes;
authorblanchet
Sun Dec 19 11:48:42 2010 +0100 (2010-12-19 ago)
changeset 412788e1cde88aae6
parent 41277 1369c27c6966
child 41279 e0400b05a62c
added a timestamp to Nitpick in verbose mode for debugging purposes;
turn on verbose mode for the examples
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/Tools/Nitpick/nitpick.ML
     1.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -nitpick_params [card = 1\<midarrow>6, unary_ints, max_potential = 0,
     1.8 +nitpick_params [verbose, card = 1\<midarrow>6, unary_ints, max_potential = 0,
     1.9                  sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
    1.10  
    1.11  subsection {* Curry in a Hurry *}
     2.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
     2.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
     2.3 @@ -11,7 +11,7 @@
     2.4  imports Main
     2.5  begin
     2.6  
     2.7 -nitpick_params [card = 1\<midarrow>8, max_potential = 0,
     2.8 +nitpick_params [verbose, card = 1\<midarrow>8, max_potential = 0,
     2.9                  sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
    2.10  
    2.11  primrec rot where
     3.1 --- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
     3.2 +++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
     3.3 @@ -12,8 +12,8 @@
     3.4  imports Main
     3.5  begin
     3.6  
     3.7 -nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
     3.8 -                timeout = 120]
     3.9 +nitpick_params [verbose, max_potential = 0, sat_solver = MiniSat_JNI,
    3.10 +                max_threads = 1, timeout = 120]
    3.11  
    3.12  typedecl guest
    3.13  typedecl key
     4.1 --- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
     4.2 +++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
     4.3 @@ -11,8 +11,8 @@
     4.4  imports Main
     4.5  begin
     4.6  
     4.7 -nitpick_params [card = 1\<midarrow>8, unary_ints, sat_solver = MiniSat_JNI,
     4.8 -                max_threads = 1, timeout = 60]
     4.9 +nitpick_params [verbose, card = 1\<midarrow>8, unary_ints,
    4.10 +                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
    4.11  
    4.12  inductive p1 :: "nat \<Rightarrow> bool" where
    4.13  "p1 0" |
     5.1 --- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
     5.2 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
     5.3 @@ -11,7 +11,7 @@
     5.4  imports Nitpick
     5.5  begin
     5.6  
     5.7 -nitpick_params [card = 1\<midarrow>5, bits = 1,2,3,4,6,
     5.8 +nitpick_params [verbose, card = 1\<midarrow>5, bits = 1,2,3,4,6,
     5.9                  sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
    5.10  
    5.11  lemma "Suc x = x + 1"
     6.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
     6.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
     6.3 @@ -17,7 +17,8 @@
     6.4  
     6.5  chapter {* 3. First Steps *}
     6.6  
     6.7 -nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
     6.8 +nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
     6.9 +                timeout = 60]
    6.10  
    6.11  subsection {* 3.1. Propositional Logic *}
    6.12  
     7.1 --- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
     7.2 +++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
     7.3 @@ -11,7 +11,7 @@
     7.4  imports Main
     7.5  begin
     7.6  
     7.7 -nitpick_params [card = 10, max_potential = 0, sat_solver = MiniSat_JNI,
     7.8 +nitpick_params [verbose, card = 10, max_potential = 0, sat_solver = MiniSat_JNI,
     7.9                  max_threads = 1, timeout = 60]
    7.10  
    7.11  lemma "x = (case u of () \<Rightarrow> y)"
     8.1 --- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
     8.2 +++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
     8.3 @@ -11,7 +11,7 @@
     8.4  imports Main
     8.5  begin
     8.6  
     8.7 -nitpick_params [card = 1\<midarrow>6, max_potential = 0,
     8.8 +nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
     8.9                  sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
    8.10  
    8.11  record point2d =
     9.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
     9.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
     9.3 @@ -11,7 +11,7 @@
     9.4  imports Main
     9.5  begin
     9.6  
     9.7 -nitpick_params [card = 1\<midarrow>6, max_potential = 0,
     9.8 +nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
     9.9                  sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
    9.10  
    9.11  lemma "P \<and> Q"
    10.1 --- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
    10.2 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
    10.3 @@ -11,7 +11,7 @@
    10.4  imports Main
    10.5  begin
    10.6  
    10.7 -nitpick_params [card = 4, sat_solver = MiniSat_JNI, max_threads = 1,
    10.8 +nitpick_params [verbose, card = 4, sat_solver = MiniSat_JNI, max_threads = 1,
    10.9                  timeout = 60]
   10.10  
   10.11  fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
    11.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
    11.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
    11.3 @@ -11,7 +11,7 @@
    11.4  imports Complex_Main
    11.5  begin
    11.6  
    11.7 -nitpick_params [card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1,
    11.8 +nitpick_params [verbose, card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1,
    11.9                  timeout = 60]
   11.10  
   11.11  typedef three = "{0\<Colon>nat, 1, 2}"
    12.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sun Dec 19 00:13:25 2010 +0100
    12.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sun Dec 19 11:48:42 2010 +0100
    12.3 @@ -246,6 +246,8 @@
    12.4                     "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
    12.5                   else
    12.6                     "goal")) [Logic.list_implies (assm_ts, orig_t)]))
    12.7 +    val _ = print_v (enclose "Timestamp: " "." o Date.fmt "%H:%M:%S"
    12.8 +                     o Date.fromTimeLocal o Time.now)
    12.9      val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
   12.10                  else orig_t
   12.11      val tfree_table =