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