[isabelle-dev] Isabelle2012 post-release mode
makarius at sketis.net
Fri May 25 14:17:34 CEST 2012
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
This is really odd. From the description it can only be a consequence of
this change from the isabelle-release repository:
date: Fri May 04 17:14:42 2012 +0200
refrain from SIGHUP handling (cf. 5f629ee2502b), which does not work on
Cygwin and appears to be redundant anyway (no extra output produced within
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
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?
More information about the isabelle-dev