[isabelle-dev] Isabelle2013-2 release
hupel at in.tum.de
Mon Nov 25 14:32:34 CET 2013
> Another approach is to have the whole prover process running
> remotely, similar to the ancient rsh mode of Proof General 2.x that
> forgotten now. Isabelle/Scala uses actors for internal
> 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
More information about the isabelle-dev