# HG changeset patch
# User wenzelm
# Date 1598360081 -7200
# Node ID bc71db05abe36516c4fd62274134b5d7fece1a66
# Parent  cb746b19e1d7d70b7f313bfe2abde55d2bc91941
removed pointless version checks: Isabelle component integration does the job already;

diff -r cb746b19e1d7 -r bc71db05abe3 src/HOL/Nitpick_Examples/minipick.ML
--- 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"
diff -r cb746b19e1d7 -r bc71db05abe3 src/HOL/Tools/Nitpick/kodkod.ML
--- 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
diff -r cb746b19e1d7 -r bc71db05abe3 src/HOL/Tools/Nitpick/nitpick.ML
--- 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))