[isabelle-dev] Relations vs. Predicates

Makarius makarius at sketis.net
Thu Apr 26 20:17:07 CEST 2012

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.


More information about the isabelle-dev mailing list