On 15/07/16 15:46, Lars Hupel wrote: >> 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. > > I disagree. 0% of LaTeX failures observed on the new infrastructure are > spurious, so I'm inclined to keep them running.
That is probably because of a very homogenous test environment. The isatest setup had a diversity of platforms and installations, e.g. strange OS X and exotic Linux (SuSE, Gentoo). That was often annoying, but also a reality check to some extent. It is unclear if and how we could get this platform zoo back: it was rather accidental due to different administration regimes. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev