[isabelle-dev] document_output vs. old document_dump/document_dump_mode

[Makarius]

On Thu, 30 Aug 2012, Tobias Nipkow wrote:

> I am still having some problems with it. Given
>
> session "HOL-IMP1" in "~~/src/HOL/IMP" = HOL +
>  options [document_output="IMP-generated", document=pdf]
>  theories
>    BExp
>
> then isabelle build -d . HOL-IMP1 puts IMP-generated into "~~/src/HOL/IMP" - I
> guess that is to be expeced. But I want it in my current directory. This works
>
> session "HOL-IMP1" in "~~/src/HOL/IMP" = HOL +
>  options [document_output="$THIS_DIR/IMP-generated", document=pdf]
>  theories
>    BExp
>
> but it requires me to set a shell variable THIS_DIR before invoking isabelle
> build. Is there a more elegant way to achive the same effect?

How did you achieve the effect of cwd before?  As far as I can tell, the 
document dump directory was always relative to the session sources.

In the ROOT specifications, any references to the file-system are relative 
to the location of the ROOT file itself.  Not writing 'in' means "." 
relatively to that.


> I tried removing the "in":
>
> session "HOL-IMP1" = HOL +
>  options [document_output="IMP-generated", document=pdf]
>  theories
>     "~~/src/HOL/IMP/BExp"
>
> But now I cannot find IMP-generated anywhere in my home directory. Where should
> I look?

Maybe you just need another run of build with option "-c" to ensure that 
the build is repeated.  Since files are identified via SHA1, it does not 
help to touch some of the sources.


Also note that document_output is not a 1-to-1 replacement for the old "-D 
generated" side-effect, it rather specifies the base directory the full 
document build-beds for each document_variant (which is just "document" by 
default).

The best starting point in the documentation at the moment is the section 
on "isabelle mkroot" in the system manual, and the ROOT that it generates. 
The example there also shows how build -D can be used as a shortcut to 
build the sessions with the ROOT in the given directory, to avoid some 
command-line redundancy.

There is some further material in chapter 4 on "presenting theories", but 
this is not complete yet.  I still don't have a systematic exposition of 
the build options.

Nonetheless, someone surprised me yesterday in using it at an expert 
level, with document_output=".", although that is not for the 
faint-hearted: it puts all the generated stuff right in the document 
template directory, hopefully without name clashes, especially on Mac OS 
file-systems.  Maybe this should be discontinued before it causes some 
harm.


 	Makarius