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