# HG changeset patch # User blanchet # Date 1292620508 -3600 # Node ID 13972ced98d99964ad1968dee57d6445598ea7b1 # Parent 73401632a80c0482c9b76949a1f76acc8c45f98f more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle diff -r 73401632a80c -r 13972ced98d9 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Fri Dec 17 21:47:13 2010 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Dec 17 22:15:08 2010 +0100 @@ -15,7 +15,7 @@ Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | NoRealZ3 | MalformedInput | MalformedOutput | Interrupted | Crashed | - InternalError | UnknownError + InternalError | UnknownError of string type step_name = string * string option @@ -26,13 +26,14 @@ type 'a proof = 'a uniform_formula step list val strip_spaces : (char -> bool) -> string -> string + val short_output : bool -> string -> string val string_for_failure : string -> failure -> string val extract_important_message : string -> string val extract_known_failure : (failure * string) list -> string -> failure option val extract_tstplike_proof_and_outcome : - bool -> int -> (string * string) list -> (failure * string) list -> string - -> string * failure option + bool -> bool -> int -> (string * string) list -> (failure * string) list + -> string -> string * failure option val is_same_step : step_name * step_name -> bool val atp_proof_from_tstplike_string : bool -> string -> string proof val map_term_names_in_atp_proof : @@ -49,7 +50,7 @@ Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | NoRealZ3 | MalformedInput | MalformedOutput | Interrupted | Crashed | InternalError | - UnknownError + UnknownError of string fun strip_spaces_in_list _ [] = [] | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1] @@ -72,6 +73,15 @@ fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char +fun elide_string threshold s = + if size s > threshold then + String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^ + String.extract (s, size s - (threshold + 1) div 2 + 6, NONE) + else + s +fun short_output verbose output = + if verbose then elide_string 1000 output else "" + fun missing_message_tail prover = " appears to be missing. You will need to install it if you want to run " ^ prover ^ "s remotely." @@ -112,9 +122,10 @@ | string_for_failure prover Crashed = "The " ^ prover ^ " crashed." | string_for_failure prover InternalError = "An internal " ^ prover ^ " error occurred." - | string_for_failure prover UnknownError = + | string_for_failure prover (UnknownError string) = (* "An" is correct for "ATP" and "SMT". *) - "An " ^ prover ^ " error occurred." + "An " ^ prover ^ " error occurred" ^ + (if string = "" then "." else ":\n" ^ string) fun extract_delimited (begin_delim, end_delim) output = output |> first_field begin_delim |> the |> snd @@ -146,16 +157,17 @@ |> find_first (fn (_, pattern) => String.isSubstring pattern output) |> Option.map fst -fun extract_tstplike_proof_and_outcome complete res_code proof_delims +fun extract_tstplike_proof_and_outcome verbose complete res_code proof_delims known_failures output = case extract_known_failure known_failures output of NONE => (case extract_tstplike_proof proof_delims output of "" => ("", SOME (if res_code = 0 andalso output = "" then Interrupted else - UnknownError)) - | tstplike_proof => if res_code = 0 then (tstplike_proof, NONE) - else ("", SOME UnknownError)) + UnknownError (short_output verbose output))) + | tstplike_proof => + if res_code = 0 then (tstplike_proof, NONE) + else ("", SOME (UnknownError (short_output verbose output)))) | SOME failure => ("", SOME (if failure = IncompleteUnprovable andalso complete then Unprovable diff -r 73401632a80c -r 13972ced98d9 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Dec 17 21:47:13 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Dec 17 22:15:08 2010 +0100 @@ -167,7 +167,7 @@ (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ \option (e.g., \"timeout = " ^ string_of_int (10 + msecs div 1000) ^ "\").") - | {outcome = SOME UnknownError, ...} => + | {outcome = SOME (UnknownError _), ...} => (* Failure sometimes mean timeout, unfortunately. *) (NONE, "Failure: No proof was found with the current time limit. You \ \can increase the time limit using the \"timeout\" \ diff -r 73401632a80c -r 13972ced98d9 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Dec 17 21:47:13 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Dec 17 22:15:08 2010 +0100 @@ -396,7 +396,7 @@ I) |>> (if measure_run_time then split_time else rpair NONE) val (tstplike_proof, outcome) = - extract_tstplike_proof_and_outcome complete res_code + extract_tstplike_proof_and_outcome verbose complete res_code proof_delims known_failures output in (output, msecs, tstplike_proof, outcome) end val readable_names = debug andalso overlord @@ -503,11 +503,12 @@ | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) = (case AList.lookup (op =) smt_failures code of SOME failure => failure - | NONE => UnknownError) + | NONE => UnknownError ("Abnormal termination with exit code " ^ + string_of_int code ^ ".")) | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources | failure_from_smt_failure (SMT_Failure.Other_Failure msg) = if String.isPrefix internal_error_prefix msg then InternalError - else UnknownError + else UnknownError msg (* FUDGE *) val smt_max_iters = Unsynchronized.ref 8