On Mon, 25 Aug 2008, Cameron Freer wrote:
> One can type a single command from the SAGE commandline to spawn a local
> webserver running the notebook interface. I've found the AJAX interface
> to be surprisingly clean, responsive, and pleasant, even for those used
> to the commandline. Such a web interface for Isabelle would probably be
> more complicated, but it does offer similar advantages -- not just the
> ability to separate the kernel from the UI, but also portability (for
> users running it locally).
>
> Kaliszyk proposed something similar for Coq a couple years ago:
> http://www.easychair.org/FLoC-06/UITP-preproceedings.pdf#page=57
Very good. Cezary Kaliszyk is actually one of the prover UI people who
greatly influenced the upcoming Isabelle architecture. Cezary has quite
responsive AJAX / JavaScript on the client side, but on the server his own
OCaml wrapper around the prover, which exposes a couple of problems. The
latter can be easily replaced by a more robust version using the new Scala
classes of Isabelle, using existing server tools available for the JVM.
If there are any AJAX experts out there who would like to produce an
interface to our (slowly emerging) server infrastructure, I would be happy
to assist them.
Makarius
