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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
