# HG changeset patch # User blanchet # Date 1266936973 -3600 # Node ID f61de25f71f9e677002fbec1c4ae9fde803c261b # Parent 22442ab3e7a3504e658e9bd369aedef068f60209 distinguish between Kodkodi warnings and errors in Nitpick; will be needed starting with version 1.2.9 of Kodkodi diff -r 22442ab3e7a3 -r f61de25f71f9 src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Feb 23 14:50:44 2010 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Feb 23 15:56:13 2010 +0100 @@ -158,7 +158,7 @@ datatype outcome = NotInstalled | - Normal of (int * raw_bound list) list * int list | + Normal of (int * raw_bound list) list * int list * string | TimedOut of int list | Interrupted of int list option | Error of string * int list @@ -304,7 +304,7 @@ datatype outcome = NotInstalled | - Normal of (int * raw_bound list) list * int list | + Normal of (int * raw_bound list) list * int list * string | TimedOut of int list | Interrupted of int list option | Error of string * int list @@ -1029,7 +1029,7 @@ val reindex = fst o nth indexed_problems in if null indexed_problems then - Normal ([], triv_js) + Normal ([], triv_js, "") else let val (serial_str, temp_dir) = @@ -1089,6 +1089,8 @@ if null ps then if code = 2 then TimedOut js + else if code = 0 then + Normal ([], js, first_error) else if first_error |> Substring.full |> Substring.position "NoClassDefFoundError" |> snd |> Substring.isEmpty |> not then @@ -1098,12 +1100,10 @@ |> perhaps (try (unprefix "Error: ")), js) else if io_error then Error ("I/O error", js) - else if code <> 0 then + else Error ("Unknown error", js) - else - Normal ([], js) else - Normal (ps, js) + Normal (ps, js, first_error) end in remove_temporary_files (); outcome end handle Exn.Interrupt => diff -r 22442ab3e7a3 -r f61de25f71f9 src/HOL/Tools/Nitpick/minipick.ML --- a/src/HOL/Tools/Nitpick/minipick.ML Tue Feb 23 14:50:44 2010 +0100 +++ b/src/HOL/Tools/Nitpick/minipick.ML Tue Feb 23 15:56:13 2010 +0100 @@ -321,7 +321,7 @@ in case solve_any_problem overlord NONE max_threads max_solutions problems of NotInstalled => "unknown" - | Normal ([], _) => "none" + | Normal ([], _, _) => "none" | Normal _ => "genuine" | TimedOut _ => "unknown" | Interrupted _ => "unknown" diff -r 22442ab3e7a3 -r f61de25f71f9 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Feb 23 14:50:44 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Feb 23 15:56:13 2010 +0100 @@ -412,7 +412,7 @@ if sat_solver <> "smart" then if need_incremental andalso not (member (op =) (Kodkod_SAT.configured_sat_solvers true) - sat_solver) then + sat_solver) then (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \ \be used instead of " ^ quote sat_solver ^ ".")); "SAT4J") @@ -581,6 +581,9 @@ fun update_checked_problems problems = List.app (Unsynchronized.change checked_problems o Option.map o cons o nth problems) + (* string -> unit *) + fun show_kodkod_warning "" = () + | show_kodkod_warning s = print_v (fn () => "Kodkod warning: " ^ s ^ ".") (* bool -> KK.raw_bound list -> problem_extension -> bool option *) fun print_and_check_model genuine bounds @@ -701,15 +704,16 @@ KK.NotInstalled => (print_m install_kodkodi_message; (max_potential, max_genuine, donno + 1)) - | KK.Normal ([], unsat_js) => - (update_checked_problems problems unsat_js; + | KK.Normal ([], unsat_js, s) => + (update_checked_problems problems unsat_js; show_kodkod_warning s; (max_potential, max_genuine, donno)) - | KK.Normal (sat_ps, unsat_js) => + | KK.Normal (sat_ps, unsat_js, s) => let val (lib_ps, con_ps) = List.partition (#unsound o snd o nth problems o fst) sat_ps in update_checked_problems problems (unsat_js @ map fst lib_ps); + show_kodkod_warning s; if null con_ps then let val num_genuine = take max_potential lib_ps diff -r 22442ab3e7a3 -r f61de25f71f9 src/HOL/Tools/Nitpick/nitpick_tests.ML --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Tue Feb 23 14:50:44 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Tue Feb 23 15:56:13 2010 +0100 @@ -325,7 +325,7 @@ fun run_all_tests () = case Kodkod.solve_any_problem false NONE 0 1 (map (problem_for_nut @{context}) tests) of - Kodkod.Normal ([], _) => () + Kodkod.Normal ([], _, _) => () | _ => error "Tests failed" end;