[isabelle-dev] new isabelle interface
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/
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).
More information about the isabelle-dev