--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Oct 27 14:40:24 2009 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Oct 27 15:55:36 2009 +0100
@@ -157,6 +157,7 @@
type raw_bound = n_ary_index * int list list
datatype outcome =
+ NotInstalled |
Normal of (int * raw_bound list) list * int list |
TimedOut of int list |
Interrupted of int list option |
@@ -301,6 +302,7 @@
type raw_bound = n_ary_index * int list list
datatype outcome =
+ NotInstalled |
Normal of (int * raw_bound list) list * int list |
TimedOut of int list |
Interrupted of int list option |
@@ -1069,6 +1071,10 @@
if null ps then
if code = 2 then
TimedOut js
+ else if first_error |> Substring.full
+ |> Substring.position "NoClassDefFoundError" |> snd
+ |> Substring.isEmpty |> not then
+ NotInstalled
else if first_error <> "" then
Error (first_error |> perhaps (try (unsuffix "."))
|> perhaps (try (unprefix "Error: ")), js)
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Oct 27 14:40:24 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Oct 27 15:55:36 2009 +0100
@@ -626,7 +626,18 @@
else
case Kodkod.solve_any_problem overlord deadline max_threads
max_solutions (map fst problems) of
- Kodkod.Normal ([], unsat_js) =>
+ Kodkod.NotInstalled =>
+ (print_m (fn () =>
+ "Nitpick requires the external Java program Kodkodi. \
+ \To install it, download the package from Isabelle's \
+ \web page and add the \"kodkodi-x.y.z\" directory's \
+ \full path to \"" ^
+ Path.implode (Path.expand (Path.appends
+ (Path.variable "ISABELLE_HOME" ::
+ (map Path.basic ["etc", "components"])))) ^
+ "\".");
+ (max_potential, max_genuine, donno + 1))
+ | Kodkod.Normal ([], unsat_js) =>
(update_checked_problems problems unsat_js;
(max_potential, max_genuine, donno))
| Kodkod.Normal (sat_ps, unsat_js) =>
@@ -785,7 +796,7 @@
(* int -> int -> scope list -> int * int * int -> Kodkod.outcome *)
fun run_batches _ _ [] (max_potential, max_genuine, donno) =
if donno > 0 andalso max_genuine > 0 then
- (print_m (fn () => excipit "ran out of resources"); "unknown")
+ (print_m (fn () => excipit "ran into difficulties"); "unknown")
else if max_genuine = original_max_genuine then
if max_potential = original_max_potential then
(print_m (K ("Nitpick found no " ^ word_model ^ ".")); "none")