catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
--- a/doc-src/Nitpick/nitpick.tex Tue Feb 23 08:08:23 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Tue Feb 23 10:02:14 2010 +0100
@@ -150,11 +150,11 @@
\postw
The results presented here were obtained using the JNI version of MiniSat and
-with multithreading disabled to reduce nondeterminism. This was done by adding
-the line
+with multithreading disabled to reduce nondeterminism and a time limit of
+15~seconds (instead of 30~seconds). This was done by adding the line
\prew
-\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1]
+\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1, \,\,\textit{timeout} = 15$\,s$]
\postw
after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
@@ -499,7 +499,7 @@
\prew
\textbf{lemma} ``$P~\textit{Suc}$'' \\
-\textbf{nitpick} [\textit{card} = 1--6] \\[2\smallskipamount]
+\textbf{nitpick} \\[2\smallskipamount]
\slshape
Nitpick found no counterexample.
\postw
@@ -1617,7 +1617,7 @@
``$w \in A \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] + 1$'' \\
``$w \in B \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] + 1$'' \\
\textbf{nitpick} \\[2\smallskipamount]
-\slshape Nitpick found no counterexample.
+\slshape Nitpick ran out of time after checking 7 of 8 scopes.
\postw
\subsection{AA Trees}
@@ -1726,7 +1726,7 @@
``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
\textbf{nitpick} \\[2\smallskipamount]
-{\slshape Nitpick found no counterexample.}
+{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
\postw
Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Feb 23 08:08:23 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Feb 23 10:02:14 2010 +0100
@@ -13,7 +13,7 @@
chapter {* 3. First Steps *}
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 15 s]
subsection {* 3.1. Propositional Logic *}
@@ -70,7 +70,7 @@
oops
lemma "P Suc"
-nitpick [card = 1-6]
+nitpick
oops
lemma "P (op +\<Colon>nat\<Rightarrow>nat\<Rightarrow>nat)"
@@ -210,7 +210,7 @@
lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>1 \<sigma> t = t"
nitpick [verbose]
nitpick [eval = "subst\<^isub>1 \<sigma> t"]
-nitpick [dont_box]
+(* nitpick [dont_box] *)
oops
primrec subst\<^isub>2 where
@@ -220,7 +220,7 @@
"subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
-nitpick
+nitpick [card = 1\<midarrow>6]
sorry
subsection {* 3.11. Scope Monotonicity *}
@@ -243,7 +243,7 @@
"n \<in> reach \<Longrightarrow> n + 2 \<in> reach"
lemma "n \<in> reach \<Longrightarrow> 2 dvd n"
-nitpick
+nitpick [unary_ints]
apply (induct set: reach)
apply auto
nitpick
@@ -252,7 +252,7 @@
oops
lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
-nitpick
+nitpick [unary_ints]
apply (induct set: reach)
apply auto
nitpick
@@ -289,12 +289,12 @@
if b \<in> labels t then labels t else (labels t - {a}) \<union> {b}
else
if b \<in> labels t then (labels t - {b}) \<union> {a} else labels t)"
-nitpick
+(* nitpick *)
proof (induct t)
case Leaf thus ?case by simp
next
case (Branch t u) thus ?case
- nitpick [non_std "'a bin_tree", show_consts]
+ nitpick [non_std, show_all]
by auto
qed
--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Feb 23 08:08:23 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Feb 23 10:02:14 2010 +0100
@@ -1004,9 +1004,11 @@
handle Option.Option => raise SYNTAX ("Kodkod.read_next_problems",
"expected number after \"PROBLEM\"")
-(* Path.T -> (int * raw_bound list) list * int list *)
+(* Path.T -> bool * ((int * raw_bound list) list * int list) *)
fun read_output_file path =
- read_next_problems (Substring.full (File.read path), [], []) |>> rev ||> rev
+ (false, read_next_problems (Substring.full (File.read path), [], [])
+ |>> rev ||> rev)
+ handle IO.Io _ => (true, ([], [])) | OS.SysErr _ => (true, ([], []))
(* The fudge term below is to account for Kodkodi's slow start-up time, which
is partly due to the JVM and partly due to the ML "bash" function. *)
@@ -1046,7 +1048,7 @@
(* unit -> unit *)
fun remove_temporary_files () =
if overlord then ()
- else List.app File.rm [in_path, out_path, err_path]
+ else List.app (K () o try File.rm) [in_path, out_path, err_path]
in
let
val ms =
@@ -1076,11 +1078,13 @@
" < " ^ File.shell_path in_path ^
" > " ^ File.shell_path out_path ^
" 2> " ^ File.shell_path err_path)
- val (ps, nontriv_js) = read_output_file out_path
- |>> map (apfst reindex) ||> map reindex
+ val (io_error, (ps, nontriv_js)) =
+ read_output_file out_path
+ ||> apfst (map (apfst reindex)) ||> apsnd (map reindex)
val js = triv_js @ nontriv_js
val first_error =
File.fold_lines (fn line => fn "" => line | s => s) err_path ""
+ handle IO.Io _ => "" | OS.SysErr _ => ""
in
if null ps then
if code = 2 then
@@ -1092,6 +1096,8 @@
else if first_error <> "" then
Error (first_error |> perhaps (try (unsuffix "."))
|> perhaps (try (unprefix "Error: ")), js)
+ else if io_error then
+ Error ("I/O error", js)
else if code <> 0 then
Error ("Unknown error", js)
else
@@ -1102,7 +1108,8 @@
in remove_temporary_files (); outcome end
handle Exn.Interrupt =>
let
- val nontriv_js = map reindex (snd (read_output_file out_path))
+ val nontriv_js =
+ read_output_file out_path |> snd |> snd |> map reindex
in
(remove_temporary_files ();
Interrupted (SOME (triv_js @ nontriv_js)))
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Feb 23 08:08:23 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Feb 23 10:02:14 2010 +0100
@@ -1819,8 +1819,7 @@
termination_tacs
in Synchronized.change cached_wf_props (cons (prop, wf)); wf end
end)
- handle List.Empty => false
- | NO_TRIPLE () => false
+ handle List.Empty => false | NO_TRIPLE () => false
(* The type constraint below is a workaround for a Poly/ML crash. *)