# HG changeset patch
# User immler@in.tum.de
# Date 1231773365 -3600
# Node ID 96599d8d8268ecc1f7ab9c50950ef7b10fbba852
# Parent  b81ae415873d7f3c85f68aef8e23e687ca8e95d9
simplified usage of remote-script; added compatible remote-atps

diff -r b81ae415873d -r 96599d8d8268 contrib/SystemOnTPTP/remote
--- a/contrib/SystemOnTPTP/remote	Sun Jan 11 21:50:05 2009 +0100
+++ b/contrib/SystemOnTPTP/remote	Mon Jan 12 16:16:05 2009 +0100
@@ -3,14 +3,18 @@
 # Wrapper for custom remote provers on SystemOnTPTP
 # Author: Fabian Immler, TU Muenchen
 #
-# Similar to the vampire wrapper, but compatible provers can be passed in the
-# command line, with %s for the problemfile e.g. 
+# Usage: ./remote prover timelimit problemfile
+# 
+# where prover should be the name of the System from http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP
+# tested and working with the standard settings: 
 #
-# ./remote Vampire---9.0 jumpirefix --output_syntax tptp --mode casc -t 3600 %s
-# ./remote Vampire---10.0 drakosha.pl 60 %s
-# ./remote SPASS---3.01 SPASS -Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof %s
-# ./remote Metis---2.1 metis --show proof --show saturation %s
-# ./remote SNARK---20080805r005 run-snark %s
+# ./remote Vampire---9.0 timelimit file
+# ./remote SPASS---3.01 timelimit file
+# ./remote Metis---2.1 timelimit file
+# ./remote SNARK---20080805r005 timelimit file
+# ./remote Otter---3.3 timelimit file
+# ./remote SOS---2.0 timelimit file
+# ./remote EP---1.0 timelimit file
 
 use warnings;
 use strict;
@@ -22,19 +26,12 @@
 # address of proof-server
 my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
 
-if(scalar(@ARGV) < 2) {
-    print "prover and command missing";
+if(scalar(@ARGV) != 3) {
+    print "usage: ";
     exit -1;
 }
 my $prover = shift(@ARGV);
-my $command = shift(@ARGV);
-
-# pass arguments
-my $options = "";
-while(scalar(@ARGV)>1){
-	$options.=" ".shift(@ARGV);
-}
-# last argument is problemfile to be uploaded
+my $timelimit = shift(@ARGV);
 my $problem = [shift(@ARGV)];
 
 # fill in form
@@ -46,8 +43,7 @@
     "ProblemSource" => "UPLOAD",
     "UPLOADProblem" => $problem,
     "System___$prover" => "$prover",
-    "Format___$prover" => "tptp",
-    "Command___$prover" => "$command $options %s"
+    "TimeLimit___$prover" => "$timelimit",
 );
 
 # Query Server
@@ -89,6 +85,7 @@
     print "# SZS output end CNFRefutation.\n";
 } else {
 	print "HTTP-Request: " . $Response->message;
+	print "\nResponse: " . $Response->content;
 	print "\nCANNOT PROVE: \n";
   print $Response->content;
 }
diff -r b81ae415873d -r 96599d8d8268 src/HOL/ATP_Linkup.thy
--- a/src/HOL/ATP_Linkup.thy	Sun Jan 11 21:50:05 2009 +0100
+++ b/src/HOL/ATP_Linkup.thy	Mon Jan 12 16:16:05 2009 +0100
@@ -113,9 +113,20 @@
 
 text {* remote provers via SystemOnTPTP *}
 setup {* AtpManager.add_prover "remote_vamp9"
-  (AtpWrapper.remote_prover "Vampire---9.0" "jumpirefix --output_syntax tptp --mode casc -t 3600") *}
-setup {* AtpManager.add_prover "remote_vamp10"
-  (AtpWrapper.remote_prover "Vampire---10.0" "drakosha.pl 60") *}
+  (AtpWrapper.remote_prover "Vampire---9.0" 90) *}
+setup {* AtpManager.add_prover "remote_spass"
+  (AtpWrapper.remote_prover "SPASS---3.01" 90) *}
+setup {* AtpManager.add_prover "remote_metis"
+  (AtpWrapper.remote_prover "Metis---2.1" 90) *}
+setup {* AtpManager.add_prover "remote_snark"
+  (AtpWrapper.remote_prover "SNARK---20080805r005" 90) *}
+setup {* AtpManager.add_prover "remote_otter"
+  (AtpWrapper.remote_prover "Otter---3.3" 90) *}
+setup {* AtpManager.add_prover "remote_e"
+  (AtpWrapper.remote_prover "EP---1.0" 90) *}
+setup {* AtpManager.add_prover "remote_sos"
+  (AtpWrapper.remote_prover "SOS---2.0" 90) *}
+  
 
 
 subsection {* The Metis prover *}
diff -r b81ae415873d -r 96599d8d8268 src/HOL/Tools/atp_wrapper.ML
--- a/src/HOL/Tools/atp_wrapper.ML	Sun Jan 11 21:50:05 2009 +0100
+++ b/src/HOL/Tools/atp_wrapper.ML	Mon Jan 12 16:16:05 2009 +0100
@@ -30,8 +30,8 @@
   val eprover_full: AtpManager.prover
   val spass_opts: int -> bool  -> AtpManager.prover
   val spass: AtpManager.prover
-  val remote_prover_opts: int -> bool -> string -> string -> AtpManager.prover
-  val remote_prover: string -> string -> AtpManager.prover
+  val remote_prover_opts: int -> bool -> string -> int -> AtpManager.prover
+  val remote_prover: string -> int -> AtpManager.prover
 end;
 
 structure AtpWrapper: ATP_WRAPPER =
@@ -156,9 +156,9 @@
 
 (* remote prover invocation via SystemOnTPTP *)
 
-fun remote_prover_opts max_new theory_const name command =
+fun remote_prover_opts max_new theory_const name timelimit =
   tptp_prover_opts max_new theory_const
-  (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ command);
+  (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ (string_of_int timelimit));
 
 val remote_prover = remote_prover_opts 60 false;