[isabelle-dev] \nexists

[Makarius]

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.

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