[isabelle-dev] Document generation / Tags

[Makarius]

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
>>>>> proofs).
>>>> 
>>>> what about option document_variants?
>>> 
>>> document_variants seems to be about the file name of the generated
>>> document.
>> 
>> 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
>    again
>  * 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.


 	Makarius