[isabelle-dev] Proposing extensions to the Isabelle library?
nipkow at in.tum.de
Tue Jan 1 14:21:43 CET 2013
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.
More information about the isabelle-dev