Re: [isabelle-dev] Isabelle2012 post-release mode
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
Re: [isabelle-dev] Isabelle2012 post-release mode
On 29/05/2012, at 9:31 PM, Makarius wrote: > 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. Normal AFP/isatest operation shouldn't be affected any more, so I don't think we need to do anything there. The AFP problem was just me trying to run existing big sessions over night. Usually, new entries don't need that. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2012 post-release mode
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-polymlFri May 25 13:23:43 2012 +0200
+++ b/lib/scripts/run-polymlFri 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
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2012 post-release mode
On 05/25/2012 03:31 PM, Lukas Bulwahn wrote: On 05/25/2012 02:17 PM, Makarius wrote: On Fri, 25 May 2012, Lukas Bulwahn wrote: On 05/23/2012 01:28 PM, Makarius wrote: Dear All, the current situation is as follows: * As of Isabelle/c5f7be4a1734 the http://isabelle.in.tum.de/repos/isabelle-release branch is merged again with the main line. * isatest is back testing http://isabelle.in.tum.de/repos/isabelle 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); It is a bit disturbing that the grand-unified Larry Wall operating system no longer works reliably. I am able to see isatest/mira processes on lxbroy10 where certain perl processes "hang", i.e. cannot be killed via SIGHUP as expected (but SIGTERM works). So far I have been unable to reproduce the behaviour in isolation. It might somehow depend on the precise options of mira. I've tried to get them from Admin/mira.py without success. What are the precises ML_OPTIONS and ISABELLE_USEDIR_OPTIONS here? They are the "default" options, but I do not know how they are detected (your bash scripts?) and how to get this information. Lukas Your attempt, changeset 6de952f4069f, was successful. lxbroy10 now can test all future changesets again. 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. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2012 post-release mode
On 23/05/2012, at 10:17 PM, Gerwin Klein wrote: > The AFP is now on freeze until the update to 2012 is out. AFP 2012 is out now and about to be announced. The repository is back to normal and open for normal commit traffic again. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2012 post-release mode
Btw: manually killing perl (just 'kill') seems to work and let the rest of the scripts continue. Gerwin On 26/05/2012, at 9:28 AM, 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: > > ~/afp/release/thys/Example-Submission$ nohup ~/tmp/Isabelle2012/bin/isabelle > make & > [...] > $ less nohup.out > > cd ..; ulimit -t 3600; /home/kleing/tmp/Isabelle2012/bin/isabelle usedir -v > true -i true -V outline=/proof,/ML -d pdf -P > "http://isabelle.in.tum.de/library/"; > /home/kleing/.isabelle/Isabelle2012/heaps/polyml-5.4.1_x86_64-linux/HOL > Example-Submission > Running HOL-Example-Submission ... > Browser info at > /home/kleing/.isabelle/Isabelle2012/browser_info/HOL/Example-Submission > Document at > /home/kleing/.isabelle/Isabelle2012/browser_info/HOL/Example-Submission/document.pdf > Document at > /home/kleing/.isabelle/Isabelle2012/browser_info/HOL/Example-Submission/outline.pdf > > 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. > > Cheers, > Gerwin > > > On 25/05/2012, at 10:17 PM, Makarius wrote: > >> On Fri, 25 May 2012, Lukas Bulwahn wrote: >> >>> On 05/23/2012 01:28 PM, Makarius wrote: Dear All, the current situation is as follows: * As of Isabelle/c5f7be4a1734 the http://isabelle.in.tum.de/repos/isabelle-release branch is merged again with the main line. * isatest is back testing http://isabelle.in.tum.de/repos/isabelle >>> >>> 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); >> >> It is a bit disturbing that the grand-unified Larry Wall operating system no >> longer works reliably. >> >> >> I am able to see isatest/mira processes on lxbroy10 where certain perl >> processes "hang", i.e. cannot be killed via SIGHUP as expected (but SIGTERM >> works). >> >> So far I have been unable to reproduce the behaviour in isolation. It might >> somehow depend on the precise options of mira. I've tried to get them from >> Admin/mira.py without success. What are the precises ML_OPTIONS and >> ISABELLE_USEDIR_OPTIONS here? >> >> >> Makarius >> >> ___ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2012 post-release mode
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: ~/afp/release/thys/Example-Submission$ nohup ~/tmp/Isabelle2012/bin/isabelle make & [...] $ less nohup.out cd ..; ulimit -t 3600; /home/kleing/tmp/Isabelle2012/bin/isabelle usedir -v true -i true -V outline=/proof,/ML -d pdf -P "http://isabelle.in.tum.de/library/"; /home/kleing/.isabelle/Isabelle2012/heaps/polyml-5.4.1_x86_64-linux/HOL Example-Submission Running HOL-Example-Submission ... Browser info at /home/kleing/.isabelle/Isabelle2012/browser_info/HOL/Example-Submission Document at /home/kleing/.isabelle/Isabelle2012/browser_info/HOL/Example-Submission/document.pdf Document at /home/kleing/.isabelle/Isabelle2012/browser_info/HOL/Example-Submission/outline.pdf 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. Cheers, Gerwin On 25/05/2012, at 10:17 PM, Makarius wrote: > On Fri, 25 May 2012, Lukas Bulwahn wrote: > >> On 05/23/2012 01:28 PM, Makarius wrote: >>> Dear All, >>> the current situation is as follows: >>> >>> * As of Isabelle/c5f7be4a1734 the >>>http://isabelle.in.tum.de/repos/isabelle-release branch is merged >>>again with the main line. >>> >>> * isatest is back testing http://isabelle.in.tum.de/repos/isabelle >> >> 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); > > It is a bit disturbing that the grand-unified Larry Wall operating system no > longer works reliably. > > > I am able to see isatest/mira processes on lxbroy10 where certain perl > processes "hang", i.e. cannot be killed via SIGHUP as expected (but SIGTERM > works). > > So far I have been unable to reproduce the behaviour in isolation. It might > somehow depend on the precise options of mira. I've tried to get them from > Admin/mira.py without success. What are the precises ML_OPTIONS and > ISABELLE_USEDIR_OPTIONS here? > > > Makarius > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2012 post-release mode
On 25.05.2012 15:23, Makarius wrote: On Fri, 25 May 2012, Makarius wrote: I am able to see isatest/mira processes on lxbroy10 where certain perl processes "hang", i.e. cannot be killed via SIGHUP as expected (but SIGTERM works). I think I've done too much killall here, so mira appears to be dead. What needs to be done to restart it? Where is this controlled anyway? Mira processes are started by hand at the moment (I still need to fix this); there should be a file mira_administration.txt somewhere in the mira directory which explains how to do this for the different machines. I'm currently on the road, so I have no usable SSH, but I can try to restart it this evening. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2012 post-release mode
On Fri, 25 May 2012, Makarius wrote: I am able to see isatest/mira processes on lxbroy10 where certain perl processes "hang", i.e. cannot be killed via SIGHUP as expected (but SIGTERM works). I think I've done too much killall here, so mira appears to be dead. What needs to be done to restart it? Where is this controlled anyway? Right now we also have problems with the isatest cron jobs (macbroy28), which work when started manually, but don't come up automatically as expected. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2012 post-release mode
On Fri, 25 May 2012, Lukas Bulwahn wrote: On 05/23/2012 01:28 PM, Makarius wrote: Dear All, the current situation is as follows: * As of Isabelle/c5f7be4a1734 the http://isabelle.in.tum.de/repos/isabelle-release branch is merged again with the main line. * isatest is back testing http://isabelle.in.tum.de/repos/isabelle 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); It is a bit disturbing that the grand-unified Larry Wall operating system no longer works reliably. I am able to see isatest/mira processes on lxbroy10 where certain perl processes "hang", i.e. cannot be killed via SIGHUP as expected (but SIGTERM works). So far I have been unable to reproduce the behaviour in isolation. It might somehow depend on the precise options of mira. I've tried to get them from Admin/mira.py without success. What are the precises ML_OPTIONS and ISABELLE_USEDIR_OPTIONS here? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2012 post-release mode
On 05/23/2012 01:28 PM, Makarius wrote: Dear All, the current situation is as follows: * As of Isabelle/c5f7be4a1734 the http://isabelle.in.tum.de/repos/isabelle-release branch is merged again with the main line. * isatest is back testing http://isabelle.in.tum.de/repos/isabelle 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. The report on https://isabelle.in.tum.de/testboard/Isabelle/report/113b081700754f768fe458e15cd460a1 and http://isabelle.in.tum.de/testboard/Isabelle/report/7950b174d6e340aba223611991c32ec6 show some error messages, but they are not very informative. Any hints are welcome. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2012 post-release mode
On 23/05/2012, at 9:28 PM, Makarius wrote: > * Gerwin should know what needs to be done to release AFP for >Isabelle2012. The AFP is now on freeze until the update to 2012 is out. I will be branching off for the release itself, but to keep the merge back simple, please refrain from committing to the AFP repository until the release is out. Since everything is building fine at the moment I'm hoping for this to happen in no more than a day or two. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
