[isabelle-dev] Isabelle manuals as regular session documents

Makarius makarius at sketis.net
Tue Aug 28 19:17:23 CEST 2012

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.

   * The Admin tool "isabelle build_doc" helps to populate the doc/
     directory on the spot, such that "isabelle doc" finds the results.
     This is again one less reason for the old-style development snapshot
     produced by isatest.  (Is anybody still working with that?)

Authors of non-outdated manuals should take a brief look if things still 
look the way they should be.  Latex is a bit weak in formally checking its 
input -- \include does not even stop on missing files.

Note that option document_output greatly helps to organized document 
output, but this particular option should not be hard-wired in public 
sessions, since it will spill output in some directory where it might not 
be wanted by others.

The old doc-src directory can now be purged manually in local clones, but 
this requires some care.  I've wiped out one of uncommitted my draft files 
today already.


More information about the isabelle-dev mailing list