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

Thanks for the help

Makarius wrote:
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:

  $ isabelle
  > 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 MHonArc.