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 http://www.scala-lang.org/).
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
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
> http://isabelle.in.tum.de/repos/isabelle/rev/351fc2f8493d (or later).
Ahhh, thanks for the tip! I now have a development version compiled (I
This archive was generated by a fusion of
Pipermail (Mailman edition) and