distinguish between Kodkodi warnings and errors in Nitpick;
authorblanchet
Tue Feb 23 15:56:13 2010 +0100 (2010-02-23)
changeset 35333f61de25f71f9
parent 35332 22442ab3e7a3
child 35334 b83b9f2a4b92
distinguish between Kodkodi warnings and errors in Nitpick;
will be needed starting with version 1.2.9 of Kodkodi
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Nitpick/minipick.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_tests.ML
     1.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Tue Feb 23 14:50:44 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Tue Feb 23 15:56:13 2010 +0100
     1.3 @@ -158,7 +158,7 @@
     1.4  
     1.5    datatype outcome =
     1.6      NotInstalled |
     1.7 -    Normal of (int * raw_bound list) list * int list |
     1.8 +    Normal of (int * raw_bound list) list * int list * string |
     1.9      TimedOut of int list |
    1.10      Interrupted of int list option |
    1.11      Error of string * int list
    1.12 @@ -304,7 +304,7 @@
    1.13  
    1.14  datatype outcome =
    1.15    NotInstalled |
    1.16 -  Normal of (int * raw_bound list) list * int list |
    1.17 +  Normal of (int * raw_bound list) list * int list * string |
    1.18    TimedOut of int list |
    1.19    Interrupted of int list option |
    1.20    Error of string * int list
    1.21 @@ -1029,7 +1029,7 @@
    1.22      val reindex = fst o nth indexed_problems
    1.23    in
    1.24      if null indexed_problems then
    1.25 -      Normal ([], triv_js)
    1.26 +      Normal ([], triv_js, "")
    1.27      else
    1.28        let
    1.29          val (serial_str, temp_dir) =
    1.30 @@ -1089,6 +1089,8 @@
    1.31                if null ps then
    1.32                  if code = 2 then
    1.33                    TimedOut js
    1.34 +                else if code = 0 then
    1.35 +                  Normal ([], js, first_error)
    1.36                  else if first_error |> Substring.full
    1.37                          |> Substring.position "NoClassDefFoundError" |> snd
    1.38                          |> Substring.isEmpty |> not then
    1.39 @@ -1098,12 +1100,10 @@
    1.40                                       |> perhaps (try (unprefix "Error: ")), js)
    1.41                  else if io_error then
    1.42                    Error ("I/O error", js)
    1.43 -                else if code <> 0 then
    1.44 +                else
    1.45                    Error ("Unknown error", js)
    1.46 -                else
    1.47 -                  Normal ([], js)
    1.48                else
    1.49 -                Normal (ps, js)
    1.50 +                Normal (ps, js, first_error)
    1.51              end
    1.52          in remove_temporary_files (); outcome end
    1.53          handle Exn.Interrupt =>
     2.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Tue Feb 23 14:50:44 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML	Tue Feb 23 15:56:13 2010 +0100
     2.3 @@ -321,7 +321,7 @@
     2.4    in
     2.5      case solve_any_problem overlord NONE max_threads max_solutions problems of
     2.6        NotInstalled => "unknown"
     2.7 -    | Normal ([], _) => "none"
     2.8 +    | Normal ([], _, _) => "none"
     2.9      | Normal _ => "genuine"
    2.10      | TimedOut _ => "unknown"
    2.11      | Interrupted _ => "unknown"
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Feb 23 14:50:44 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Feb 23 15:56:13 2010 +0100
     3.3 @@ -412,7 +412,7 @@
     3.4        if sat_solver <> "smart" then
     3.5          if need_incremental andalso
     3.6             not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
     3.7 -                      sat_solver) then
     3.8 +                       sat_solver) then
     3.9            (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \
    3.10                         \be used instead of " ^ quote sat_solver ^ "."));
    3.11             "SAT4J")
    3.12 @@ -581,6 +581,9 @@
    3.13      fun update_checked_problems problems =
    3.14        List.app (Unsynchronized.change checked_problems o Option.map o cons
    3.15                  o nth problems)
    3.16 +    (* string -> unit *)
    3.17 +    fun show_kodkod_warning "" = ()
    3.18 +      | show_kodkod_warning s = print_v (fn () => "Kodkod warning: " ^ s ^ ".")
    3.19  
    3.20      (* bool -> KK.raw_bound list -> problem_extension -> bool option *)
    3.21      fun print_and_check_model genuine bounds
    3.22 @@ -701,15 +704,16 @@
    3.23              KK.NotInstalled =>
    3.24              (print_m install_kodkodi_message;
    3.25               (max_potential, max_genuine, donno + 1))
    3.26 -          | KK.Normal ([], unsat_js) =>
    3.27 -            (update_checked_problems problems unsat_js;
    3.28 +          | KK.Normal ([], unsat_js, s) =>
    3.29 +            (update_checked_problems problems unsat_js; show_kodkod_warning s;
    3.30               (max_potential, max_genuine, donno))
    3.31 -          | KK.Normal (sat_ps, unsat_js) =>
    3.32 +          | KK.Normal (sat_ps, unsat_js, s) =>
    3.33              let
    3.34                val (lib_ps, con_ps) =
    3.35                  List.partition (#unsound o snd o nth problems o fst) sat_ps
    3.36              in
    3.37                update_checked_problems problems (unsat_js @ map fst lib_ps);
    3.38 +              show_kodkod_warning s;
    3.39                if null con_ps then
    3.40                  let
    3.41                    val num_genuine = take max_potential lib_ps
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Tue Feb 23 14:50:44 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Tue Feb 23 15:56:13 2010 +0100
     4.3 @@ -325,7 +325,7 @@
     4.4  fun run_all_tests () =
     4.5    case Kodkod.solve_any_problem false NONE 0 1
     4.6                                  (map (problem_for_nut @{context}) tests) of
     4.7 -    Kodkod.Normal ([], _) => ()
     4.8 +    Kodkod.Normal ([], _, _) => ()
     4.9    | _ => error "Tests failed"
    4.10  
    4.11  end;