[isabelle-dev] Relations vs. Predicates

[Makarius]

On Wed, 18 Apr 2012, Christian Sternagel wrote:

>> This is only to make the manual compile again.
> This one didn't show up during 'isabelle makeall all'. Shouldn't 
> documentation be part of "all"? I guess then that a test should also include 
> "./Admin/build doc"? Anything else besides
>
>  isabelle makeall all
>  ./Admin/build doc
>
> to test a changeset (apart from external dependencies like the AFP)?

The doc test should be somehow more automated, but it will take a few more 
years of reforms to get there.  The doc-src setup is a bit special, since 
it predates the Isabelle document preparation system, which was only 
introduced recently in 1999/2000 or so.

There is never a complete test of everything.  You should take the results 
of "isabelle makeall all" and AFP admin/testall as indication of how a 
change could affect the dark matter of further Isabelle applications out 
there, and potentially determine the level of detail for the NEWS entry 
from that estimate.


 	Makarius