*** 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
