[isabelle-dev] AFP failures

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Tue Nov 26 11:52:14 CET 2013

Hi all,

The AFP tests are finally back, and this revealed a series of failures related to my refactorings last week. Looking more closely at the falures, I found they were all in the LaTeX generation, which I hadn't tested locally before pushing. In most of the theories, it's the LaTeX symbol \sqsubset that causes problem, because the necessary package is not included.

Does anybody have any idea of why this suddenly pops up as an issue just because I moved a few theories around?


More information about the isabelle-dev mailing list