[isabelle-dev] Isabelle manuals as regular session documents

[Makarius]

On Thu, 30 Aug 2012, Lars Noschinski wrote:

> 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

In principle the 'files' section should mention all informal files that 
are somehow needed to build the session. For the latex stuff, these are 
all shell scripts and style files -- there is also a corellation with the 
copying in document/build.

This already indicates a remaining weakness of the document build setup, 
because it resembles the old Makefiles too closely with its redundancy and 
uncertainty about dependencies.


I am already considering one more reform for the ROOT:

   document_files ...

specifies exactly the files that should be copied into the document build 
bed, before running any latex jobs.  Thus the duplication with 'files' and 
cp in document/build is avoided, and any omissions are more easily 
detected since without a copy of a required file latex won't run.

I did not move forward yet, because my impression is that the early 
adopters on this mailing list have difficulties to catch up.


 	Makarius