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

[Tobias Nipkow]

Am 30/08/2012 22:37, schrieb 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.

I had to use a shell variable in the past. I just wondered if the new build
system might obviate that.

Tobias

> 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