# HG changeset patch
# User blanchet
# Date 1266915734 -3600
# Node ID 997aa3a3e4bbfcfd4fab9c3508241774d6bcaf9c
# Parent  359e0fd38a92a0a760c8e0acefc6e8454ccfb94e
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example

diff -r 359e0fd38a92 -r 997aa3a3e4bb doc-src/Nitpick/nitpick.tex
--- 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
diff -r 359e0fd38a92 -r 997aa3a3e4bb src/HOL/Nitpick_Examples/Manual_Nits.thy
--- 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
 
diff -r 359e0fd38a92 -r 997aa3a3e4bb src/HOL/Tools/Nitpick/kodkod.ML
--- 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)))
diff -r 359e0fd38a92 -r 997aa3a3e4bb src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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. *)