# HG changeset patch
# User blanchet
# Date 1292408789 -3600
# Node ID f5229ab54284933d87df88a64138ad4ee77b1586
# Parent  0e19032737121e5c5855b6604b316615eb84a834
added timeout max for remote server invocation

diff -r 0e1903273712 -r f5229ab54284 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Dec 15 11:26:29 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Dec 15 11:26:29 2010 +0100
@@ -205,14 +205,16 @@
     SOME sys => sys
   | NONE => error ("System " ^ quote name ^ " not available at SystemOnTPTP.")
 
+val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
+
 fun remote_config system_name system_versions proof_delims known_failures
                   default_max_relevant use_conjecture_for_hypotheses
                   : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    required_execs = [],
    arguments = fn _ => fn timeout =>
-     " -t " ^ string_of_int (to_secs 0 timeout) ^ " -s " ^
-     the_system system_name system_versions,
+     " -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
+     ^ " -s " ^ the_system system_name system_versions,
    has_incomplete_mode = false,
    proof_delims = insert (op =) tstp_proof_delims proof_delims,
    known_failures =