Email Gateway (Mar 14 2021 at 21:19): Email Gateway (Mar 14 2021 at 21:19):From: Makarius <makarius@sketis.net>
* General *
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):
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Mar 14 2021 at 21:44):From: Makarius <makarius@sketis.net>
For completeness, this is the underlying HTTP module in Isabelle/Scala:
More than 10 years ago, I was promoting the use of perl as "universal system
glue". Now we can do it more concisely in Isabelle/Scala, without external
dependencies, and with fine points adjusted to Isabelle standards. The above
is < 10Kb for client and server, which is used for isabelle.preview in
Isabelle/jEdit.
It is still too early to ask the canonical question about "any remaining uses
of perl": there are still quite a lot in small scripts that are not
incorporated in Isabelle/Scala yet, e.g. "isabelle latex".
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Dec 21 2024 at 16:20 UTC