[isabelle-dev] Relations vs. Predicates
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