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
