[isabelle-dev] new isabelle interface

[Cameron Freer]

On Mon, 25 Aug 2008, Makarius wrote:

> On Sun, 24 Aug 2008, Chris Capel wrote:
>
>> I'm thinking about making a new interface to Isabelle, along the lines
>> of Proof General, but not requiring Emacs (ugh). It would be done in C#
>> and be for Windows initially, though depending on how I do it it could
>> probably be made to work in Linux and other Unixen as well.
>>
>> First of all, is there anything done already along these lines?
>
> About two years ago I realized that it is high time to look again into the
> important issue of Isabelle UI, after about 10 years of Proof General /
> Emacs as de-facto standard.
...
>    These prefabricated JVM/Scala support modules shipped with Isabelle
>    definitely have a certain platform bias.  Other UI projects are free
>    to ignore this and build their own stuff, potentially going down to
>    the underlying protocols instead of using the APIs.


At the Isabelle user meeting after TPHOLs last week, I mentioned
SAGE's web notebook as a interesting approach:
live version: http://www.sagenb.org/
documentation: http://www.sagemath.org/doc/tut/node45.html
http://www.sagemath.org/doc/ref/node8.html
http://sage.math.washington.edu/home/tkosan/newbies_book/short_version/getting_started_with_sage_v1.1.pdf

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

If such an interface were trivial to invoke from a local Isabelle
installation, it could also serve as another UI option (or the only
one on platforms otherwise not supported).

  - Cameron