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).
Inspecting the Admin/isatest/isatest-doc script more closely, I've got the
impression that it assumes that the "at-poly" test has alrady finished, so
that the images are still lying around in their proper place.
That session used to be run on macbroy22, until I changed it to macbroy28
on 17-Jan-2011 to make it coincide with the machine of the doc test,
because I thought it would be one of these NFS flukes.
That was not the case, though. Inspecting /home/isatest/log for the past
few months reveals that the relevant "at-poly" test changed its behaviour
significantly on 07-Dec-2010: terminating very late in the morning, and
crashing poly on HOL-Nitpick_Examples, as can be seen e.g. in
/home/isatest/log/isatest-makeall-at-poly-2011-02-08-macbroy28.log
which also gives the reason for it (by chance as a consequence of
11ae688e4e30):
### 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.)
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.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
