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 
failed.


> 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 
now.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.