[isabelle-dev] \nexists

[Tobias Nipkow]

On 15/07/2016 15:32, Makarius wrote:
> On 15/07/16 13:53, Johannes Hölzl wrote:
>> Am Freitag, den 15.07.2016, 12:15 +0200 schrieb Tobias Nipkow:
>>> LaTeX build problems are not infrequent and could be avoided easily
>>> if "build"
>>> produced the document by default.
>>
>> +1
>
> -10
>
> Every minute counts in the routine tests that I run continuously all the
> time. We are in fact again above 30min for "isabelle build -a" for my 12
> core machine, which is where the pain starts.

For me a default is something that a) is beneficial for the majority of users 
and b) can be overwritten if you don't like it. Isn't that possible here?

Tobias

> Latex tests add very little information for the extra time. It is
> usually easy to figure out what needs to be done to make a broken
> document work again. Moreover, the test often fails because of bad latex
> installations, not because of bad documents.
>
>
> This old problem has come back on us now, because the Jenkins test
> always produces documents -- and thus a lot of mails if something is
> broken there.
>
> Latex should be tested occasionally, but it could be done in a less
> intrusive manner. E.g. only once a day or once week.
>
>
> 	Makarius
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160715/5aef7ebe/attachment.bin>