# HG changeset patch
# User wenzelm
# Date 1615732124 -3600
# Node ID f27d7b12e8a470692a152bc9e5b72b59bd2598e8
# Parent  c7f14309e291e0bb08b0a8f125dd709e17d0c926
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;

diff -r c7f14309e291 -r f27d7b12e8a4 src/HOL/Tools/ATP/system_on_tptp.ML
--- a/src/HOL/Tools/ATP/system_on_tptp.ML	Sun Mar 14 13:21:59 2021 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.ML	Sun Mar 14 15:28:44 2021 +0100
@@ -8,6 +8,8 @@
 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} ->
+    {output: string, timing: Time.time}
 end
 
 structure SystemOnTPTP: SYSTEM_ON_TPTP =
@@ -21,4 +23,10 @@
     val systems = trim_split_lines (\<^scala>\<open>SystemOnTPTP.list_systems\<close> 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)]
+  |> \<^scala>\<open>SystemOnTPTP.run_system\<close>
+  |> split_strings0 |> (fn [output, timing] =>
+    {output = output, timing = Time.fromMilliseconds (Value.parse_int timing)})
+
 end
diff -r c7f14309e291 -r f27d7b12e8a4 src/HOL/Tools/ATP/system_on_tptp.scala
--- a/src/HOL/Tools/ATP/system_on_tptp.scala	Sun Mar 14 13:21:59 2021 +0100
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala	Sun Mar 14 15:28:44 2021 +0100
@@ -23,7 +23,7 @@
     timeout: Time = HTTP.Client.default_timeout): HTTP.Content =
   {
     val parameters0 =
-      List("NoHTML" -> 1, "QuietFlag" -> "-q01")
+      List("NoHTML" -> 1, "QuietFlag" -> "-q0")
         .filterNot(p0 => parameters.exists(p => p0._1 == p._1))
     try {
       HTTP.Client.post(url, parameters0 ::: parameters,
@@ -43,4 +43,43 @@
     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 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 -r c7f14309e291 -r f27d7b12e8a4 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Sun Mar 14 13:21:59 2021 +0100
+++ b/src/Pure/System/scala.scala	Sun Mar 14 15:28:44 2021 +0100
@@ -260,4 +260,5 @@
   Isabelle_System.Rm_Tree,
   Isabelle_System.Download,
   Isabelle_Tool.Isabelle_Tools,
-  isabelle.atp.SystemOnTPTP.List_Systems)
+  isabelle.atp.SystemOnTPTP.List_Systems,
+  isabelle.atp.SystemOnTPTP.Run_System)