[isabelle-dev] Isabelle2012 post-release mode

[Makarius]

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