Re: [isabelle-dev] [Fwd: doc test failed]
On 09/02/2011, at 1:50 AM, Makarius wrote: On Tue, 8 Feb 2011, Gerwin Klein wrote: The test should build all images, but it is possible that the doc test is started before the rest of the test gets there. Explicitly building ZF when processing doc-src should make that work. I'm about to push that change. We will see if that helps.. That's now eb5900951702, but it merely treats the symptoms by changing my traditional document setup in an adhoc fashion (and giving a misleading explanation in the log entry). Not really. Isar-Ref was the non-traditional one. All other documentation parts did exactly what Isar-Ref does now, which is what we do in all other Makefiles that refer to a logic image (and which is why the other ones worked). You're right that it does only treat the symptom, though. ### No timeout support on this ML platform This is a known (documented) feature of polyml-5.2, which is used in this test. To avoid further confusion in the future, I will discontinue this old Poly/ML version altogether and dispose the dummy versions of multithreading and timeouts. (Tests with real time parameters remain inherently erratic, of course.) Yes, that's a good idea. Another important question is why isatest did not report the failure of the important at-poly session, which is one of the core tests in some sense. That is indeed strange. I'll see if I can track it down. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [Fwd: doc test failed]
The test should build all images, but it is possible that the doc test is started before the rest of the test gets there. Explicitly building ZF when processing doc-src should make that work. I'm about to push that change. We will see if that helps.. Cheers, Gerwin On 06/02/2011, at 11:01 PM, Tobias Nipkow wrote: Yes, the missing ZF image is to be the problem. For some reason that has changed, as Slawomir Kolodynski also noticed. So we should either build ZF again or stop that test. Tobias Alexander Krauss schrieb: (please keep postings to isabelle-dev in English) Tobias Nipkow wrote: Seit Wochen wenn nicht Monaten bekomme ich alle paar Tage diese Fehlermeldung: More precisely, the error occurs (almost) daily since January 11th, according to my email archive. Fuehlt sich hier jemand zustaendig? So far, I didn't really feel responsible, since I don't know how the doc test works and what its implicit assumptions are. It seems though that the IsaMakefile for IsarRef assumes that the images are already present, whereas, e.g., in doc-src/ZF/IsaMakefile it is rebuilt explicitly. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] [Fwd: doc test failed]
Seit Wochen wenn nicht Monaten bekomme ich alle paar Tage diese Fehlermeldung: 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 Fuehlt sich hier jemand zustaendig? Tobias ---BeginMessage--- 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 ...
Re: [isabelle-dev] [Fwd: doc test failed]
(please keep postings to isabelle-dev in English) Tobias Nipkow wrote: Seit Wochen wenn nicht Monaten bekomme ich alle paar Tage diese Fehlermeldung: More precisely, the error occurs (almost) daily since January 11th, according to my email archive. Fuehlt sich hier jemand zustaendig? So far, I didn't really feel responsible, since I don't know how the doc test works and what its implicit assumptions are. It seems though that the IsaMakefile for IsarRef assumes that the images are already present, whereas, e.g., in doc-src/ZF/IsaMakefile it is rebuilt explicitly. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [Fwd: doc test failed]
Yes, the missing ZF image is to be the problem. For some reason that has changed, as Slawomir Kolodynski also noticed. So we should either build ZF again or stop that test. Tobias Alexander Krauss schrieb: (please keep postings to isabelle-dev in English) Tobias Nipkow wrote: Seit Wochen wenn nicht Monaten bekomme ich alle paar Tage diese Fehlermeldung: More precisely, the error occurs (almost) daily since January 11th, according to my email archive. Fuehlt sich hier jemand zustaendig? So far, I didn't really feel responsible, since I don't know how the doc test works and what its implicit assumptions are. It seems though that the IsaMakefile for IsarRef assumes that the images are already present, whereas, e.g., in doc-src/ZF/IsaMakefile it is rebuilt explicitly. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [Fwd: doc test failed]
On Sun, 6 Feb 2011, Tobias Nipkow wrote: Yes, the missing ZF image is to be the problem. For some reason that has changed, as Slawomir Kolodynski also noticed. So we should either build ZF again or stop that test. What Slawomir has noticed is merely the lack of ZF in official Isabelle2011, which was omitted to reduce the general bloat of the bundle. The doc test is quite different, part of isatest, and I don't quite understand how it works. I have made some attempts at NFS workarounds some weeks ago, without any change (I have also informed Gerwin about it). Alexander Krauss schrieb: It seems though that the IsaMakefile for IsarRef assumes that the images are already present, whereas, e.g., in doc-src/ZF/IsaMakefile it is rebuilt explicitly. This is the normal setup, at least for the manuals that I maintain. IsarRef also depends on HOL and HOLCF, and isatest did not complain about that missing. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
