44 val spass_H2LR0LT0 : string |
44 val spass_H2LR0LT0 : string |
45 val spass_H2NuVS0 : string |
45 val spass_H2NuVS0 : string |
46 val spass_H2NuVS0Red2 : string |
46 val spass_H2NuVS0Red2 : string |
47 val spass_H2SOS : string |
47 val spass_H2SOS : string |
48 val is_vampire_noncommercial_license_accepted : unit -> bool option |
48 val is_vampire_noncommercial_license_accepted : unit -> bool option |
|
49 val isabelle_scala_function: string list * string list |
49 val remote_atp : string -> string -> string list -> (string * string) list -> |
50 val remote_atp : string -> string -> string list -> (string * string) list -> |
50 (atp_failure * string) list -> atp_formula_role -> (Proof.context -> slice_spec * string) -> |
51 (atp_failure * string) list -> atp_formula_role -> (Proof.context -> slice_spec * string) -> |
51 string * (unit -> atp_config) |
52 string * (unit -> atp_config) |
52 val add_atp : string * (unit -> atp_config) -> theory -> theory |
53 val add_atp : string * (unit -> atp_config) -> theory -> theory |
53 val get_atp : theory -> string -> (unit -> atp_config) |
54 val get_atp : theory -> string -> (unit -> atp_config) |
613 error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n(Available systems: " ^ |
614 error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n(Available systems: " ^ |
614 commas_quote syss ^ ".)"))) |
615 commas_quote syss ^ ".)"))) |
615 |
616 |
616 val max_remote_secs = 1000 (* give Geoff Sutcliffe's servers a break *) |
617 val max_remote_secs = 1000 (* give Geoff Sutcliffe's servers a break *) |
617 |
618 |
|
619 val isabelle_scala_function = (["SCALA_HOME"], ["bin/scala"]) |
|
620 |
618 fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice = |
621 fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice = |
619 {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]), |
622 {exec = isabelle_scala_function, |
620 arguments = fn _ => fn _ => fn command => fn timeout => fn problem => fn _ => |
623 arguments = fn _ => fn _ => fn command => fn timeout => fn problem => fn _ => |
621 (if command <> "" then "-c " ^ quote command ^ " " else "") ^ |
624 (cat_strings0 |
622 "-s " ^ the_remote_system system_name system_versions ^ " " ^ |
625 [the_remote_system system_name system_versions, |
623 "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^ |
626 Isabelle_System.absolute_path problem, |
624 " " ^ File.bash_path problem, |
627 command, string_of_int (Int.min (max_remote_secs, to_secs 1 timeout) * 1000)]), |
625 proof_delims = union (op =) tstp_proof_delims proof_delims, |
628 proof_delims = union (op =) tstp_proof_delims proof_delims, |
626 known_failures = known_failures @ known_perl_failures @ known_says_failures, |
629 known_failures = known_failures @ known_perl_failures @ known_says_failures, |
627 prem_role = prem_role, |
630 prem_role = prem_role, |
628 best_slices = fn ctxt => [(1.0, best_slice ctxt)], |
631 best_slices = fn ctxt => [(1.0, best_slice ctxt)], |
629 best_max_mono_iters = default_max_mono_iters, |
632 best_max_mono_iters = default_max_mono_iters, |