203 fun the_system name versions = |
203 fun the_system name versions = |
204 case get_system name versions of |
204 case get_system name versions of |
205 SOME sys => sys |
205 SOME sys => sys |
206 | NONE => error ("System " ^ quote name ^ " not available at SystemOnTPTP.") |
206 | NONE => error ("System " ^ quote name ^ " not available at SystemOnTPTP.") |
207 |
207 |
|
208 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *) |
|
209 |
208 fun remote_config system_name system_versions proof_delims known_failures |
210 fun remote_config system_name system_versions proof_delims known_failures |
209 default_max_relevant use_conjecture_for_hypotheses |
211 default_max_relevant use_conjecture_for_hypotheses |
210 : atp_config = |
212 : atp_config = |
211 {exec = ("ISABELLE_ATP", "scripts/remote_atp"), |
213 {exec = ("ISABELLE_ATP", "scripts/remote_atp"), |
212 required_execs = [], |
214 required_execs = [], |
213 arguments = fn _ => fn timeout => |
215 arguments = fn _ => fn timeout => |
214 " -t " ^ string_of_int (to_secs 0 timeout) ^ " -s " ^ |
216 " -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout))) |
215 the_system system_name system_versions, |
217 ^ " -s " ^ the_system system_name system_versions, |
216 has_incomplete_mode = false, |
218 has_incomplete_mode = false, |
217 proof_delims = insert (op =) tstp_proof_delims proof_delims, |
219 proof_delims = insert (op =) tstp_proof_delims proof_delims, |
218 known_failures = |
220 known_failures = |
219 known_failures @ known_perl_failures @ |
221 known_failures @ known_perl_failures @ |
220 [(TimedOut, "says Timeout")], |
222 [(TimedOut, "says Timeout")], |