Re: [isabelle] Isabelle 2007 destroys heaps



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
  ML>

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?


	Makarius





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