[isabelle-dev] Isabelle2013-2 release
makarius at sketis.net
Mon Nov 25 15:35:11 CET 2013
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).
More information about the isabelle-dev