[isabelle-dev] Isabelle2012 post-release mode

[Gerwin Klein]

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
>