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

Reply via email to