[isabelle-dev] Isabelle manuals as regular session documents
Lars Noschinski
noschinl at in.tum.de
Thu Aug 30 15:32:49 CEST 2012
On 28.08.2012 19:17, Makarius wrote:
> This is an update on this ancient issue, which is not NEWS since it is
> not relevant to users, only for people hooked on the repository. It
> should nonetheless simplify many lives.
>
> This refers to Isabelle/037d32448e29, which also contains a short update
> on README_REPOSITORY.
>
> * The doc sessions now conform better to the current Isabelle document
> preparation system (from > 10 years ago) with some recent updates on
> the build process.
>
> * The sources are in src/Doc together with all other session sources.
> This is not nostalgy for the old name "Doc" from many years ago,
> but helps to grep/hypersearch over session sources exhaustively.
I am adapting the Haskabelle documentation build setup right now. The
build system for the Haskabelle documentation tries to reuse the TeX
machinery for Isabelle's documentation:
So, there is an "doc-src" directory in Haskebelle, containing only a
"Haskabelle" directory, containing the documentation. "doc-src" is then
populated with symlinks of the whole contents of ~~/doc-src and
~~/lib/texinputs. It then reuses Makefile.in for its own build-process.
It seems that all this is not needed anymore and I can just adapt the
configuration given for e.g.g ~~/src/Doc/Classes. However, I'm a bit
unsure about the dependencies I should give. My current ROOT file looks
like this:
session Haskabelle (doc) in "Haskabelle" = HOL +
options [document_variants = "haskabelle"]
theories [document = false] Setup
theories Haskabelle
files
"document/build"
"document/root.tex"
"document/style.sty"
However, the sessions ~~/src/Doc/ROOT contain various sets of
dependencies in ~~/src/Doc, e.g.:
Classes:
"../prepare_document"
"../pdfsetup.sty"
Functions:
"../prepare_document"
"../pdfsetup.sty"
"../iman.sty"
"../extra.sty"
"../isar.sty"
"../manual.bib"
Should I add these dependencies, too? (As $ISABELLE_HOME/src/Doc/...)?
Or should I omit them? They seem to be inconsistently handled in
~~/src/Doc/ROOT, too.
The dependencies of Classes are incomplete (probably
-- Lars
More information about the isabelle-dev
mailing list