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

[Gerwin Klein]

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