author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 73568 | bdba138d462d |
child 78592 | fdfe9b91d96e |
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.scala |
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 |
package isabelle.atp |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
8 |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
9 |
import isabelle._ |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
10 |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
11 |
import java.net.URL |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
12 |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
13 |
|
75393 | 14 |
object SystemOnTPTP { |
73420 | 15 |
/* requests */ |
16 |
||
73418
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
17 |
def get_url(options: Options): URL = Url(options.string("SystemOnTPTP")) |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
18 |
|
73422 | 19 |
def post_request( |
20 |
url: URL, |
|
21 |
parameters: List[(String, Any)], |
|
75393 | 22 |
timeout: Time = HTTP.Client.default_timeout |
23 |
): HTTP.Content = { |
|
73423 | 24 |
try { |
73441 | 25 |
HTTP.Client.post(url, |
26 |
("NoHTML" -> 1) :: parameters, |
|
27 |
timeout = timeout, |
|
28 |
user_agent = "Sledgehammer") |
|
73423 | 29 |
} |
30 |
catch { case ERROR(msg) => cat_error("Failed to access SystemOnTPTP server", msg) } |
|
73420 | 31 |
} |
32 |
||
33 |
||
34 |
/* list systems */ |
|
35 |
||
73430 | 36 |
def list_systems(url: URL): HTTP.Content = |
73441 | 37 |
post_request(url, |
38 |
List("SubmitButton" -> "ListSystems", |
|
39 |
"ListStatus" -> "READY", |
|
40 |
"QuietFlag" -> "-q0")) |
|
73418
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
41 |
|
75393 | 42 |
object List_Systems extends Scala.Fun_String("SystemOnTPTP.list_systems", thread = true) { |
73418
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
43 |
val here = Scala_Project.here |
73440 | 44 |
def apply(url: String): String = list_systems(Url(url)).text |
73418
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
45 |
} |
73431
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
46 |
|
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
47 |
|
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
48 |
/* run system */ |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
49 |
|
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
50 |
def run_system(url: URL, |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
51 |
system: String, |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
52 |
problem: String, |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
53 |
extra: String = "", |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
54 |
quiet: String = "01", |
75393 | 55 |
timeout: Time = Time.seconds(60) |
56 |
): HTTP.Content = { |
|
73431
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
57 |
val paramaters = |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
58 |
List( |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
59 |
"SubmitButton" -> "RunSelectedSystems", |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
60 |
"ProblemSource" -> "FORMULAE", |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
61 |
"FORMULAEProblem" -> problem, |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
62 |
"ForceSystem" -> "-force", |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
63 |
"System___" + system -> system, |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
64 |
"TimeLimit___" + system -> timeout.seconds.ceil.toLong, |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
65 |
"Command___" + system -> extra, |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
66 |
"QuietFlag" -> ("-q" + quiet)) |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
67 |
post_request(url, paramaters, timeout = timeout + Time.seconds(15)) |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
68 |
} |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
69 |
|
75393 | 70 |
object Run_System extends Scala.Fun_Strings("SystemOnTPTP.run_system", thread = true) { |
73431
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
71 |
val here = Scala_Project.here |
75393 | 72 |
def apply(args: List[String]): List[String] = { |
73568
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73565
diff
changeset
|
73 |
val List(url, system, problem_path, extra, Value.Int(timeout)) = args |
73434
00b77365552e
clarified signature: refer to file name instead of file content;
wenzelm
parents:
73431
diff
changeset
|
74 |
val problem = File.read(Path.explode(problem_path)) |
73441 | 75 |
|
73431
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
76 |
val res = run_system(Url(url), system, problem, extra = extra, timeout = Time.ms(timeout)) |
73440 | 77 |
val text = res.text |
78 |
val timing = res.elapsed_time.ms |
|
79 |
||
73431
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
80 |
val bad_prover = "WARNING: " + system + " does not exist" |
73440 | 81 |
if (split_lines(text).exists(_.startsWith(bad_prover))) { |
73431
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
82 |
error("The ATP " + quote(system) + " is not available at SystemOnTPTP") |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
83 |
} |
73568
bdba138d462d
clarified signature: more structured arguments, notably for remote provers;
wenzelm
parents:
73565
diff
changeset
|
84 |
else List(text, timing.toString) |
73431
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
85 |
} |
f27d7b12e8a4
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents:
73430
diff
changeset
|
86 |
} |
73418
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
87 |
} |