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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
