[isabelle-dev] Document generation / Tags
makarius at sketis.net
Fri Sep 7 17:41:39 CEST 2012
On Thu, 6 Sep 2012, Lars Noschinski wrote:
> On 06.09.2012 12:09, Makarius wrote:
>> On Thu, 6 Sep 2012, Lars Noschinski wrote:
>>> On 06.09.2012 10:20, Florian Haftmann wrote:
>>>>> I see "isabelle document" has a simple option to switch on/off various
>>>>> things in the generated document (for example, proofs). Is there a way
>>>>> to supply these directly from the ROOT file? Would be useful for these
>>>>> one-off use cases (e.g. I want a view on my theory omitting all the
>>>> what about option document_variants?
>>> document_variants seems to be about the file name of the generated
>> The variants have names and tags to modify certain ranges of the text.
>> See option -V in old usedir in the system manual.
> Thanks; I've never really used document generation before, so I was not aware
> of this.
> Something else I discovered when I tried to use a build script:
> * Add a script document/build producing an error
> * Execute "isabelle build -c -o document=false" for your session. It
> will obviously fail.
With document=false it should not fail here. I think you have
document=pdf hardwired in ROOT, which takes precedence. Such persistent
document options are exactly what you do for private paper/slides
sessions, but not for public ones (Isabelle repository or AFP).
> * Remove document/build
> * Execute again "isabelle build -c -o document=false". It will fail
> * Completely remove the document_output directory
> * Execute again "isabelle build -c -o document=false". Now it will
> work again.
> It seems that some tool in the build chain could be more aggressive in
> cleaning up stuff.
It is the intended behaviour of document_output. The idea is to model the
old-fashioned situation where you lump together a lot of tex sources and
run some of the tex tools on it (latex, bibtex etc.), until you are
satisfied with the result.
This means intermediate states need to be preserved, even if they might
contain junk. In that case you do "rm -rf output" manually.
I've come across the description of the "aggressive" option -c of isabelle
document recently here
http://isabelle.in.tum.de/repos/isabelle/rev/342ca8f3197b#l4.272 and was
unsure about the delicate distinction in the behaviour. It will probably
become more clear when document preparation is done interactively, and
related reforms for it emerging.
More information about the isabelle-dev