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?
Has the isabelle tip changed
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
