Re: [isabelle] Isabelle 2007 destroys heaps
Ok. it seems you have pinned the problem. 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
Thanks for the help
On Thu, 29 Nov 2007, Daniel Wasserrab wrote:
By terminate I mean exiting the ProofGeneral via "Exit Isabelle" (or
Ctrl-c Ctrl-x). Then starting a new Isabelle process in ProofGeneral
just states "Starting process: bla/bin/isabelle-process -PI -m PGASCII
HOL" and then hangs up.
OK, so lets try this without ProofGeneral:
> val it = () : unit
val commit = fn : unit -> bool
Now CTRL-D will terminate the process. Does this work as expected?
There might be also a problem with the permissions of
Isabelle/heaps/polyml-5.1_x86-linux/HOL (should be read-only). Which file
system type is used for Isabelle/heaps?
This archive was generated by a fusion of
Pipermail (Mailman edition) and