nipkow at in.tum.de
Fri Jul 15 17:08:15 CEST 2016
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.
> 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?
> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev