[isabelle-dev] Proposing extensions to the Isabelle library?
makarius at sketis.net
Tue Jan 1 14:27:25 CET 2013
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
More information about the isabelle-dev