# HG changeset patch # User haftmann # Date 1256655922 -3600 # Node ID b207d84b64ad26cec5c8ada6283fe5aca75ff7b1 # Parent f9ff11344ec4a351b8c51d90d67abc86d4ac7c8d# Parent aac547760e1672e83f2d7be917d84f2b04476ad6 merged diff -r aac547760e16 -r b207d84b64ad src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Oct 27 16:04:44 2009 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Oct 27 16:05:22 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) diff -r aac547760e16 -r b207d84b64ad src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Oct 27 16:04:44 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Oct 27 16:05:22 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")