--- 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);
--- 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;