# HG changeset patch
# User blanchet
# Date 1284042456 -7200
# Node ID e2a3c435334bd04630acb76f9f635fda877e8d16
# Parent  bdfcf243460190dd9adaa7acfb52ef0af16e99b4
more precise error messages when Vampire is interrupted or SPASS runs into an internal bug

diff -r bdfcf2434601 -r e2a3c435334b src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Sep 09 16:06:11 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Sep 09 16:27:36 2010 +0200
@@ -10,7 +10,8 @@
   datatype failure =
     Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
     OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
-    MalformedInput | MalformedOutput | Interrupted | UnknownError
+    MalformedInput | MalformedOutput | Interrupted | InternalError |
+    UnknownError
 
   type prover_config =
     {exec: string * string,
@@ -42,7 +43,7 @@
 datatype failure =
   Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
   SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput |
-  MalformedOutput | Interrupted | UnknownError
+  MalformedOutput | Interrupted | InternalError | UnknownError
 
 type prover_config =
   {exec: string * string,
@@ -86,6 +87,7 @@
     \developers."
   | string_for_failure MalformedOutput = "The ATP output is malformed."
   | string_for_failure Interrupted = "The ATP was interrupted."
+  | string_for_failure InternalError = "An internal ATP error occurred."
   | string_for_failure UnknownError = "An unknown ATP error occurred."
 
 fun known_failure_in_output output =
@@ -183,7 +185,8 @@
       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
       (MalformedInput, "Undefined symbol"),
       (MalformedInput, "Free Variable"),
-      (SpassTooOld, "tptp2dfg")],
+      (SpassTooOld, "tptp2dfg"),
+      (InternalError, "Please report this error")],
    default_max_relevant = 350 (* FUDGE *),
    explicit_forall = true,
    use_conjecture_for_hypotheses = true}
@@ -212,7 +215,8 @@
       (TimedOut, "SZS status Timeout"),
       (Unprovable, "Satisfiability detected"),
       (Unprovable, "Termination reason: Satisfiable"),
-      (VampireTooOld, "not a valid option")],
+      (VampireTooOld, "not a valid option"),
+      (Interrupted, "Aborted by signal SIGINT")],
    default_max_relevant = 400 (* FUDGE *),
    explicit_forall = false,
    use_conjecture_for_hypotheses = true}
diff -r bdfcf2434601 -r e2a3c435334b src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Sep 09 16:06:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Sep 09 16:27:36 2010 +0200
@@ -165,7 +165,7 @@
              "" => ("", SOME (if res_code = 0 andalso output = "" then
                                 Interrupted
                               else
-                                UnknownError))
+                                 UnknownError))
            | proof => if res_code = 0 then (proof, NONE)
                       else ("", SOME UnknownError))
   | SOME failure =>