Another approach is to have the whole prover process running
remotely, similar to the ancient rsh mode of Proof General 2.x that
is
forgotten now. Isabelle/Scala uses actors for internal
communication,
and this needs to be upgraded soon to one of the newer actor
frameworks, such as Akka -- the Scala guys continuously provide many
new things and dismantle old things eventually. I've heard that Akka
supports remote actors routinely.
Akka does in fact support remote actors, but that doesn't free us from
having to think about network and protocol issues.
A possible approach could be to provide another PIDE-based application
besides Isabelle/jEdit, /Eclipse and similar, which merely provides
low-level access via network, and on the other side, equip
Isabelle/Scala with the ability to communicate with a network backend.
One could imagine a menu option in Isabelle/jEdit for choosing between a
local and a remote instance of the prover.
While this approach is quite general and obliterates the need for some
other tools, its implementation would require significant work, even
when using the remote actor facilities of Akka. It is in the realm of
possibility, though.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
