[isabelle-dev] [Fwd: doc test failed]
makarius at sketis.net
Sun Feb 6 13:19:45 CET 2011
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
More information about the isabelle-dev