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

[Makarius]

On Tue, 1 Jan 2013, Tobias Nipkow wrote:

> 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.

I am doing lots of changes and fixes of other people's changes all the 
time.  The document test is practically irrelevant, and I am not 
prescribing to people out there to do tests that I don't doing myself as 
well.


 	Makarius