[isabelle-dev] Isabelle2013-2 release

[Lars Hupel]

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