Re: [isabelle] Interfacing with Isabelle
On Thu, 26 Feb 2009, Scott West wrote:
> > 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
Well, your ML function does not have to terminate immediately. The setup
for Proof General for example takes over the tty and then reacts to
further input. All of this is very delicate to get right, though.
Better try something based on the new process wrapper.
> > 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).
> I now have a development version compiled (I think... untested)
OK, maybe you want to subscribe to
which is the proper place to discuss things that are not in the official
Also make sure to use polyml-5.2.1, say from
http://isabelle.in.tum.de/polyml-5.2.1/ -- otherwise threads will not
work, and these are required for any of the newer interaction models.
(Threads will also give you better multicore performance.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and