# HG changeset patch
# User wenzelm
# Date 1601372121 -7200
# Node ID 7cb0c5fbe2d9ee21a204728b4b96f043564742d6
# Parent  da2cbe54e53e9a8921624015b81431ef12fee0a1
obsolete --- KODKODI is always present via component;

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