# 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 \Tools/ATP/system_on_tptp.ML\ ML_file \Tools/Sledgehammer/async_manager_legacy.ML\ ML_file \Tools/Sledgehammer/sledgehammer_util.ML\ ML_file \Tools/Sledgehammer/sledgehammer_fact.ML\ 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>\SystemOnTPTP\ + +fun list_systems () = get_url () |> \<^scala_thread>\SystemOnTPTP.list_systems\ |> 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