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
