[isabelle-dev] Isabelle2013-2 release

[Makarius]

On Mon, 25 Nov 2013, Lars Hupel wrote:

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

I did not understand the last part about network and protocols, but I did 
not look at Akka either.  Martin Ring from Bremen has told me that he is 
using remote Akka with Isabelle/Scala quite sucessfully already.

To get a remote prover process, the most obvious idea is to make the 
Isabelle_Process a remote actor, with the existing Isabelle_Process.Input 
and Isabelle_Process.Output messages as Scala values.

This would of course require to revisit questions about performance of 
actor channels: the existing approach in Isabelle/Scala only started 
working properly, after I made some re-adjustments of the internal 
communication network in autumn 2011 (just before Isabelle2011-1, which 
then became the first usable Isabelle/jEdit implementation).


 	Makarius