[isabelle-dev] Isabelle2012 post-release mode

[Makarius]

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