[isabelle-dev] Proposing extensions to the Isabelle library?

[Tobias Nipkow]

Am 01/01/2013 14:10, schrieb Makarius:
> On Sun, 30 Dec 2012, Tobias Nipkow wrote:
> 
>>> The hints in README_REPOSITORY and the "system" manual suggest that "isabelle
>>> build -a" is the standard way to build all Isabelle sessions.
>>
>> In which case the latex document is not tested, which is why the wiki suggests
>> the longer invocation, to save other people unpleasant surprises.
> 
> This can be safely ignored.  I never do it like that myself.

At the risk of repeating myself: It can only be ignore safely if you don't mind
wasting other peoples time on it later.

> When the documents break, one can fix afterwards -- it is usually obvious how to
> do it.

"It is usually obvious how to fix it" is a non-argument for not checking for
such errors right away.

> No information is gained by spending more time here.

You gain the information if it is broken or not. It is not my time but machine
time, and a small fraction of the overall test time.

Tobias