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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev