reverted to explicitly check the presence of a refutation
(compare to 479a2fce65e6);
simplified handling of errors in remote script

--- a/contrib/SystemOnTPTP/remote	Fri Apr 03 18:03:29 2009 +0200
+++ b/contrib/SystemOnTPTP/remote	Sat Apr 04 20:22:39 2009 +0200
@@ -26,18 +26,20 @@
 getopts("hws:t:c:",\%Options);
 
 #----Usage
+sub usage() {
+  print("Usage: remote [<options>] <File name>\n");
+  print("    <options> are ...\n");
+  print("    -h            - print this help\n");
+  print("    -w            - list available ATP systems\n");
+  print("    -s<system>    - specified system to use\n");
+  print("    -t<timelimit> - CPU time limit for system\n");
+  print("    -c<command>   - custom command for system\n");
+  print("    <File name>   - TPTP problem file\n");
+  exit(0);
+}
 if (exists($Options{'h'})) {
-    print("Usage: remote <options> [<File name>]\n");
-    print("    <options> are ...\n");
-    print("    -h            - print this help\n");
-    print("    -w            - list available ATP systems\n");
-    print("    -s<system>    - specified system to use\n");
-    print("    -t<timelimit> - CPU time limit for system\n");
-    print("    -c<command>   - custom command for system\n");
-    print("    <File name>   - TPTP problem file\n");
-    exit(0);
+  usage();
 }
-
 #----What systems flag
 if (exists($Options{'w'})) {
     $URLParameters{"SubmitButton"} = "ListSystems";
@@ -67,7 +69,9 @@
     if (scalar(@ARGV) >= 1) {
         $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
     } else {
-die("Missing problem file");
+      print("Missing problem file\n");
+      usage();
+      die;
     }
 }
 
@@ -88,38 +92,29 @@
 } elsif (exists($Options{'w'})) {
   print $Response->content;
   exit (0);
-} elsif ($Response->content =~ /NO SOLUTION OUTPUT BY SYSTEM/){
-  print "No Solution Output by System\n";
-  exit(-1);
-} elsif ($Response->content =~ /ERROR: Could not form TPTP format derivation/) {
-  print "Could not form TPTP format derivation\n";
-  exit(-1);
 } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
   print "Specified System $1 does not exist\n";
   exit(-1);
-} elsif ($Response->content =~ /^\s*$/) {
-  print "Empty response (specified bad system? Inappropriate problem file format?)\n";
-  exit(-1);
-} elsif ($Response->content !~ /%\s*Result\s*:(.*)\n%\s*Output\s*:(.*)\n%/) {
-  print "Bad response: \n".$Response->content;
-  exit(-1);
+} elsif ($Response->content =~ /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/) {
+  my @lines = split( /\n/, $Response->content);
+  my $extract = "";
+  foreach my $line (@lines){
+      #ignore comments
+      if ($line !~ /^%/ && !($line eq "")) {
+          $extract .= "$line";
+      }
+  }
+  # insert newlines after ').'
+  $extract =~ s/\s//g;
+  $extract =~ s/\)\.cnf/\)\.\ncnf/g;
+
+  # orientation for res_reconstruct.ML
+  print "# SZS output start CNFRefutation.\n";
+  print "$extract\n";
+  print "# SZS output end CNFRefutation.\n";
+  exit(0);
 } else {
-    my @lines = split( /\n/, $Response->content);
-    my $extract = "";
-    foreach my $line (@lines){
-        #ignore comments
-        if ($line !~ /^%/ && !($line eq "")) {
-            $extract .= "$line";
-        }
-    }
-    # insert newlines after ').'
-    $extract =~ s/\s//g;
-    $extract =~ s/\)\.cnf/\)\.\ncnf/g;
-    
-    # orientation for res_reconstruct.ML
-    print "# SZS output start CNFRefutation.\n";
-    print "$extract\n";
-    print "# SZS output end CNFRefutation.\n";
-    exit(0);
+  print "Remote-script could not extract proof:\n".$Response->content;
+  exit(-1);
 }
 

--- a/src/HOL/Tools/atp_wrapper.ML	Fri Apr 03 18:03:29 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML	Sat Apr 04 20:22:39 2009 +0200
@@ -102,7 +102,7 @@
     (ResAtp.get_relevant max_new theory_const goal n)
     (ResAtp.write_problem_file false)
     command
-    ResReconstruct.find_failure_e_vamp_spass
+    ResReconstruct.find_failure
     (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
     timeout n goal;
 
@@ -166,7 +166,7 @@
   (ResAtp.write_problem_file true)
   (Path.explode "$SPASS_HOME/SPASS",
     "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)
-  ResReconstruct.find_failure_e_vamp_spass
+  ResReconstruct.find_failure
   ResReconstruct.lemma_list_dfg
   timeout n goal;
 

--- a/src/HOL/Tools/res_reconstruct.ML	Fri Apr 03 18:03:29 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Sat Apr 04 20:22:39 2009 +0200
@@ -15,7 +15,7 @@
   val strip_prefix: string -> string -> string option
   val setup: Context.theory -> Context.theory
   (* extracting lemma list*)
-  val find_failure_e_vamp_spass: string -> string option
+  val find_failure: string -> string option
   val lemma_list_dfg: string * string vector * Proof.context * Thm.thm * int -> string
   val lemma_list_tstp: string * string vector * Proof.context * Thm.thm * int -> string
   (* structured proofs *)
@@ -459,14 +459,16 @@
     
   (* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
   
-  val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable","SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"];
+  val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable",
+    "SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"];
   val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
-  val failure_strings_SPASS = ["SPASS beiseite: Completion found.","SPASS beiseite: Ran out of time.",
-  "SPASS beiseite: Maximal number of loops exceeded."];
-  fun find_failure_e_vamp_spass proof =
+  val failure_strings_SPASS = ["SPASS beiseite: Completion found.",
+    "SPASS beiseite: Ran out of time.", "SPASS beiseite: Maximal number of loops exceeded."];
+  val failure_strings_remote = ["Remote-script could not extract proof"];
+  fun find_failure proof =
     let val failures =
       map_filter (fn s => if String.isSubstring s proof then SOME s else NONE) 
-         (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS)
+         (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote)
     in if null failures then NONE else SOME (hd failures) end;
     
   (*=== EXTRACTING PROOF-TEXT === *)