Re: [isabelle] Isabelle 2007 destroys heaps



On Thu, 29 Nov 2007, Makarius wrote:

> On Thu, 29 Nov 2007, Daniel Wasserrab wrote:
> 
> > If I make the HOL heap read-only, it all works again. But if I create 
> > via "isabelle -q HOL Test" a new heap file, then this "Test" heap is 
> > again writeable and the same problem occurs. So manually adjusting these 
> > self-created heaps is necessary?
> 
> By adding option -w to the isabelle invokation the resulting heap will be 
> read-only; isatool usedir provides a slightly more high-level mechanism to 
> achive a similar effect.

Just in case you really mean to have writable persistent sessions: there 
is a general problem in restarting a session that has been committed from 
Isar or Proof General interaction mode (committing from ML is OK).  This 
is related to multithreading in Poly/ML 5.1 -- the commit happens in a 
critical section and the related mutex is written out in locked state. 
After reloading the session, this results in a deadlock!

You can workaround this by pretending that your Poly/ML is actually 5.0, 
e.g. like this in ~/isabelle/etc/settings:

  ML_SYSTEM=polyml-5.0

And then rebuild the logic images.


An alternative is to modify Isabelle/Pure like this:

Index: Pure/General/secure.ML
===================================================================
RCS file: Pure/General/secure.ML,v
retrieving revision 1.14
diff -r1.14 secure.ML
55c55
< fun commit () = CRITICAL (fn () => orig_use_text "" Output.ml_output false "commit();");
---
> fun commit () = orig_use_text "" Output.ml_output false "commit();";


You will also need to rebuild logics, but can continue to work with 
Poly/ML 5.1 and multicore support enabled (and proper timeout for 
auto_quickcheck).


	Makarius





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