removed pointless version checks: Isabelle component integration does the job already;
--- a/src/HOL/Nitpick_Examples/minipick.ML Tue Aug 25 13:44:09 2020 +0200
+++ b/src/HOL/Nitpick_Examples/minipick.ML Tue Aug 25 14:54:41 2020 +0200
@@ -437,9 +437,7 @@
case solve_any_problem debug overlord deadline max_threads max_solutions
problems of
JavaNotFound => "unknown"
- | JavaTooOld => "unknown"
| KodkodiNotInstalled => "unknown"
- | KodkodiTooOld => "unknown"
| Normal ([], _, _) => "none"
| Normal _ => "genuine"
| TimedOut _ => "unknown"
--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Aug 25 13:44:09 2020 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Aug 25 14:54:41 2020 +0200
@@ -158,9 +158,7 @@
datatype outcome =
JavaNotFound |
- JavaTooOld |
KodkodiNotInstalled |
- KodkodiTooOld |
Normal of (int * raw_bound list) list * int list * string |
TimedOut of int list |
Error of string * int list
@@ -306,9 +304,7 @@
datatype outcome =
JavaNotFound |
- JavaTooOld |
KodkodiNotInstalled |
- KodkodiTooOld |
Normal of (int * raw_bound list) list * int list * string |
TimedOut of int list |
Error of string * int list
@@ -325,8 +321,6 @@
|> space_explode "."
|> map (the_default 0 o Int.fromString)
-fun is_kodkodi_too_old () =
- is_less (dict_ord int_ord (kodkodi_version (), [1, 2, 14]))
(** Auxiliary functions on Kodkod problems **)
@@ -1076,12 +1070,8 @@
Normal ([], js, first_error)
else if rc = 127 then
JavaNotFound
- else if has_error "UnsupportedClassVersionError" then
- JavaTooOld
else if has_error "NoClassDefFoundError" then
KodkodiNotInstalled
- else if is_kodkodi_too_old () then
- KodkodiTooOld
else if first_error <> "" then
Error (first_error, js)
else
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Aug 25 13:44:09 2020 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Aug 25 14:54:41 2020 +0200
@@ -176,11 +176,8 @@
"something appears to be wrong with your Isabelle installation"
val java_not_found_message =
"Java could not be launched -- " ^ isabelle_wrong_message
-val java_too_old_message =
- "The Java version is too old -- " ^ isabelle_wrong_message
val kodkodi_not_installed_message =
"Nitpick requires the external Java program Kodkodi"
-val kodkodi_too_old_message = "The installed Kodkodi version is too old"
val max_unsound_delay_ms = 200
val max_unsound_delay_percent = 2
@@ -725,15 +722,9 @@
KK.JavaNotFound =>
(print_nt (K java_not_found_message);
(found_really_genuine, max_potential, max_genuine, donno + 1))
- | KK.JavaTooOld =>
- (print_nt (K java_too_old_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.KodkodiTooOld =>
- (print_nt (K kodkodi_too_old_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))