[isabelle-dev] Open Issues with JinjaThreads entry

Gerwin Klein gerwin.klein at nicta.com.au
Tue Oct 4 08:09:21 CEST 2011

On 04/10/2011, at 4:59 PM, Andreas Lochbihler wrote:

>>> the traditional isatest's AFP-Test did not report any failures the last few days,
>>> but the emerging testboard infrastructure mentions failures over the last few versions, and the current tips
>>> 76aec35b4898934df700ee54ce4d8fb7b99b0388:AFP,fa3715b35370fd27bc9e6bd03fad4a34b0724af3:Isabelle
>>> still seem to be broken.
>>> For people involved in this issue, here is a more detailed report:
>>> http://isabelle.in.tum.de/reports/Isabelle/report/37c2d104871b443f8b6dbd0a8b8b0314
>> The report just ends with "Interrupt". Is it possible that this is a time-out or similar?
> I would not call it broken - it's just lack of resources. It important line in the log is
> Run out of store - interrupting threads

Ah, didn't spot that. This indeed is the usual out of memory problem.

> The tail of the output log tells me that the interrupt occured when one of the huge locales get opened. On my local machine, JinjaThreads requires to build in single-threaded mode about 12G of memory plus a few more when the heap image is written.

Yes, I can confirm that: our server logs show a spike each night at around 12G. The test runs with -M 1 -q 0 -p 0 for JinjaThreads. 

Interesting to see that the spike is for opening the locale. This is one of the things that might hit us as well.


More information about the isabelle-dev mailing list