Re: [isabelle] Document preparation hints

On Wed, 15 Jan 2014, Timothy Bourke wrote:

or globally on the isabelle build command line:

  isabelle build -o skip_proofs -D.

In fact, I find that this builds with skip_proofs are faster but that no .tex file is generated. Is the latter expected?

Abstractly, skip_proofs falls under the "too many options" syndrome of contempory Isabelle, so arbitrary behaviour can be expected in conjunction with other options, like document preparation. Since skip_proofs was once added as ad-hoc addition to the Isar top-level that was not exactly well-defined until today, it has fluctuated back and forth quite a lot over the years.

As far as I can see in Isabelle2013-2, skip_proofs now works with all Isar commands (including diagnostic commands and antiquotations), but its presence in some theory blanks-out the generated .tex file. (Document prepration requires intermediate toplevel states, but skipped ones are undefined.)

So for the purpose of this thread, "isabelle build -o skip_proofs" does not make any sense with document preparation. The flag should be added to individual theories within the session ROOT file, and the theories in question won't appear in the document.


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