[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
> * 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

However, the sessions ~~/src/Doc/ROOT contain various sets of 
dependencies in ~~/src/Doc, e.g.:



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