[isabelle-dev] AFP failures

[Gerwin Klein]

On 26 Nov 2013, at 11:44 pm, Makarius <makarius at sketis.net> wrote:

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

Correct.

This is not really a good situation to be in. Generally, we set up AFP documents such that they contain only theories of the entry itself, and nothing of other entries or libraries.

Sometimes this happens with explicit “document = False” options, and sometimes by making sure these other theories are contained in previous sessions.

The explicit option leads to the theory still being included in the HTML session, which we would also like to avoid.

Trying to make sure other theories are in previous sessions such as Library leads to the problem above.

I don’t have a good solution. We could try to use both mechanisms above at the same time, but it’s actually not easy to find all theories external to an entry if they are contained in previous sessions in the first place.

Cheers,
Gerwin

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.