[isabelle-dev] Open Issues with JinjaThreads entry

Andreas Lochbihler andreas.lochbihler at kit.edu
Tue Oct 4 07:59:57 CEST 2011

>> 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

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 


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum 
in der Helmholtz-Gemeinschaft

More information about the isabelle-dev mailing list