[isabelle-dev] JinjaThreads

[Makarius]

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. 
>> http://isabelle.in.tum.de/reports/Isabelle/report/628b2a4bd3f94f478b929b72f811c5af. 
>> 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 
extend.

But there is another problem with JinjaThreads right now:

   Isabelle/d43ddad41d81
   AFP/3dcc6b9eae2b

   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.


 	Makarius