Email Gateway (Aug 18 2022 at 11:04): Email Gateway (Aug 18 2022 at 11:04):From: Daniel Wasserrab <wasserra@infosun.fim.uni-passau.de>
Hello everyone,
the new Isabelle 2007 seems to destroy heaps. When I open an Isabelle
process, terminate it and try to start a new one, Isabelle hangs up and
doesn't respond any more. I get the same behaviour if one process is
running and I try to run isatool, the isatool process also hangs up. You
have to rebuild the heap (or have a "untouched" save copy) if you want
Isabelle to work properly again.
I'm not the only one with this behaviour, my colleague has exactly the
same problem. Does anyone know why this happens and how to fix it?
Regards
Daniel
Email Gateway (Aug 18 2022 at 11:05):From: Makarius <makarius@sketis.net>
On Wed, 28 Nov 2007, Daniel Wasserrab wrote:
When I open an Isabelle process, terminate it and try to start a new
one, Isabelle hangs up and doesn't respond any more.
What exactly do you mean by "terminate"? Is this just an interrupt
signal, or the stop button in Proof General?
I'm not the only one with this behaviour, my colleague has exactly the
same problem. Does anyone know why this happens and how to fix it?
All this sounds very odd. What is your platform (operating system,
Poly/ML version, Emacs version)?
Makarius
Email Gateway (Aug 18 2022 at 11:05):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 11:06):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 18 2022 at 11:06):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 11:06):From: Daniel Wasserrab <wasserra@infosun.fim.uni-passau.de>
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.
We are running on Fedora 4, linux kernel 2.6.17-1.2142_FC4smp, poly-ml
5.1, ProofGeneral-3.7pre071112 (the versions to download for the new
Isabelle2007), XEmacs 21.4 (patch 19)
Makarius wrote:
Email Gateway (Aug 18 2022 at 11:06):From: Daniel Wasserrab <wasserra@infosun.fim.uni-passau.de>
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
Daniel
Makarius wrote:
Last updated: May 03 2024 at 04:19 UTC