[isabelle-dev] Isabelle2013-2 release
makarius at sketis.net
Mon Nov 25 12:15:19 CET 2013
On Mon, 25 Nov 2013, Gerwin Klein wrote:
> the main use case for WWW_Find is with images that are potentially too
> big to build yourself or that you don’t have on your machine for some
> other reason (e.g. too big for a laptop or small desktop).
> If the find_theorems panel could connect to a remote resource similar to
> sledgehammer's remote provers, we could remove WWW_Find.
The question here is what to make remotely available.
A crude solution is to offer prebuilt heap images for remove file-system
access or copying, although this is presumably a bit awkward.
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
This issue is not imminent, but might be revisited before the next release
More information about the isabelle-dev