# HG changeset patch
# User wenzelm
# Date 1615588235 -3600
# Node ID 7d7d959547a16f8fe3a9a73995388c490f0297da
# Parent  1dcc2b228b8b45c135d82243af81234c665ee097
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);

diff -r 1dcc2b228b8b -r 7d7d959547a1 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Fri Mar 12 23:00:01 2021 +0100
+++ b/src/HOL/Sledgehammer.thy	Fri Mar 12 23:30:35 2021 +0100
@@ -13,6 +13,7 @@
   "sledgehammer_params" :: thy_decl
 begin
 
+ML_file \<open>Tools/ATP/system_on_tptp.ML\<close>
 ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>
diff -r 1dcc2b228b8b -r 7d7d959547a1 src/HOL/Tools/ATP/system_on_tptp.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/system_on_tptp.ML	Fri Mar 12 23:30:35 2021 +0100
@@ -0,0 +1,20 @@
+(*  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 -> string list
+end
+
+structure SystemOnTPTP: SYSTEM_ON_TPTP =
+struct
+
+fun get_url () = Options.default_string \<^system_option>\<open>SystemOnTPTP\<close>
+
+fun list_systems () = get_url () |> \<^scala_thread>\<open>SystemOnTPTP.list_systems\<close> |> split_lines
+
+end
diff -r 1dcc2b228b8b -r 7d7d959547a1 src/HOL/Tools/ATP/system_on_tptp.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala	Fri Mar 12 23:30:35 2021 +0100
@@ -0,0 +1,37 @@
+/*  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
+{
+  def get_url(options: Options): URL = Url(options.string("SystemOnTPTP"))
+
+  def proper_lines(text: String): List[String] =
+    Library.trim_split_lines(text).filterNot(_.startsWith("%"))
+
+  def list_systems(url: URL): List[String] =
+  {
+    val result =
+      HTTP.Client.post(url, user_agent = "Sledgehammer", parameters =
+        List("NoHTML" -> 1,
+          "QuietFlag" -> "-q0",
+          "SubmitButton" -> "ListSystems",
+          "ListStatus" -> "READY"))
+    proper_lines(result.text)
+  }
+
+  object List_Systems extends Scala.Fun("SystemOnTPTP.list_systems")
+  {
+    val here = Scala_Project.here
+    def apply(url: String): String = cat_lines(list_systems(Url(url)))
+  }
+}
diff -r 1dcc2b228b8b -r 7d7d959547a1 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Fri Mar 12 23:00:01 2021 +0100
+++ b/src/HOL/Tools/etc/options	Fri Mar 12 23:30:35 2021 +0100
@@ -35,6 +35,9 @@
 public option vampire_noncommercial : string = "unknown"
   -- "status of Vampire activation for noncommercial use (yes, no, unknown)"
 
+public option SystemOnTPTP : string = "http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply"
+  -- "URL for SystemOnTPTP service"
+
 public option MaSh : string = "sml"
   -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"
 
diff -r 1dcc2b228b8b -r 7d7d959547a1 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Fri Mar 12 23:00:01 2021 +0100
+++ b/src/Pure/System/scala.scala	Fri Mar 12 23:30:35 2021 +0100
@@ -252,4 +252,5 @@
   Isabelle_System.Copy_File_Base,
   Isabelle_System.Rm_Tree,
   Isabelle_System.Download,
-  Isabelle_Tool.Isabelle_Tools)
+  Isabelle_Tool.Isabelle_Tools,
+  isabelle.atp.SystemOnTPTP.List_Systems)
diff -r 1dcc2b228b8b -r 7d7d959547a1 src/Pure/Tools/scala_project.scala
--- a/src/Pure/Tools/scala_project.scala	Fri Mar 12 23:00:01 2021 +0100
+++ b/src/Pure/Tools/scala_project.scala	Fri Mar 12 23:30:35 2021 +0100
@@ -74,6 +74,7 @@
       "src/Tools/jEdit/src-base/" -> Path.explode("isabelle.jedit_base"),
       "src/Tools/jEdit/src/" -> Path.explode("isabelle.jedit"),
       "src/HOL/SPARK/Tools" -> Path.explode("isabelle.spark"),
+      "src/HOL/Tools/ATP" -> Path.explode("isabelle.atp"),
       "src/HOL/Tools/Nitpick" -> Path.explode("isabelle.nitpick"))
 
 
diff -r 1dcc2b228b8b -r 7d7d959547a1 src/Pure/build-jars
--- a/src/Pure/build-jars	Fri Mar 12 23:00:01 2021 +0100
+++ b/src/Pure/build-jars	Fri Mar 12 23:30:35 2021 +0100
@@ -10,6 +10,7 @@
 
 declare -a SOURCES=(
   src/HOL/SPARK/Tools/spark.scala
+  src/HOL/Tools/ATP/system_on_tptp.scala
   src/HOL/Tools/Nitpick/kodkod.scala
   src/Pure/Admin/afp.scala
   src/Pure/Admin/build_csdp.scala