[isabelle-dev] Isabelle2013-2 release

[Makarius]

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

This issue is not imminent, but might be revisited before the next release 
in 2014.


 	Makarius