[isabelle-dev] AFP failures
makarius at sketis.net
Tue Nov 26 13:44:29 CET 2013
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.
More information about the isabelle-dev