[isabelle-dev] new isabelle interface
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