[isabelle-dev] new isabelle interface

Cameron Freer freer at math.mit.edu
Mon Aug 25 15:32:42 CEST 2008

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

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:

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

More information about the isabelle-dev mailing list