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 
> system?

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 
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
which is the proper place to discuss things that are not in the official 
release yet.

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


	Makarius





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