[isabelle-dev] Open Issues with JinjaThreads entry

[Gerwin Klein]

[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