177 Pretty.block [t |> shorten_names_in_term |
177 Pretty.block [t |> shorten_names_in_term |
178 |> Syntax.pretty_term ctxt, |
178 |> Syntax.pretty_term ctxt, |
179 Pretty.str (if j = 1 then "." else ";")]) |
179 Pretty.str (if j = 1 then "." else ";")]) |
180 (length ts downto 1) ts))] |
180 (length ts downto 1) ts))] |
181 |
181 |
182 fun install_java_message () = |
182 val isabelle_wrong_message = |
183 "Nitpick requires Java Development Kit 1.6 via ISABELLE_JDK_HOME setting." |
183 "Something appears to be wrong with your Isabelle installation." |
184 fun install_kodkodi_message () = |
184 fun java_not_found_message () = |
|
185 "Java could not be launched. " ^ isabelle_wrong_message |
|
186 fun java_too_old_message () = |
|
187 "The Java version is too old. " ^ isabelle_wrong_message |
|
188 fun kodkodi_not_installed_message () = |
185 "Nitpick requires the external Java program Kodkodi. To install it, download \ |
189 "Nitpick requires the external Java program Kodkodi. To install it, download \ |
186 \the package from \"http://www21.in.tum.de/~blanchet/#software\" and add the \ |
190 \the package from \"http://www21.in.tum.de/~blanchet/#software\" and add the \ |
187 \\"kodkodi-x.y.z\" directory's full path to " ^ |
191 \\"kodkodi-x.y.z\" directory's full path to " ^ |
188 Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/etc/components")) ^ |
192 Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/etc/components")) ^ |
189 " on a line of its own." |
193 " on a line of its own." |
800 if max_solutions <= 0 then |
804 if max_solutions <= 0 then |
801 (found_really_genuine, 0, 0, donno) |
805 (found_really_genuine, 0, 0, donno) |
802 else |
806 else |
803 case KK.solve_any_problem debug overlord deadline max_threads |
807 case KK.solve_any_problem debug overlord deadline max_threads |
804 max_solutions (map fst problems) of |
808 max_solutions (map fst problems) of |
805 KK.JavaNotInstalled => |
809 KK.JavaNotFound => |
806 (print_nt install_java_message; |
810 (print_nt java_not_found_message; |
807 (found_really_genuine, max_potential, max_genuine, donno + 1)) |
811 (found_really_genuine, max_potential, max_genuine, donno + 1)) |
808 | KK.JavaTooOld => |
812 | KK.JavaTooOld => |
809 (print_nt install_java_message; |
813 (print_nt java_too_old_message; |
810 (found_really_genuine, max_potential, max_genuine, donno + 1)) |
814 (found_really_genuine, max_potential, max_genuine, donno + 1)) |
811 | KK.KodkodiNotInstalled => |
815 | KK.KodkodiNotInstalled => |
812 (print_nt install_kodkodi_message; |
816 (print_nt kodkodi_not_installed_message; |
813 (found_really_genuine, max_potential, max_genuine, donno + 1)) |
817 (found_really_genuine, max_potential, max_genuine, donno + 1)) |
814 | KK.Normal ([], unsat_js, s) => |
818 | KK.Normal ([], unsat_js, s) => |
815 (update_checked_problems problems unsat_js; show_kodkod_warning s; |
819 (update_checked_problems problems unsat_js; show_kodkod_warning s; |
816 (found_really_genuine, max_potential, max_genuine, donno)) |
820 (found_really_genuine, max_potential, max_genuine, donno)) |
817 | KK.Normal (sat_ps, unsat_js, s) => |
821 | KK.Normal (sat_ps, unsat_js, s) => |
1060 val print_t = if mode = TPTP then Output.urgent_message else K () |
1064 val print_t = if mode = TPTP then Output.urgent_message else K () |
1061 in |
1065 in |
1062 if getenv "KODKODI" = "" then |
1066 if getenv "KODKODI" = "" then |
1063 (* The "expect" argument is deliberately ignored if Kodkodi is missing so |
1067 (* The "expect" argument is deliberately ignored if Kodkodi is missing so |
1064 that the "Nitpick_Examples" can be processed on any machine. *) |
1068 that the "Nitpick_Examples" can be processed on any machine. *) |
1065 (print_nt (Pretty.string_of (plazy install_kodkodi_message)); |
1069 (print_nt (Pretty.string_of (plazy kodkodi_not_installed_message)); |
1066 ("no_kodkodi", state)) |
1070 ("no_kodkodi", state)) |
1067 else |
1071 else |
1068 let |
1072 let |
1069 val unknown_outcome = (unknownN, state) |
1073 val unknown_outcome = (unknownN, state) |
1070 val deadline = Option.map (curry Time.+ (Time.now ())) timeout |
1074 val deadline = Option.map (curry Time.+ (Time.now ())) timeout |