[isabelle-dev] Isabelle2012 post-release mode

[Lukas Bulwahn]

On 05/25/2012 03:31 PM, Lukas Bulwahn wrote:
> On 05/25/2012 02: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?
>>
> They are the "default" options, but I do not know how they are 
> detected (your bash scripts?) and how to get this information.
>
> Lukas
>

Your attempt, changeset 6de952f4069f, was successful. lxbroy10 now can 
test all future changesets again.
Unfortunately, once mira tests older changesets it hangs, so all 
developers should please push to the testboard, tell me, and I will 
restart the daemon.


Lukas