--- 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>
--- /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
--- /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)))
+ }
+}
--- 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)"
--- 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)
--- 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"))
--- 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