makarius at sketis.net
Fri Jan 13 18:24:18 CET 2012
On Thu, 12 Jan 2012, Lukas Bulwahn wrote:
> On 01/11/2012 09:29 PM, Alexander Krauss wrote:
>> The real problem is in fact JinjaThreads. AFAIK, the only machine at
>> TUM where it can still build (in principle) is lxbroy10, but as Lukas
>> pointed out there are still some failures, cf.
>> I hope that we can get further data on whether this is a repeatable
>> problem in the next days.
> NB: JinjaThreads has been failing in the mira testing of the
> configuration AFP-big since the beginning of testing on lxbroy10. Up to
> now, we don't know which system configurations is actually causing this
> failure. But nobody has spent much time to investigate this sofar.
I haven't been aware of that. The configuration goes back to myself, in
private communication with Alex. I did not check it later. In
4a892432e8f1 it is now more conventional, also tested manually to some
But there is another problem with JinjaThreads right now:
thys/JinjaThreads/Framework/FWDeadlock.thy line 251:
blast does not terminate and fills up memory
It looks like another set vs. pred thing stemming from coinductive_set
deadlocked further above.
An expert of "having a set-back" should know what to do here.
More information about the isabelle-dev