On Tue, 29 May 2012, Makarius wrote:
On Sat, 26 May 2012, Gerwin Klein wrote:
I think I have a similar problem getting the last two big AFP entries
online (Flyspeck and JinjaThreads).
When I use "nohup isabelle make" or anything that calls isabelle make,
the session builds fine, runs to the end of document preparation, but
then hangs inside perl doing nothing. For example:
Stops here without returning, and ps shows me that perl is still running
for this session.
This is on 64bit Linux (debian) and perl v5.14.2.
Without nohup things are fine.
The correlation with nohup is probably relevant, since it is supposed to
change the SIGHUP behaviour of the processes being run under its control.
Oddly, I still cannot reproduce the problem reliably, say on macbroy2 (Snow
Leopard) or my Ubuntu 10.04 LTS. I did manage to get a sporadic "hang" on
lxbroy10, but only in very rare situations.
My impression is that a relatively new perl version is required to run into
the trap, say 5.12 .. 5.14.
I've made some more experiments. With nohup on Linux the SIGHUP sent to
the feeder.pl script seems to be always absorbed, independently of the
perl version. On Mac OS, SIGHUP works either with or without nohup, which
is the accidental reason why I did not notice it in the final release
stage.
Reading the various man pages and specifications of nohup on the Web, it
seems that its exact signal masking behaviour is not precisely defined,
but SIGTERM will de-facto work most of the time. Thus the change
6de952f4069f after Isabelle2012 should be sufficient, but the official
release is now back in a state of the late 1990-ies, where one could not
use nohup reliably (also not CTRL-Z).
Back then the canonical solution was GNU "screen", which works without
affecting signal masks. So this is the current workaround again.
If more than one user stumbles over the issue, I consider putting some
note somewhere on the website, say as "Errata", but such things are
ignored by default anyway. So lets wait an see.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
