[isabelle-dev] Isabelle2012 post-release mode
gerwin.klein at nicta.com.au
Sat May 26 01:42:55 CEST 2012
Btw: manually killing perl (just 'kill') seems to work and let the rest of the scripts continue.
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.
> 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
>> 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?
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev