--- a/src/HOL/Nitpick_Examples/minipick.ML Tue Sep 29 11:15:51 2020 +0200
+++ b/src/HOL/Nitpick_Examples/minipick.ML Tue Sep 29 11:35:21 2020 +0200
@@ -437,7 +437,6 @@
case solve_any_problem debug overlord deadline max_threads max_solutions
problems of
JavaNotFound => "unknown"
- | KodkodiNotInstalled => "unknown"
| Normal ([], _, _) => "none"
| Normal _ => "genuine"
| TimedOut _ => "unknown"
--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Sep 29 11:15:51 2020 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Sep 29 11:35:21 2020 +0200
@@ -158,7 +158,6 @@
datatype outcome =
JavaNotFound |
- KodkodiNotInstalled |
Normal of (int * raw_bound list) list * int list * string |
TimedOut of int list |
Error of string * int list
@@ -304,7 +303,6 @@
datatype outcome =
JavaNotFound |
- KodkodiNotInstalled |
Normal of (int * raw_bound list) list * int list * string |
TimedOut of int list |
Error of string * int list
@@ -1057,9 +1055,6 @@
perhaps (try (unprefix "Error: ")))
|> find_first (fn line => line <> "" andalso line <> "EXIT")
|> the_default ""
- fun has_error s =
- first_error |> Substring.full |> Substring.position s |> snd
- |> Substring.isEmpty |> not
in
if null ps then
if rc = 130 then
@@ -1070,8 +1065,6 @@
Normal ([], js, first_error)
else if rc = 127 then
JavaNotFound
- else if has_error "NoClassDefFoundError" then
- KodkodiNotInstalled
else if first_error <> "" then
Error (first_error, js)
else
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 29 11:15:51 2020 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 29 11:35:21 2020 +0200
@@ -176,8 +176,6 @@
"something appears to be wrong with your Isabelle installation"
val java_not_found_message =
"Java could not be launched -- " ^ isabelle_wrong_message
-val kodkodi_not_installed_message =
- "Nitpick requires the external Java program Kodkodi"
val max_unsound_delay_ms = 200
val max_unsound_delay_percent = 2
@@ -716,9 +714,6 @@
KK.JavaNotFound =>
(print_nt (K java_not_found_message);
(found_really_genuine, max_potential, max_genuine, donno + 1))
- | KK.KodkodiNotInstalled =>
- (print_nt (K kodkodi_not_installed_message);
- (found_really_genuine, max_potential, max_genuine, donno + 1))
| KK.Normal ([], unsat_js, s) =>
(update_checked_problems problems unsat_js; show_kodkod_warning s;
(found_really_genuine, max_potential, max_genuine, donno))
@@ -960,36 +955,30 @@
val print_nt = if is_mode_nt mode then writeln else K ()
val print_t = if mode = TPTP then writeln else K ()
in
- if getenv "KODKODI" = "" then
- (* The "expect" argument is deliberately ignored if Kodkodi is missing so
- that the "Nitpick_Examples" can be processed on any machine. *)
- (print_nt (Pretty.string_of (plazy (K kodkodi_not_installed_message)));
- ("no_kodkodi", []))
- else
- let
- val unknown_outcome = (unknownN, [])
- val deadline = Time.now () + timeout
- val outcome as (outcome_code, _) =
- Timeout.apply (timeout + timeout_bonus)
- (pick_them_nits_in_term deadline state params mode i n step subst
- def_assm_ts nondef_assm_ts) orig_t
- handle TOO_LARGE (_, details) =>
- (print_t "% SZS status GaveUp";
- print_nt ("Limit reached: " ^ details); unknown_outcome)
- | TOO_SMALL (_, details) =>
- (print_t "% SZS status GaveUp";
- print_nt ("Limit reached: " ^ details); unknown_outcome)
- | Kodkod.SYNTAX (_, details) =>
- (print_t "% SZS status GaveUp";
- print_nt ("Malformed Kodkodi output: " ^ details);
- unknown_outcome)
- | Timeout.TIMEOUT _ =>
- (print_t "% SZS status TimedOut";
- print_nt "Nitpick ran out of time"; unknown_outcome)
- in
- if expect = "" orelse outcome_code = expect then outcome
- else error ("Unexpected outcome: " ^ quote outcome_code)
- end
+ let
+ val unknown_outcome = (unknownN, [])
+ val deadline = Time.now () + timeout
+ val outcome as (outcome_code, _) =
+ Timeout.apply (timeout + timeout_bonus)
+ (pick_them_nits_in_term deadline state params mode i n step subst
+ def_assm_ts nondef_assm_ts) orig_t
+ handle TOO_LARGE (_, details) =>
+ (print_t "% SZS status GaveUp";
+ print_nt ("Limit reached: " ^ details); unknown_outcome)
+ | TOO_SMALL (_, details) =>
+ (print_t "% SZS status GaveUp";
+ print_nt ("Limit reached: " ^ details); unknown_outcome)
+ | Kodkod.SYNTAX (_, details) =>
+ (print_t "% SZS status GaveUp";
+ print_nt ("Malformed Kodkodi output: " ^ details);
+ unknown_outcome)
+ | Timeout.TIMEOUT _ =>
+ (print_t "% SZS status TimedOut";
+ print_nt "Nitpick ran out of time"; unknown_outcome)
+ in
+ if expect = "" orelse outcome_code = expect then outcome
+ else error ("Unexpected outcome: " ^ quote outcome_code)
+ end
end
fun is_fixed_equation ctxt