[isabelle-dev] \nexists

Lars Hupel hupel at in.tum.de
Fri Jul 15 15:46:53 CEST 2016

> 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.

Even more so because I will flip the switch to have Jenkins generate
devel.isa-afp.org including browser_info and documents this weekend.


More information about the isabelle-dev mailing list