[isabelle-dev] Isabelle2012 post-release mode

[Gerwin Klein]

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-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>