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