[isabelle-dev] Isabelle2012 post-release mode
makarius at sketis.net
Thu May 31 13:26:28 CEST 2012
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
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.
More information about the isabelle-dev