| author | haftmann |
| Fri, 27 Jun 2025 08:09:26 +0200 | |
| changeset 82775 | 61c39a9e5415 |
| parent 73568 | bdba138d462d |
| permissions | -rw-r--r-- |
|
73418
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/ATP/system_on_tptp.ML |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
3 |
|
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
4 |
Support for remote ATPs via SystemOnTPTP. |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
5 |
*) |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
6 |
|
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
7 |
signature SYSTEM_ON_TPTP = |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
8 |
sig |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
9 |
val get_url: unit -> string |
|
73424
2b657a70116c
clarified signature: url may change dynamically and is part of result;
wenzelm
parents:
73419
diff
changeset
|
10 |
val list_systems: unit -> {url: string, systems: string list}
|
|
73568
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73435
diff
changeset
|
11 |
val run_system_encoded: string list -> {output: string, timing: Time.time}
|
|
73434
00b77365552e
clarified signature: refer to file name instead of file content;
wenzelm
parents:
73431
diff
changeset
|
12 |
val run_system: {system: string, problem: Path.T, extra: string, timeout: Time.time} ->
|
|
73431
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
13 |
{output: string, timing: Time.time}
|
|
73418
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
14 |
end |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
15 |
|
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
16 |
structure SystemOnTPTP: SYSTEM_ON_TPTP = |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
17 |
struct |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
18 |
|
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
19 |
fun get_url () = Options.default_string \<^system_option>\<open>SystemOnTPTP\<close> |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
20 |
|
|
73424
2b657a70116c
clarified signature: url may change dynamically and is part of result;
wenzelm
parents:
73419
diff
changeset
|
21 |
fun list_systems () = |
|
2b657a70116c
clarified signature: url may change dynamically and is part of result;
wenzelm
parents:
73419
diff
changeset
|
22 |
let |
|
2b657a70116c
clarified signature: url may change dynamically and is part of result;
wenzelm
parents:
73419
diff
changeset
|
23 |
val url = get_url () |
| 73430 | 24 |
val systems = trim_split_lines (\<^scala>\<open>SystemOnTPTP.list_systems\<close> url) |
|
73424
2b657a70116c
clarified signature: url may change dynamically and is part of result;
wenzelm
parents:
73419
diff
changeset
|
25 |
in {url = url, systems = systems} end
|
|
73418
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
26 |
|
|
73435
1cc848548f21
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
wenzelm
parents:
73434
diff
changeset
|
27 |
fun run_system_encoded args = |
|
73568
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73435
diff
changeset
|
28 |
(get_url () :: args) |
|
73431
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
29 |
|> \<^scala>\<open>SystemOnTPTP.run_system\<close> |
|
73568
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73435
diff
changeset
|
30 |
|> (fn [a, b] => {output = a, timing = Time.fromMilliseconds (Value.parse_int b)})
|
|
73431
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
31 |
|
|
73435
1cc848548f21
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
wenzelm
parents:
73434
diff
changeset
|
32 |
fun run_system {system, problem, extra, timeout} =
|
|
73568
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73435
diff
changeset
|
33 |
[system, Isabelle_System.absolute_path problem, extra, string_of_int (Time.toMilliseconds timeout)] |
|
73435
1cc848548f21
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
wenzelm
parents:
73434
diff
changeset
|
34 |
|> run_system_encoded |
|
1cc848548f21
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
wenzelm
parents:
73434
diff
changeset
|
35 |
|
|
73418
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
36 |
end |