[isabelle-dev] Isabelle2012 post-release mode

[Makarius]

On Tue, 29 May 2012, Lukas Bulwahn wrote:

>>>> With the mira testing, Isabelle-makeall on lxbroy10 seems to be not 
>>>> terminating after the release branch was merged back.
>>>> I killed the processes now throughout the days, but I cannot tell what 
>>>> the error is.
>>>> 
>>>> It seems as if the script "perl -w /lib/scripts/feeder.pl" is doing 
>>>> something wrong.
>>> 
>>> This is really odd.  From the description it can only be a consequence of 
>>> this change from the isabelle-release repository:
>>> 
>>> changeset:   47868:32c03d45fffe
>>> user:        wenzelm
>>> date:        Fri May 04 17:14:42 2012 +0200
>>> files:       lib/scripts/feeder.pl
>>> description:
>>> refrain from SIGHUP handling (cf. 5f629ee2502b), which does not work on 
>>> Cygwin and appears to be redundant anyway (no extra output produced within 
>>> pipe);


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.


> Your attempt, changeset 6de952f4069f, was successful. lxbroy10 now can 
> test all future changesets again.

For the record, it is the following trivial change:

diff -r c79adcae9869 -r 6de952f4069f lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Fri May 25 13:23:43 2012 +0200
+++ b/lib/scripts/run-polyml	Fri May 25 17:14:14 2012 +0200
@@ -76,3 +76,3 @@
  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-  { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+  { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
  RC="$?"

Since the feeder process no longer treats HUP specifically, any of the 
signals that normally terminate a process can be used.  (Oddly, setting 
the signal handler for HUP before had caused it to be ignored on Cygwin.)

The above kill -TERM can be taken as the standard workaround for the 
problem until we find out more about the situation.


> Unfortunately, once mira tests older changesets it hangs, so all 
> developers should please push to the testboard, tell me, and I will 
> restart the daemon.

This touches the general problem that Isabelle2012 now has erratic signal 
handling or not handling, specifically on Linux with recent perl and big 
sessions.

Published releases are immutable, and can only be superseded by other 
releases.  For the moment my tendency is to wait and see how relevant it 
is for most users.  We can certainly modify the 
/home/isabelle/Isabelle2012 installation to accomodate isatest/AFP.


 	Makarius