diff --git a/src/HOL/Tools/ATP/system_on_tptp.ML b/src/HOL/Tools/ATP/system_on_tptp.ML --- a/src/HOL/Tools/ATP/system_on_tptp.ML +++ b/src/HOL/Tools/ATP/system_on_tptp.ML @@ -1,32 +1,34 @@ (* Title: HOL/Tools/ATP/system_on_tptp.ML Author: Makarius Support for remote ATPs via SystemOnTPTP. *) signature SYSTEM_ON_TPTP = sig val get_url: unit -> string val list_systems: unit -> {url: string, systems: string list} - val run_system: {system: string, problem: string, extra: string, timeout: Time.time} -> + val run_system: {system: string, problem: Path.T, extra: string, timeout: Time.time} -> {output: string, timing: Time.time} end structure SystemOnTPTP: SYSTEM_ON_TPTP = struct fun get_url () = Options.default_string \<^system_option>\SystemOnTPTP\ fun list_systems () = let val url = get_url () 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, problem, extra, string_of_int (Time.toMilliseconds timeout)] + cat_strings0 + [get_url (), system, Isabelle_System.absolute_path problem, + extra, string_of_int (Time.toMilliseconds timeout)] |> \<^scala>\SystemOnTPTP.run_system\ |> split_strings0 |> (fn [output, timing] => {output = output, timing = Time.fromMilliseconds (Value.parse_int timing)}) end diff --git a/src/HOL/Tools/ATP/system_on_tptp.scala b/src/HOL/Tools/ATP/system_on_tptp.scala --- a/src/HOL/Tools/ATP/system_on_tptp.scala +++ b/src/HOL/Tools/ATP/system_on_tptp.scala @@ -1,85 +1,86 @@ /* Title: HOL/Tools/ATP/system_on_tptp.scala Author: Makarius Support for remote ATPs via SystemOnTPTP. */ package isabelle.atp import isabelle._ import java.net.URL object SystemOnTPTP { /* requests */ def get_url(options: Options): URL = Url(options.string("SystemOnTPTP")) def post_request( url: URL, parameters: List[(String, Any)], timeout: Time = HTTP.Client.default_timeout): HTTP.Content = { val parameters0 = List("NoHTML" -> 1, "QuietFlag" -> "-q0") .filterNot(p0 => parameters.exists(p => p0._1 == p._1)) try { HTTP.Client.post(url, parameters0 ::: parameters, timeout = timeout, user_agent = "Sledgehammer") } catch { case ERROR(msg) => cat_error("Failed to access SystemOnTPTP server", msg) } } /* list systems */ def list_systems(url: URL): HTTP.Content = post_request(url, List("SubmitButton" -> "ListSystems", "ListStatus" -> "READY")) object List_Systems extends Scala.Fun("SystemOnTPTP.list_systems", thread = true) { val here = Scala_Project.here def apply(url: String): String = list_systems(Url(url)).string } /* run system */ def run_system(url: URL, system: String, problem: String, extra: String = "", quiet: String = "01", timeout: Time = Time.seconds(60)): HTTP.Content = { val paramaters = List( "SubmitButton" -> "RunSelectedSystems", "ProblemSource" -> "FORMULAE", "FORMULAEProblem" -> problem, "ForceSystem" -> "-force", "System___" + system -> system, "TimeLimit___" + system -> timeout.seconds.ceil.toLong, "Command___" + system -> extra, "QuietFlag" -> ("-q" + quiet)) post_request(url, paramaters, timeout = timeout + Time.seconds(15)) } object Run_System extends Scala.Fun("SystemOnTPTP.run_system", thread = true) { val here = Scala_Project.here def apply(arg: String): String = { - val List(url, system, problem, extra, Value.Int(timeout)) = Library.split_strings0(arg) + val List(url, system, problem_path, extra, Value.Int(timeout)) = Library.split_strings0(arg) + val problem = File.read(Path.explode(problem_path)) val res = run_system(Url(url), system, problem, extra = extra, timeout = Time.ms(timeout)) val bad_prover = "WARNING: " + system + " does not exist" if (res.trim_split_lines.exists(_.startsWith(bad_prover))) { error("The ATP " + quote(system) + " is not available at SystemOnTPTP") } else Library.cat_strings0(List(res.string, res.elapsed_time.ms.toString)) } } } diff --git a/src/Pure/System/isabelle_system.ML b/src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML +++ b/src/Pure/System/isabelle_system.ML @@ -1,117 +1,118 @@ (* Title: Pure/System/isabelle_system.ML Author: Makarius Isabelle system support. *) signature ISABELLE_SYSTEM = sig val bash_process: string -> Process_Result.T val bash_output: string -> string * int val bash: string -> int val bash_functions: unit -> string list val check_bash_function: Proof.context -> string * Position.T -> string + val absolute_path: Path.T -> string val make_directory: Path.T -> Path.T val copy_dir: Path.T -> Path.T -> unit val copy_file: Path.T -> Path.T -> unit val copy_file_base: Path.T * Path.T -> Path.T -> unit val create_tmp_path: string -> string -> Path.T val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a val rm_tree: Path.T -> unit val with_tmp_dir: string -> (Path.T -> 'a) -> 'a val download: string -> Path.T -> unit end; structure Isabelle_System: ISABELLE_SYSTEM = struct (* bash *) fun bash_process script = Scala.function "bash_process" ("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script) |> split_strings0 |> (fn [] => raise Exn.Interrupt | [err] => error err | a :: b :: c :: d :: lines => let val rc = Value.parse_int a; val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c); val (out_lines, err_lines) = chop (Value.parse_int d) lines; in Process_Result.make {rc = rc, out_lines = out_lines, err_lines = err_lines, timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}} end | _ => raise Fail "Malformed Isabelle/Scala result"); val bash = bash_process #> Process_Result.print #> Process_Result.rc; fun bash_output s = let val res = bash_process s; val _ = warning (Process_Result.err res); in (Process_Result.out res, Process_Result.rc res) end; (* bash functions *) fun bash_functions () = bash_process "declare -Fx" |> Process_Result.check |> Process_Result.out_lines |> map_filter (space_explode " " #> try List.last); fun check_bash_function ctxt arg = Completion.check_entity Markup.bash_functionN (bash_functions () |> map (rpair Position.none)) ctxt arg; (* directory and file operations *) val absolute_path = Path.implode o File.absolute_path; fun scala_function0 name = ignore o Scala.function name o cat_strings0; fun scala_function name = scala_function0 name o map absolute_path; fun make_directory path = (scala_function "make_directory" [path]; path); fun copy_dir src dst = scala_function "copy_dir" [src, dst]; fun copy_file src dst = scala_function "copy_file" [src, dst]; fun copy_file_base (base_dir, src) target_dir = scala_function0 "copy_file_base" [absolute_path base_dir, Path.implode src, absolute_path target_dir]; (* tmp files *) fun create_tmp_path name ext = let val path = File.tmp_path (Path.basic (name ^ serial_string ()) |> Path.ext ext); val _ = File.exists path andalso raise Fail ("Temporary file already exists: " ^ Path.print path); in path end; fun with_tmp_file name ext f = let val path = create_tmp_path name ext in Exn.release (Exn.capture f path before ignore (try File.rm path)) end; (* tmp dirs *) fun rm_tree path = scala_function "rm_tree" [path]; fun with_tmp_dir name f = let val path = create_tmp_path name "" in Exn.release (Exn.capture f (make_directory path) before ignore (try rm_tree path)) end; (* download file *) fun download url file = ignore (Scala.function "download" (cat_strings0 [url, absolute_path file])); end;