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

Makarius makarius at sketis.net
Sun Mar 14 22:19:39 CET 2021

*** 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

This refers to Isabelle/e92f2e44e4d8.

Example invocation with remote provers:

sledgehammer [provers = remote_e remote_alt_ergo remote_zipperposition

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



More information about the isabelle-dev mailing list