more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
--- 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
--- 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\" \
--- 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