--- Begin Message ---
Session(s) IsarRef/ in the documentation test failed (log attached).
Test ended on: macbroy28, Sun Feb 6 08:20:21 CET 2011.
Have a nice day,
isatest
Start test at Sun Feb 6 08:17:01 CET 2011
Testing [Classes/]
Running HOL-Thy ...
Timing HOL-Thy (1 threads, 2.259s elapsed time, 2.216s cpu time, 0.147s GC time)
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/Classes/Thy/document
Finished HOL-Thy (0:00:03 elapsed time, 0:00:02 cpu time)
Finished [Classes/]
Testing [Codegen/]
make: Nothing to be done for `default'.
Finished [Codegen/]
Testing [Functions/]
make: Nothing to be done for `default'.
Finished [Functions/]
Testing [IsarImplementation/]
make: Nothing to be done for `default'.
Finished [IsarImplementation/]
Testing [IsarOverview/]
Running HOL-Isar ...
Timing HOL-Isar (1 threads, 1.813s elapsed time, 1.773s cpu time, 0.139s GC time)
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/IsarOverview/Isar/document
Finished HOL-Isar (0:00:03 elapsed time, 0:00:02 cpu time)
Finished [IsarOverview/]
Testing [IsarRef/]
Running HOL-IsarRef ...
Timing HOL-IsarRef (1 threads, 5.306s elapsed time, 5.152s cpu time, 0.523s GC time)
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/IsarRef/Thy/document
Finished HOL-IsarRef (0:00:07 elapsed time, 0:00:05 cpu time, factor 0.71)
Running HOLCF-IsarRef ...
Timing HOLCF-IsarRef (1 threads, 0.093s elapsed time, 0.092s cpu time, 0.000s GC time)
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/IsarRef/Thy/document
Finished HOLCF-IsarRef (0:00:01 elapsed time, 0:00:00 cpu time)
Running ZF-IsarRef ...
Unknown logic "ZF" -- no heap file found in:
/home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux
/mnt/home/isatest/isadist/Isabelle_06-Feb-2011/heaps/polyml-5.2_x86-linux
ZF-IsarRef FAILED
(see also /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/log/ZF-IsarRef)
make: *** [/home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux/log/ZF-IsarRef.gz] Error 2
Finished [IsarRef/]
Testing [LaTeXsugar/]
Running HOL-Sugar ...
Timing HOL-Sugar (1 threads, 0.992s elapsed time, 0.968s cpu time, 0.039s GC time)
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/LaTeXsugar/Sugar/document
Finished HOL-Sugar (0:00:02 elapsed time, 0:00:01 cpu time)
Finished [LaTeXsugar/]
Testing [Locales/]
Running HOL-Locales ...
Timing HOL-Locales (1 threads, 3.386s elapsed time, 3.365s cpu time, 0.333s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL/Locales
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/Locales/Locales/document
Finished HOL-Locales (0:00:05 elapsed time, 0:00:03 cpu time)
Finished [Locales/]
Testing [Main/]
Running HOL-Docs ...
Timing HOL-Docs (1 threads, 1.337s elapsed time, 1.313s cpu time, 0.106s GC time)
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/Main/Docs/document
Finished HOL-Docs (0:00:03 elapsed time, 0:00:01 cpu time)
Finished [Main/]
Testing [System/]
Running Pure-System ...
Timing Pure-System (1 threads, 0.544s elapsed time, 0.482s cpu time, 0.030s GC time)
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/System/Thy/document
Finished Pure-System (0:00:01 elapsed time, 0:00:00 cpu time)
Finished [System/]
Testing [TutorialI/]
make[1]: Entering directory `/mnt/home/isatest/isadist/Isabelle_06-Feb-2011/src/HOL'
make[2]: Entering directory `/mnt/home/isatest/isadist/Isabelle_06-Feb-2011/src/Pure'
make[2]: Nothing to be done for `Pure'.
make[2]: Leaving directory `/mnt/home/isatest/isadist/Isabelle_06-Feb-2011/src/Pure'
make[1]: Leaving directory `/mnt/home/isatest/isadist/Isabelle_06-Feb-2011/src/HOL'
Running HOL-ToyList ...
Timing HOL-ToyList (1 threads, 0.409s elapsed time, 0.391s cpu time, 0.000s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL/ToyList
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/TutorialI/ToyList/document
Finished HOL-ToyList (0:00:02 elapsed time, 0:00:00 cpu time)
Running HOL-ToyList2 ...
Timing HOL-ToyList2 (1 threads, 0.191s elapsed time, 0.182s cpu time, 0.000s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL/ToyList2
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/TutorialI/ToyList2/document
Finished HOL-ToyList2 (0:00:02 elapsed time, 0:00:00 cpu time)
Running HOL-Ifexpr ...
Timing HOL-Ifexpr (1 threads, 1.709s elapsed time, 1.700s cpu time, 0.154s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL/Ifexpr
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/TutorialI/Ifexpr/document
Finished HOL-Ifexpr (0:00:03 elapsed time, 0:00:02 cpu time)
Running HOL-CodeGen ...
Timing HOL-CodeGen (1 threads, 1.376s elapsed time, 1.373s cpu time, 0.121s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL/CodeGen
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/TutorialI/CodeGen/document
Finished HOL-CodeGen (0:00:02 elapsed time, 0:00:01 cpu time)
Running HOL-Trie ...
Timing HOL-Trie (1 threads, 2.869s elapsed time, 2.845s cpu time, 0.224s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL/Trie
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/TutorialI/Trie/document
Finished HOL-Trie (0:00:05 elapsed time, 0:00:03 cpu time)
Running HOL-Datatype ...
Timing HOL-Datatype (1 threads, 5.285s elapsed time, 5.262s cpu time, 0.488s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL/Datatype
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/TutorialI/Datatype/document
Finished HOL-Datatype (0:00:07 elapsed time, 0:00:05 cpu time, factor 0.71)
Running HOL-Fun ...
Timing HOL-Fun (1 threads, 1.815s elapsed time, 1.784s cpu time, 0.128s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL/Fun
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/TutorialI/Fun/document
Finished HOL-Fun (0:00:03 elapsed time, 0:00:02 cpu time)
Running HOL-Advanced ...
Timing HOL-Advanced (1 threads, 0.216s elapsed time, 0.196s cpu time, 0.000s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL/Advanced
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/TutorialI/Advanced/document
Finished HOL-Advanced (0:00:02 elapsed time, 0:00:00 cpu time)
Running HOL-Rules ...
Timing HOL-Rules (1 threads, 1.964s elapsed time, 1.934s cpu time, 0.146s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL/Rules
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/TutorialI/Rules/document
Finished HOL-Rules (0:00:04 elapsed time, 0:00:02 cpu time)
Running HOL-Sets ...
Timing HOL-Sets (1 threads, 14.431s elapsed time, 14.371s cpu time, 0.793s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL/Sets
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/TutorialI/Sets/document
Finished HOL-Sets (0:00:16 elapsed time, 0:00:14 cpu time, factor 0.87)
Running HOL-CTL ...
Timing HOL-CTL (1 threads, 3.401s elapsed time, 3.370s cpu time, 0.289s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL/CTL
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/TutorialI/CTL/document
Finished HOL-CTL (0:00:05 elapsed time, 0:00:03 cpu time)
Running HOL-Inductive ...
Timing HOL-Inductive (1 threads, 11.937s elapsed time, 11.870s cpu time, 0.762s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL/Inductive
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/TutorialI/Inductive/document
Finished HOL-Inductive (0:00:14 elapsed time, 0:00:12 cpu time, factor 0.85)
Running HOL-Types ...
Timing HOL-Types (1 threads, 3.755s elapsed time, 3.709s cpu time, 0.311s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL/Types
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/TutorialI/Types/document
Finished HOL-Types (0:00:05 elapsed time, 0:00:04 cpu time)
Running HOL-Misc ...
Timing HOL-Misc (1 threads, 2.923s elapsed time, 2.869s cpu time, 0.220s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL/Misc
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/TutorialI/Misc/document
Finished HOL-Misc (0:00:05 elapsed time, 0:00:03 cpu time)
Running HOL-Protocol ...
Timing HOL-Protocol (1 threads, 8.889s elapsed time, 8.854s cpu time, 0.832s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL/Protocol
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/TutorialI/Protocol/document
Finished HOL-Protocol (0:00:10 elapsed time, 0:00:09 cpu time, factor 0.90)
Running HOL-Documents ...
Timing HOL-Documents (1 threads, 1.438s elapsed time, 1.436s cpu time, 0.147s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/HOL/Documents
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/TutorialI/Documents/document
Finished HOL-Documents (0:00:02 elapsed time, 0:00:02 cpu time)
Finished [TutorialI/]
Testing [ZF/]
make[1]: Entering directory `/mnt/home/isatest/isadist/Isabelle_06-Feb-2011/src/ZF'
make[2]: Entering directory `/mnt/home/isatest/isadist/Isabelle_06-Feb-2011/src/FOL'
make[3]: Entering directory `/mnt/home/isatest/isadist/Isabelle_06-Feb-2011/src/Pure'
make[3]: Nothing to be done for `Pure'.
make[3]: Leaving directory `/mnt/home/isatest/isadist/Isabelle_06-Feb-2011/src/Pure'
make[2]: Leaving directory `/mnt/home/isatest/isadist/Isabelle_06-Feb-2011/src/FOL'
Building ZF ...
Timing ZF (1 threads, 51.702s elapsed time, 51.516s cpu time, 4.300s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/ZF
Document at /home/isatest/isabelle-at-poly/browser_info/ZF/document.pdf
Finished ZF (0:01:17 elapsed time, 0:01:11 cpu time, factor 0.92)
make[1]: Leaving directory `/mnt/home/isatest/isadist/Isabelle_06-Feb-2011/src/ZF'
Running ZF-. ...
Timing ZF-. (1 threads, 0.577s elapsed time, 0.556s cpu time, 0.040s GC time)
Browser info at /home/isatest/isabelle-at-poly/browser_info/ZF/.
Document sources at /mnt/home/isatest/hg-isabelle/doc-src/ZF/document
Finished ZF-. (0:00:01 elapsed time, 0:00:00 cpu time)
Finished [ZF/]
End test on Sun Feb 6 08:20:21 CET 2011, elapsed time: 0:03:20
Failed sessions: IsarRef/
--- End Message ---
