[isabelle-dev] NEWS: Remote provers from SystemOnTPTP via Isabelle/Scala

[Makarius]

*** General ***

* Remote provers from SystemOnTPTP (notably for Sledgehammer) are now
managed via Isabelle/Scala instead of perl; the dependency on
libwww-perl has been eliminated (notably on Linux). Rare
INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties
https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/doc-files/net-properties.html


This refers to Isabelle/e92f2e44e4d8.


Example invocation with remote provers:

sledgehammer [provers = remote_e remote_alt_ergo remote_zipperposition
remote_vampire]


Note: remote_vampire is actually broken right now, because SystemOnTPTP has
changed its repertoire of Vampire versions. (Remote services are sometimes
convenient for experimentation, but a properly integrated local installation
is more reliable.)


This is how to print the list of systems in Isabelle/ML:

ML_command ‹SystemOnTPTP.list_systems () |> #systems |> cat_lines |> writeln›


And here is the actual implementation in Isabelle/Scala (using HTTP POST
requests):

https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/HOL/Tools/ATP/system_on_tptp.scala;e92f2e44e4d8


	Makarius