[isabelle-dev] new isabelle interface

Makarius makarius at sketis.net
Mon Aug 25 11:58:57 CEST 2008

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.

Spending quite some time in investigating the general situation, and 
discussing with a number of people who have been involved in prover UI 
implementation, this is my general strategy as far as the official 
Isabelle distribution is concerned:

  * The Isabelle system itself is changed to make it easier to interface 
    to existing editor frameworks, IDEs etc.  The ancient tty model of 
    issuing individual commands one by one and getting messages back 
    promptly is replaced by some kind of ``editor buffer model''.  (The 
    old tty interaction remains available as an emulation on top of that.)

    Moreover all prover output is decorated with precise source 
    information, to allow the UI to attach feedback messages to the source 
    text (using tooltips, twiggles etc.)  There are also new "status" 
    messages that provide detailed information about the state of 
    processing sources by the prover, e.g. indicating references to formal 
    entities (terms and theorems) in the text.

  * The Isabelle distribution also provides some tightly fit layer to 
    integrate the prover process into the JVM platform, targeting mostly 
    Scala as source language.  See also http://www.scala-lang.org/ about 
    the latest innovations in the JVM world.

    This basic interface layer will make it quite easy to build an actual 
    UI on top.  At the moment we have some local student project going to 
    explore this for jEdit (http://www.jedit.org).  One could also think 
    of Netbeans at some point, if one has real resources to spend.  (I 
    will not get involved in anything using Eclipse.)

    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.

In the past view months/weeks I've made substantial progress in the above 
respects.  See recent development snapshots of Isabelle, and don't bother 
to ask me about further details.

> I plan to use SML.NET to compile Isabelle. Does anyone forsee any 
> problems with this? Is Isabelle's code fairly portable across Standard 
> ML compilers?

I would be surprised if it will work as expected.  For Isabelle you need 
the old-fashioned dynamic-compilation mode that allows to invoke the 
compiler at any point at run time.  Can SML.NET do that?

Moreover, our Poly/ML platform has quite good performance, including 
proper parallel execution on multiple cores.  (We will use more of that 
soon.)  I don't think you will get to the same level of Poly/ML 
performance on .NET without some fundamental rearrangements.

> Besides what's in the source distribution, is there any internals
> documentation I should know about?

Did you see the "Isabelle/Isar implementation manual" (which is only 20% 
finished and parts of it already outdated).

Concerning the general prover interaction model, there are a couple of 
papers on PGIP by David Aspinall and others.  More recent considerations 
are in the UITP 2008 paper by Holger Gast.  Anything beyond that is 
subject to ongoing research (and development).

The latest sources are always available via 
http://isabelle.in.tum.de/repos/isabelle/ which even allows you to 
subscribe to the changelog via RSS/Atom, so you can immerse yourself in 
tons of fine-grained change messages :-)

> Is there much in Isabelle that's Unix-specific that I'd need to port? If 
> so, it would be nice to have a clean way to do that.

We assume standard Posix behaviour everywhere.  Thanks to Cygwin even the 
Windows platform is able to participate here.  E.g. it is already possible 
to have several Posix threads running within Isabelle, some of them 
controlling external Posix processes and still get Posix signals between 
threads and processes through in the expected manner.  (This even works if 
native windows stuff is run via Cygwin.)

Our JVM/Scala layer will also hold up this Posix-ish view, e.g. Isabelle 
file names like "~/tmp/A.thy" or "$ISABELLE_HOME/src/HOL/List.thy" will be 
handled as expected.


More information about the isabelle-dev mailing list