[isabelle-dev] Open Issues with JinjaThreads entry

Gerwin Klein gerwin.klein at nicta.com.au
Sun Oct 2 10:07:01 CEST 2011

[sorry for the incomplete email before, mail client accident..]

On 02/10/2011, at 6:57 PM, Lukas Bulwahn 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.

Interesting. It worked fine the last few days in the AFP test since Andreas fixed it, e.g. 2010-10-01 (testing against isabelle-RC1):

Testing [JinjaThreads]
cd /home/kleing/volatile/isadist/Isabelle_01-Oct-2011/src/HOL; /home/kleing/volatile/isadist/Isabelle_01-Oct-2011/bin/isabelle make HOL-Word
make[1]: Entering directory `/home/kleing/volatile/isadist/Isabelle_01-Oct-2011/src/HOL'
make[2]: Entering directory `/home/kleing/volatile/isadist/Isabelle_01-Oct-2011/src/Pure'
make[2]: Nothing to be done for `Pure'.
make[2]: Leaving directory `/home/kleing/volatile/isadist/Isabelle_01-Oct-2011/src/Pure'
Building HOL-Word ...
Timing HOL-Word (4 threads, 12.164s elapsed time, 32.254s cpu time, 3.208s GC time, factor 2.65)
Finished HOL-Word (0:00:34 elapsed time, 0:00:45 cpu time, factor 1.32)
make[1]: Leaving directory `/home/kleing/volatile/isadist/Isabelle_01-Oct-2011/src/HOL'
cd ..; /home/kleing/volatile/isadist/Isabelle_01-Oct-2011/bin/isabelle usedir -v true -i true -g true -d pdf -V outline=/proof,/ML -M 1 -q 0 -p 0 /home/kleing/afp/isabelle-afp-poly/heaps/polyml-5.4.0_x86_64-linux/HOL-Word JinjaThreads
Running HOL-Word-JinjaThreads ...
Timing HOL-Word-JinjaThreads (1 threads, 4084.464s elapsed time, 4078.263s cpu time, 650.917s GC time, factor 1.00)
Browser info at /home/kleing/afp/isabelle-afp-poly/browser_info/HOL/HOL-Word/JinjaThreads
Document at /home/kleing/afp/isabelle-afp-poly/browser_info/HOL/HOL-Word/JinjaThreads/document.pdf
Document at /home/kleing/afp/isabelle-afp-poly/browser_info/HOL/HOL-Word/JinjaThreads/outline.pdf
Finished HOL-Word-JinjaThreads (1:09:13 elapsed time, 1:09:03 cpu time, factor 0.99)
Finished [JinjaThreads]

> 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? It doesn't seem to be memory, that usually looks different.

Has the isabelle tip changed in anything that could be relevant to JinjaThreads?


More information about the isabelle-dev mailing list