Re: [isabelle] Interfacing with Isabelle

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

It sounds like this repeated invocation would make you constantly lose the 
current proof state. Or can can this be avoided by dumping/re-loading the heap 
every time? At the very least it sounds as if it may have a high cost due to 
the repeated initializations of the system?

> 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

I've actually used Scala a little before (and use Haskell quite a bit, so am 
familiar with the functional style). I will give this a look.

> > 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 can't be more specific, because I really don't know :). I am still in the 
exploring stage right now, seeing what can be done and what the best way to do 
it is. I will likely do another round of research on general theorem prover 
interfaces and things like this if it proves needed (too busy right now).

> > 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
> (or later).

Ahhh, thanks for the tip! I now have a development version compiled (I 
think... untested)


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