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

[Makarius]

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