--- a/src/HOL/Tools/ATP/system_on_tptp.ML Sun Mar 14 18:27:55 2021 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.ML Sun Mar 14 18:32:11 2021 +0100
@@ -8,7 +8,7 @@
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
@@ -24,7 +24,9 @@
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>\<open>SystemOnTPTP.run_system\<close>
|> split_strings0 |> (fn [output, timing] =>
{output = output, timing = Time.fromMilliseconds (Value.parse_int timing)})
--- a/src/HOL/Tools/ATP/system_on_tptp.scala Sun Mar 14 18:27:55 2021 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala Sun Mar 14 18:32:11 2021 +0100
@@ -72,7 +72,8 @@
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"
--- a/src/Pure/System/isabelle_system.ML Sun Mar 14 18:27:55 2021 +0100
+++ b/src/Pure/System/isabelle_system.ML Sun Mar 14 18:32:11 2021 +0100
@@ -11,6 +11,7 @@
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