Re: [isabelle] Undefined facts in skip_proofs mode (take two)



> Hence my desire to pull out document processing into a separate job. Of
> course I don't want to recheck the whole AFP every time. My idea was to
> run everything using "skip_proofs".
>
> Gerwin pointed out to me yesterday that isatest does it too for some
> sessions.

To clarify that discussion from yesterday (we got interrupted, I think): isatest currently runs some specific sessions with skip_proofs. The purpose of these is not to generate documents, and it is indeed unclear to me if skip_proofs would not lead to a number of surprises, in particular for thm antiquotations, schematic lemmas and other fun things that can occur in documents.

That means, I donât think itâll work as a reliable method for getting documents quickly, at least not in general.

The purpose of skip_proofs is only to speed up interactive sessions for very large proofs, in the full knowledge that this sacrifices soundness for that session and that it may lead to unexpected results.

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.