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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
