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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
