# HG changeset patch # User immler@in.tum.de # Date 1237040144 -3600 # Node ID 0ac3db5a59a8ad820435ffe570a995ed8b0e8ad3 # Parent ea4dabfea029dacf8a3f4ac4b6a71bb617cef592 removed connection check; adapted times diff -r ea4dabfea029 -r 0ac3db5a59a8 contrib/SystemOnTPTP/remote --- a/contrib/SystemOnTPTP/remote Sat Mar 14 12:51:13 2009 +0100 +++ b/contrib/SystemOnTPTP/remote Sat Mar 14 15:15:44 2009 +0100 @@ -21,16 +21,6 @@ "ProblemSource" => "UPLOAD", ); -# check connection -my $TestAgent = LWP::UserAgent->new; -$TestAgent->timeout(5); -my $TestRequest = GET($SystemOnTPTPFormReplyURL); -my $TestResponse = $TestAgent->request($TestRequest); -if(! $TestResponse->is_success) { - print "HTTP-Error: " . $TestResponse->message . "\n"; - exit(-1); -} - #----Get format and transform options if specified my %Options; getopts("hws:t:c:",\%Options); @@ -85,7 +75,7 @@ my $Agent = LWP::UserAgent->new; if (exists($Options{'t'})) { # give server more time to respond - $Agent->timeout($Options{'t'} * 2 + 10); + $Agent->timeout($Options{'t'} + 10); } my $Request = POST($SystemOnTPTPFormReplyURL, Content_Type => 'form-data',Content => \%URLParameters); diff -r ea4dabfea029 -r 0ac3db5a59a8 src/HOL/Tools/atp_wrapper.ML --- a/src/HOL/Tools/atp_wrapper.ML Sat Mar 14 12:51:13 2009 +0100 +++ b/src/HOL/Tools/atp_wrapper.ML Sat Mar 14 15:15:44 2009 +0100 @@ -165,7 +165,7 @@ fun remote_prover_opts max_new theory_const args timeout = tptp_prover_opts max_new theory_const - (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", args ^ " -t " ^ string_of_int timeout) + (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", args ^ " -t " ^ string_of_int (timeout - 10)) timeout; val remote_prover = remote_prover_opts 60 false;