[isabelle-dev] AFP failures

[Makarius]

On Tue, 26 Nov 2013, Johannes Hölzl wrote:

> Am Dienstag, den 26.11.2013, 13:12 +0100 schrieb Makarius:
> [..]
>>> I added now Zorn to HOL-Library (isa# acb41098607a), at least
>>> Coinductive works now.
>>
>> I don't understand this at all, neither the above explanation nor the
>> formal changeset (with its vacuous log message).
>>
>> How does the inclusion or non-inclusion of some theory affect the latex
>> macro environment?
>
> When Zorn is not in HOL-Library its tex-output is included in the
> document for AFP-Coinductive. The root.tex for AFP-Coinductive does not
> include the setup for \sqsubset, so its pdf-generation fails. By adding
> Zorn back to HOL-Library, the output for Zorn is not included in the pdf
> for AFP-Coinductive.

This means, by rearranging certain library sessions, AFP documents 
suddenly include theories into the document that are not meant to be 
there. We don't have a systematic check for this, so AFP documents are 
generally endangered.  It was merely a fortunate accident that the 
additional Zorn.tex of AFP/Coinductive was using undefined latex macros.


 	Makarius