[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? Cheers, Gerwin _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
