# HG changeset patch # User immler@in.tum.de # Date 1232393050 -3600 # Node ID 1f007b7b8ad3b7cf5a52d84924b6f8c020d1c064 # Parent 3f8b24fcfbd6a6d89fd00bddf71ee93ceb52d874# Parent 6cccea7c94d4e4dc8f2a1815c869b5db18325071 Automated merge with http://isabelle.in.tum.de/repos/isabelle/tip diff -r 3f8b24fcfbd6 -r 1f007b7b8ad3 contrib/SystemOnTPTP/remote --- a/contrib/SystemOnTPTP/remote Mon Jan 19 20:05:41 2009 +0100 +++ b/contrib/SystemOnTPTP/remote Mon Jan 19 20:24:10 2009 +0100 @@ -3,14 +3,14 @@ # 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 EP---1.0 timelimit file use warnings; use strict; @@ -22,19 +22,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 +39,7 @@ "ProblemSource" => "UPLOAD", "UPLOADProblem" => $problem, "System___$prover" => "$prover", - "Format___$prover" => "tptp", - "Command___$prover" => "$command $options %s" + "TimeLimit___$prover" => "$timelimit", ); # Query Server @@ -89,6 +81,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 3f8b24fcfbd6 -r 1f007b7b8ad3 src/HOL/ATP_Linkup.thy --- a/src/HOL/ATP_Linkup.thy Mon Jan 19 20:05:41 2009 +0100 +++ b/src/HOL/ATP_Linkup.thy Mon Jan 19 20:24:10 2009 +0100 @@ -113,9 +113,12 @@ 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_e" + (AtpWrapper.remote_prover "EP---1.0" 90) *} + subsection {* The Metis prover *} diff -r 3f8b24fcfbd6 -r 1f007b7b8ad3 src/HOL/Tools/atp_wrapper.ML --- a/src/HOL/Tools/atp_wrapper.ML Mon Jan 19 20:05:41 2009 +0100 +++ b/src/HOL/Tools/atp_wrapper.ML Mon Jan 19 20:24:10 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;