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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
