distinguish between Kodkodi warnings and errors in Nitpick;
will be needed starting with version 1.2.9 of Kodkodi
--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Feb 23 14:50:44 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Feb 23 15:56:13 2010 +0100
@@ -158,7 +158,7 @@
datatype outcome =
NotInstalled |
- Normal of (int * raw_bound list) list * int list |
+ Normal of (int * raw_bound list) list * int list * string |
TimedOut of int list |
Interrupted of int list option |
Error of string * int list
@@ -304,7 +304,7 @@
datatype outcome =
NotInstalled |
- Normal of (int * raw_bound list) list * int list |
+ Normal of (int * raw_bound list) list * int list * string |
TimedOut of int list |
Interrupted of int list option |
Error of string * int list
@@ -1029,7 +1029,7 @@
val reindex = fst o nth indexed_problems
in
if null indexed_problems then
- Normal ([], triv_js)
+ Normal ([], triv_js, "")
else
let
val (serial_str, temp_dir) =
@@ -1089,6 +1089,8 @@
if null ps then
if code = 2 then
TimedOut js
+ else if code = 0 then
+ Normal ([], js, first_error)
else if first_error |> Substring.full
|> Substring.position "NoClassDefFoundError" |> snd
|> Substring.isEmpty |> not then
@@ -1098,12 +1100,10 @@
|> perhaps (try (unprefix "Error: ")), js)
else if io_error then
Error ("I/O error", js)
- else if code <> 0 then
+ else
Error ("Unknown error", js)
- else
- Normal ([], js)
else
- Normal (ps, js)
+ Normal (ps, js, first_error)
end
in remove_temporary_files (); outcome end
handle Exn.Interrupt =>
--- a/src/HOL/Tools/Nitpick/minipick.ML Tue Feb 23 14:50:44 2010 +0100
+++ b/src/HOL/Tools/Nitpick/minipick.ML Tue Feb 23 15:56:13 2010 +0100
@@ -321,7 +321,7 @@
in
case solve_any_problem overlord NONE max_threads max_solutions problems of
NotInstalled => "unknown"
- | Normal ([], _) => "none"
+ | Normal ([], _, _) => "none"
| Normal _ => "genuine"
| TimedOut _ => "unknown"
| Interrupted _ => "unknown"
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Feb 23 14:50:44 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Feb 23 15:56:13 2010 +0100
@@ -412,7 +412,7 @@
if sat_solver <> "smart" then
if need_incremental andalso
not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
- sat_solver) then
+ sat_solver) then
(print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \
\be used instead of " ^ quote sat_solver ^ "."));
"SAT4J")
@@ -581,6 +581,9 @@
fun update_checked_problems problems =
List.app (Unsynchronized.change checked_problems o Option.map o cons
o nth problems)
+ (* string -> unit *)
+ fun show_kodkod_warning "" = ()
+ | show_kodkod_warning s = print_v (fn () => "Kodkod warning: " ^ s ^ ".")
(* bool -> KK.raw_bound list -> problem_extension -> bool option *)
fun print_and_check_model genuine bounds
@@ -701,15 +704,16 @@
KK.NotInstalled =>
(print_m install_kodkodi_message;
(max_potential, max_genuine, donno + 1))
- | KK.Normal ([], unsat_js) =>
- (update_checked_problems problems unsat_js;
+ | KK.Normal ([], unsat_js, s) =>
+ (update_checked_problems problems unsat_js; show_kodkod_warning s;
(max_potential, max_genuine, donno))
- | KK.Normal (sat_ps, unsat_js) =>
+ | KK.Normal (sat_ps, unsat_js, s) =>
let
val (lib_ps, con_ps) =
List.partition (#unsound o snd o nth problems o fst) sat_ps
in
update_checked_problems problems (unsat_js @ map fst lib_ps);
+ show_kodkod_warning s;
if null con_ps then
let
val num_genuine = take max_potential lib_ps
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Tue Feb 23 14:50:44 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Tue Feb 23 15:56:13 2010 +0100
@@ -325,7 +325,7 @@
fun run_all_tests () =
case Kodkod.solve_any_problem false NONE 0 1
(map (problem_for_nut @{context}) tests) of
- Kodkod.Normal ([], _) => ()
+ Kodkod.Normal ([], _, _) => ()
| _ => error "Tests failed"
end;