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:
And then rebuild the logic images.
An alternative is to modify Isabelle/Pure like this:
RCS file: Pure/General/secure.ML,v
retrieving revision 1.14
diff -r1.14 secure.ML
< 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and