[isabelle-dev] Isabelle manuals as regular session documents
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
More information about the isabelle-dev