[isabelle-dev] \nexists

[Makarius]

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