[isabelle-dev] [Fwd: doc test failed]

[Makarius]

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