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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
