handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on

--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Jul 28 22:18:35 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Jul 28 23:01:27 2010 +0200
@@ -9,7 +9,8 @@
 sig
   datatype failure =
     Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
-    OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
+    OutOfResources | OldSpass | NoPerl | NoLibwwwPerl | MalformedInput |
+    MalformedOutput | UnknownError
 
   type prover_config =
     {executable: string * string,
@@ -21,6 +22,9 @@
      prefers_theory_relevant: bool,
      explicit_forall: bool}
 
+  val string_for_failure : failure -> string
+  val known_failure_in_output :
+    string -> (failure * string) list -> failure option
   val add_prover: string * prover_config -> theory -> theory
   val get_prover: theory -> string -> prover_config
   val available_atps: theory -> unit
@@ -35,8 +39,9 @@
 (* prover configuration *)
 
 datatype failure =
-  Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
-  OldSpass | MalformedInput | MalformedOutput | UnknownError
+    Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
+    OutOfResources | OldSpass | NoPerl | NoLibwwwPerl | MalformedInput |
+    MalformedOutput | UnknownError
 
 type prover_config =
   {executable: string * string,
@@ -48,6 +53,42 @@
    prefers_theory_relevant: bool,
    explicit_forall: bool}
 
+val missing_message_tail =
+  " appears to be missing. You will need to install it if you want to run \
+  \ATPs remotely."
+
+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 =
+    "Warning: Isabelle requires a more recent version of SPASS with \
+    \support for the TPTP syntax. To install it, download and untar the \
+    \package \"http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/contrib/\
+    \spass-3.7.tar.gz\" and add the \"spass-3.7\" directory's absolute path \
+    \to " ^
+    quote (Path.implode (Path.expand (Path.appends
+               (Path.variable "ISABELLE_HOME_USER" ::
+                map Path.basic ["etc", "components"])))) ^
+    " on a line of its own."
+  | string_for_failure NoPerl = "Perl" ^ missing_message_tail
+  | string_for_failure NoLibwwwPerl =
+    "The Perl module \"libwww-perl\"" ^ missing_message_tail
+  | string_for_failure MalformedInput =
+    "Internal Isabelle error: The ATP problem is malformed. Please report \
+    \this to the Isabelle developers."
+  | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
+  | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
+
+fun known_failure_in_output output =
+  find_first (fn (_, pattern) => String.isSubstring pattern output)
+  #> Option.map fst
+
+val known_perl_failures =
+  [(NoPerl, "env: perl"),
+   (NoLibwwwPerl, "HTTP")]
 
 (* named provers *)
 
@@ -118,6 +159,7 @@
      |> not complete ? prefix "-SOS=1 ",
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
+     known_perl_failures @
      [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
       (TimedOut, "SPASS beiseite: Ran out of time"),
       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
@@ -154,14 +196,16 @@
 
 (* Remote prover invocation via SystemOnTPTP *)
 
-val systems = Synchronized.var "atp_systems" ([]: string list)
+val systems = Synchronized.var "atp_systems" ([] : string list)
 
 fun get_systems () =
-  case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w" of
+  case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
     (answer, 0) => split_lines answer
   | (answer, _) =>
     error ("Failed to get available systems at SystemOnTPTP:\n" ^
-           perhaps (try (unsuffix "\n")) answer)
+           (case known_failure_in_output answer known_perl_failures of
+              SOME failure => string_for_failure failure
+            | NONE => perhaps (try (unsuffix "\n")) answer))
 
 fun refresh_systems_on_tptp () =
   Synchronized.change systems (fn _ => get_systems ())
@@ -175,11 +219,6 @@
     NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.")
   | SOME sys => sys);
 
-val remote_known_failures =
-  [(CantConnect, "HTTP-Error"),
-   (TimedOut, "says Timeout"),
-   (MalformedOutput, "Remote script could not extract proof")]
-
 fun remote_config atp_prefix
         ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
           prefers_theory_relevant, explicit_forall, ...} : prover_config)
@@ -190,7 +229,10 @@
      " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
      the_system atp_prefix,
    proof_delims = insert (op =) tstp_proof_delims proof_delims,
-   known_failures = remote_known_failures @ known_failures,
+   known_failures =
+     known_failures @ known_perl_failures @
+     [(CantConnect, "HTTP-Error"),
+      (TimedOut, "says Timeout")],
    max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
    prefers_theory_relevant = prefers_theory_relevant,
    explicit_forall = explicit_forall}

--- a/src/HOL/Tools/ATP/scripts/remote_atp	Wed Jul 28 22:18:35 2010 +0200
+++ b/src/HOL/Tools/ATP/scripts/remote_atp	Wed Jul 28 23:01:27 2010 +0200
@@ -101,7 +101,7 @@
   print $Response->content;
   exit (0);
 } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
-  print "Specified System $1 does not exist\n";
+  print "Specified system $1 does not exist\n";
   exit(-1);
 } else {
   print $Response->content;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Jul 28 22:18:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Jul 28 23:01:27 2010 +0200
@@ -148,42 +148,17 @@
 
 fun extract_proof_and_outcome complete res_code proof_delims known_failures
                               output =
-  case map_filter (fn (failure, pattern) =>
-                      if String.isSubstring pattern output then SOME failure
-                      else NONE) known_failures of
-    [] => (case extract_proof proof_delims output of
-             "" => ("", SOME UnknownError)
+  case known_failure_in_output output known_failures of
+    NONE => (case extract_proof proof_delims output of
+             "" => ("", SOME MalformedOutput)
            | proof => if res_code = 0 then (proof, NONE)
                       else ("", SOME UnknownError))
-  | (failure :: _) =>
+  | SOME failure =>
     ("", SOME (if failure = IncompleteUnprovable andalso complete then
                  Unprovable
                else
                  failure))
 
-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 =
-    (* FIXME: Change the error message below to point to the Isabelle download
-       page once the package is there. *)
-    "Warning: Sledgehammer requires a more recent version of SPASS with \
-    \support for the TPTP syntax. To install it, download and untar the \
-    \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \
-    \\"spass-3.7\" directory's full path to \"" ^
-    Path.implode (Path.expand (Path.appends
-        (Path.variable "ISABELLE_HOME_USER" ::
-         map Path.basic ["etc", "components"]))) ^
-    "\" on a line of its own."
-  | string_for_failure MalformedInput =
-    "Internal Sledgehammer error: The ATP problem is malformed. Please report \
-    \this to the Isabelle developers."
-  | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
-  | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
-
 
 (* Clause preparation *)