--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 29 10:25:53 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 29 10:36:36 2010 +0200
@@ -33,8 +33,8 @@
axiom_clauses: ((string * int) * thm) list option,
filtered_clauses: ((string * int) * thm) list option}
datatype failure =
- Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
- MalformedInput | MalformedOutput | UnknownError
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
+ OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
type prover_result =
{outcome: failure option,
message: string,
@@ -102,8 +102,8 @@
filtered_clauses: ((string * int) * thm) list option}
datatype failure =
- Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
- MalformedInput | MalformedOutput | UnknownError
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
+ OldSpass | MalformedInput | MalformedOutput | UnknownError
type prover_result =
{outcome: failure option,
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 29 10:25:53 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 29 10:36:36 2010 +0200
@@ -95,6 +95,7 @@
fun string_for_failure Unprovable = "The ATP problem is unprovable."
| string_for_failure IncompleteUnprovable =
"The ATP cannot prove the problem."
+ | string_for_failure CantConnect = "Can't connect to remote ATP."
| string_for_failure TimedOut = "Timed out."
| string_for_failure OutOfResources = "The ATP ran out of resources."
| string_for_failure OldSpass =
@@ -465,7 +466,8 @@
case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of
(answer, 0) => split_lines answer
| (answer, _) =>
- error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
+ error ("Failed to get available systems at SystemOnTPTP:\n" ^
+ perhaps (try (unsuffix "\n")) answer)
fun refresh_systems_on_tptp () =
Synchronized.change systems (fn _ => get_systems ())
@@ -480,7 +482,8 @@
| SOME sys => sys);
val remote_known_failures =
- [(TimedOut, "says Timeout"),
+ [(CantConnect, "HTTP-Error"),
+ (TimedOut, "says Timeout"),
(MalformedOutput, "Remote script could not extract proof")]
fun remote_config atp_prefix args