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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev