30 val string_for_failure : failure -> string |
30 val string_for_failure : failure -> string |
31 val extract_important_message : string -> string |
31 val extract_important_message : string -> string |
32 val extract_known_failure : |
32 val extract_known_failure : |
33 (failure * string) list -> string -> failure option |
33 (failure * string) list -> string -> failure option |
34 val extract_tstplike_proof_and_outcome : |
34 val extract_tstplike_proof_and_outcome : |
35 bool -> bool -> int -> (string * string) list -> (failure * string) list |
35 bool -> bool -> bool -> int -> (string * string) list |
36 -> string -> string * failure option |
36 -> (failure * string) list -> string -> string * failure option |
37 val is_same_step : step_name * step_name -> bool |
37 val is_same_step : step_name * step_name -> bool |
38 val atp_proof_from_tstplike_string : bool -> string -> string proof |
38 val atp_proof_from_tstplike_string : bool -> string -> string proof |
39 val map_term_names_in_atp_proof : |
39 val map_term_names_in_atp_proof : |
40 (string -> string) -> string proof -> string proof |
40 (string -> string) -> string proof -> string proof |
41 val nasty_atp_proof : string Symtab.table -> string proof -> string proof |
41 val nasty_atp_proof : string Symtab.table -> string proof -> string proof |
78 String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^ |
78 String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^ |
79 String.extract (s, size s - (threshold + 1) div 2 + 6, NONE) |
79 String.extract (s, size s - (threshold + 1) div 2 + 6, NONE) |
80 else |
80 else |
81 s |
81 s |
82 fun short_output verbose output = |
82 fun short_output verbose output = |
83 if verbose then elide_string 1000 output else "" |
83 if verbose then |
|
84 if output = "" then "No details available" else elide_string 1000 output |
|
85 else |
|
86 "" |
84 |
87 |
85 val missing_message_tail = |
88 val missing_message_tail = |
86 " appears to be missing. You will need to install it if you want to invoke \ |
89 " appears to be missing. You will need to install it if you want to invoke \ |
87 \remote provers." |
90 \remote provers." |
88 |
91 |
152 fun extract_known_failure known_failures output = |
155 fun extract_known_failure known_failures output = |
153 known_failures |
156 known_failures |
154 |> find_first (fn (_, pattern) => String.isSubstring pattern output) |
157 |> find_first (fn (_, pattern) => String.isSubstring pattern output) |
155 |> Option.map fst |
158 |> Option.map fst |
156 |
159 |
157 fun extract_tstplike_proof_and_outcome verbose complete res_code proof_delims |
160 fun extract_tstplike_proof_and_outcome debug verbose complete res_code |
158 known_failures output = |
161 proof_delims known_failures output = |
159 case extract_known_failure known_failures output of |
162 case extract_known_failure known_failures output of |
160 NONE => (case extract_tstplike_proof proof_delims output of |
163 NONE => |
161 "" => ("", SOME (if res_code = 0 andalso output = "" then |
164 (case extract_tstplike_proof proof_delims output of |
162 ProofMissing |
165 "" => |
163 else |
166 ("", SOME (if res_code = 0 andalso (not debug orelse output = "") then |
164 UnknownError (short_output verbose output))) |
167 ProofMissing |
165 | tstplike_proof => |
168 else |
166 if res_code = 0 then (tstplike_proof, NONE) |
169 UnknownError (short_output verbose output))) |
167 else ("", SOME (UnknownError (short_output verbose output)))) |
170 | tstplike_proof => |
|
171 if res_code = 0 then (tstplike_proof, NONE) |
|
172 else ("", SOME (UnknownError (short_output verbose output)))) |
168 | SOME failure => |
173 | SOME failure => |
169 ("", SOME (if failure = IncompleteUnprovable andalso complete then |
174 ("", SOME (if failure = IncompleteUnprovable andalso complete then |
170 Unprovable |
175 Unprovable |
171 else |
176 else |
172 failure)) |
177 failure)) |