better workaround for E's off-by-one-second issue

--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 24 20:09:30 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 24 21:40:03 2010 +0200
@@ -125,10 +125,20 @@
   priority ("Available ATPs: " ^
             commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
 
-fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
+fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000
 
 (* E prover *)
 
+(* Give older versions of E an extra second, because the "eproof" script wrongly
+   subtracted an entire second to account for the overhead of the script
+   itself, which is in fact much lower. *)
+fun e_bonus () =
+  case getenv "E_VERSION" of
+    "" => 1000
+  | version =>
+    if exists (fn s => String.isPrefix s version) ["0.9", "1.0"] then 1000
+    else 0
+
 val tstp_proof_delims =
   ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
 
@@ -137,8 +147,7 @@
    required_execs = [],
    arguments = fn _ => fn timeout =>
      "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent \
-     \--soft-cpu-limit=" ^
-     string_of_int (to_generous_secs timeout),
+     \--cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout),
    has_incomplete_mode = false,
    proof_delims = [tstp_proof_delims],
    known_failures =
@@ -165,7 +174,7 @@
    required_execs = [("SPASS_HOME", "SPASS")],
    arguments = fn complete => fn timeout =>
      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
-      \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout))
+      \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
      |> not complete ? prefix "-SOS=1 ",
    has_incomplete_mode = true,
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
@@ -191,7 +200,7 @@
   {exec = ("VAMPIRE_HOME", "vampire"),
    required_execs = [],
    arguments = fn _ => fn timeout =>
-     "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
+     "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
      " --thanks Andrei --input_file",
    has_incomplete_mode = false,
    proof_delims =
@@ -251,7 +260,7 @@
   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    required_execs = [],
    arguments = fn _ => fn timeout =>
-     " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
+     " -t " ^ string_of_int (to_secs 0 timeout) ^ " -s " ^
      the_system system_name system_versions,
    has_incomplete_mode = false,
    proof_delims = insert (op =) tstp_proof_delims proof_delims,