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