# HG changeset patch # User wenzelm # Date 1615750166 -3600 # Node ID 1cc848548f219f890c4175a2994b5acb9755d711 # Parent 00b77365552e0708c82d19a6227bec339fd302f8 invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl); clarified inlined command-line; clarified errors: exception ERROR becomes UnknownError (it could stem from Scala function); diff -r 00b77365552e -r 1cc848548f21 src/HOL/Tools/ATP/system_on_tptp.ML --- a/src/HOL/Tools/ATP/system_on_tptp.ML Sun Mar 14 18:32:11 2021 +0100 +++ b/src/HOL/Tools/ATP/system_on_tptp.ML Sun Mar 14 20:29:26 2021 +0100 @@ -8,6 +8,7 @@ sig val get_url: unit -> string val list_systems: unit -> {url: string, systems: string list} + val run_system_encoded: string -> {output: string, timing: Time.time} val run_system: {system: string, problem: Path.T, extra: string, timeout: Time.time} -> {output: string, timing: Time.time} end @@ -23,12 +24,16 @@ val systems = trim_split_lines (\<^scala>\SystemOnTPTP.list_systems\ url) in {url = url, systems = systems} end -fun run_system {system, problem, extra, timeout} = - cat_strings0 - [get_url (), system, Isabelle_System.absolute_path problem, - extra, string_of_int (Time.toMilliseconds timeout)] +fun run_system_encoded args = + cat_strings0 [get_url (), args] |> \<^scala>\SystemOnTPTP.run_system\ |> split_strings0 |> (fn [output, timing] => {output = output, timing = Time.fromMilliseconds (Value.parse_int timing)}) +fun run_system {system, problem, extra, timeout} = + cat_strings0 + [system, Isabelle_System.absolute_path problem, + extra, string_of_int (Time.toMilliseconds timeout)] + |> run_system_encoded + end diff -r 00b77365552e -r 1cc848548f21 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Sun Mar 14 18:32:11 2021 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Sun Mar 14 20:29:26 2021 +0100 @@ -46,6 +46,7 @@ val spass_H2NuVS0Red2 : string val spass_H2SOS : string val is_vampire_noncommercial_license_accepted : unit -> bool option + val isabelle_scala_function: string list * string list val remote_atp : string -> string -> string list -> (string * string) list -> (atp_failure * string) list -> atp_formula_role -> (Proof.context -> slice_spec * string) -> string * (unit -> atp_config) @@ -615,13 +616,15 @@ val max_remote_secs = 1000 (* give Geoff Sutcliffe's servers a break *) +val isabelle_scala_function = (["SCALA_HOME"], ["bin/scala"]) + fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice = - {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]), + {exec = isabelle_scala_function, arguments = fn _ => fn _ => fn command => fn timeout => fn problem => fn _ => - (if command <> "" then "-c " ^ quote command ^ " " else "") ^ - "-s " ^ the_remote_system system_name system_versions ^ " " ^ - "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^ - " " ^ File.bash_path problem, + (cat_strings0 + [the_remote_system system_name system_versions, + Isabelle_System.absolute_path problem, + command, string_of_int (Int.min (max_remote_secs, to_secs 1 timeout) * 1000)]), proof_delims = union (op =) tstp_proof_delims proof_delims, known_failures = known_failures @ known_perl_failures @ known_says_failures, prem_role = prem_role, diff -r 00b77365552e -r 1cc848548f21 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sun Mar 14 18:32:11 2021 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sun Mar 14 20:29:26 2021 +0100 @@ -158,7 +158,7 @@ Path.explode dest_dir + problem_file_name else error ("No such directory: " ^ quote dest_dir) - val command0 = + val executable = (case find_first (fn var => getenv var <> "") (fst exec) of SOME var => let @@ -264,20 +264,27 @@ val ord = effective_term_order ctxt name val args = arguments ctxt full_proofs extra slice_timeout prob_path (ord, ord_info, sel_weights) - val command = "exec 2>&1; " ^ File.bash_path command0 ^ " " ^ args + val command = File.bash_path executable ^ " " ^ args + + fun run_command () = + if exec = isabelle_scala_function then + let val {output, timing} = SystemOnTPTP.run_system_encoded args + in (output, timing) end + else + let val res = Isabelle_System.bash_process ("exec 2>&1; " ^ command) + in (Process_Result.out res, Process_Result.timing_elapsed res) end val _ = atp_problem |> lines_of_atp_problem format ord ord_info - |> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) + |> (exec <> isabelle_scala_function) ? + cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |> File.write_list prob_path val ((output, run_time), (atp_proof, outcome)) = - Timeout.apply generous_slice_timeout Isabelle_System.bash_process command - |> (fn res => - (Process_Result.out res |> - (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I), - Process_Result.timing_elapsed res)) + Timeout.apply generous_slice_timeout run_command () + |>> overlord ? + (fn output => prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") output) |> (fn accum as (output, _) => (accum, extract_tstplike_proof_and_outcome verbose proof_delims known_failures output @@ -285,6 +292,7 @@ atp_problem handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable))) handle Timeout.TIMEOUT _ => (("", slice_timeout), ([], SOME TimedOut)) + | ERROR msg => (("", Time.zeroTime), ([], SOME (UnknownError msg))) val outcome = (case outcome of