[isabelle-dev] NEWS: Isabelle sessions and build management

[Makarius]

On Fri, 3 Aug 2012, Peter Lammich wrote:

> In Collections and refine-monadic, as far as I can remember, there are
> two specialties:
>  1. We use a book document class rather than the default article, which
> required some fine-tuning of the documents. We use text_raw
> "\chapter{...}" instead of header "".
>
>  2. We generate the userguide as a separate document, re-using the
> tex-files generated by the previous run of Isabelle.

See http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/592ecaab3932
how I addressed that.

The userguide is now just another document variant.  Since it uses a 
different documentclass than the other document variants "document" and 
"outline", I had to make a tiny little generalization here:

Isabelle/be8002ee43d8
user:        wenzelm
date:        Tue Jul 31 16:23:20 2012 +0200
files:       NEWS doc-src/System/Thy/Presentation.thy 
doc-src/System/Thy/document/Presentation.tex lib/Tools/document
description:
document variant NAME may use different LaTeX entry point 
document/root_NAME.tex if that file exists;


The aforementioned 
https://bitbucket.org/makarius/afp-build/raw/c39b1f29a0d1/NOTES file has 
the following pending items for your AFP sessions:

* Collections
   . check document
   . missing LammichLochbihler2010ITP
   . generated files (!?)

gen_algo/StdInst.thy: gen_algo/StdInst.in.thy
 	scripts/inst.rb < gen_algo/StdInst.in.thy > gen_algo/StdInst.thy

impl/Impl_Overview.thy: scripts/doc.rb spec/*.thy impl/*.thy
 	cat spec/*.thy impl/*.thy | scripts/doc.rb > 
impl/Impl_Overview.thy

* Refine_Monadic
   . check document


Is there really any *need* to have ruby produce theory sources?  Browsing 
through the outcome briefly, it looks very conventional: a few document 
antiquotations and a few defininitions/theorems/interpretations issued in 
Isabelle/ML should do the job.  The bit of Isabelle/ML should be shorter 
than the ruby stuff.


This is the only surviving case of generated sources in the reachable 
universe of Isabelle + AFP.

People out there are still free to work with funny make files around 
isabelle build, if they think they need it; its option -n reports the 
up-to-date status of the selected sessions without doing anything.


 	Makarius