Re: [isabelle] Interfacing with Isabelle
On Wed, 25 Feb 2009, Scott West wrote:
> Is there a standard, accepted, advised, or otherwise endorsed method of
> interfacing with the Isabelle system? Currently I have a small program
> which spawns a Isabelle TTY through the isatool, and communicates
> through the standard handles.
Traditionally, the "standard" way to work with Isabelle under external
program control is rather primitive, see the "isabelle-process" command in
the system manual. Here you get access to the raw ML toplevel, and you
can pass ML expressions via the -e option. In principle this allows you
to do whatever you want, by invoking suitable ML things of your own
making. (Which is quite admittedly quite hard.)
A few such interaction wrappers have emerged in the past (notably for
Proof General), and made it into the official distribution, adding funny
options like -P -I -X to isabelle-process.
Starting with Isabelle2008 we have introduced one final wrapper
(isabelle-process option -W), which is meant to interface to a proper API
that lives in the JVM world. That JVM library is part of the official
Isabelle distribution, so user code does not need to fiddle with low-level
interaction protocols anymore (that is the basic plan).
In Isabelle2008 this extra layer is still Java/JVM, but we have already
left behind Java altogether in favour of Scala/JVM (which is the Next Big
Thing in programming language design, see http://www.scala-lang.org/).
There are still many things missing here; we have only started to make
actual use of Isabelle within the Scala/JVM world, using jEdit as editor
framework. Others have tried Netbeans with some success.
> I feel this may not be the best way for automated-interaction (I'm
> trying to see if I can make a new interface).
Can you be more specific what you are working on? Interacting with
interactive provers under program control is very hard to get right. I
have been involved in a couple of attempts so far, some succesful, many
> I became stymied by the documentation of the underlying ML (is there
> some disjointedness between the documentation and the current release?).
The manuals usually lag behind the real system a couple of years. The
newer manuals are at least formally checked against the system, meaning
that any references to ML entities, Isar commands, methods etc. correct.
For the forthcoming release the main reference manuals (isar-ref,
implementation, system) come in significantly updated and extended
versions. If your are interested, you may already peek at this version
via the repository
http://isabelle.in.tum.de/repos/isabelle/rev/351fc2f8493d (or later).
It is usually easier to peek at (fully tested) snapshots via
http://isabelle.in.tum.de/devel/ but that appears to be unmaintained right
This archive was generated by a fusion of
Pipermail (Mailman edition) and