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