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

Makarius makarius at sketis.net
Fri Aug 3 15:35:27 CEST 2012


On Fri, 3 Aug 2012, Jasmin Christian Blanchette wrote:

> For Huffman, the "fixdoc" script is not critical. It replaces 'a with 
> \alpha and things like that. I can live without it. But what do you mean 
> by "regular system functions"?

This is how I first did it:

http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/d095ce0cdabf
user:        wenzelm
date:        Tue Jul 31 11:01:42 2012 +0200
files:       .hgignore thys/Huffman/IsaMakefile 
thys/Huffman/document/IsaMakefile thys/Huffman/document/fixdoc 
thys/Huffman/document/isabelletags.sty thys/Huffman/fixdoc
description:
more conventional document setup, using inner document/IsaMakefile to do 
the patching;


Since IsaMakefiles are becoming extinct soon, I later refined it as 
follows:

http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/293122866d12
tag:         tip
user:        wenzelm
date:        Fri Aug 03 12:21:12 2012 +0200
files:       thys/Huffman/ROOT thys/Huffman/document/IsaMakefile 
thys/Huffman/document/build thys/Huffman/document/fixdoc thys/ROOT
description:
modernized document/build;


See also Isabelle/63ef2f0cf8bb:

user:        wenzelm
date:        Fri Aug 03 12:37:31 2012 +0200
files:       NEWS doc-src/System/Thy/Presentation.thy 
doc-src/System/Thy/document/Presentation.tex lib/Tools/document
description:
simplified custom document/build script, instead of old-style 
document/IsaMakefile;


The latter also includes the updated documentation.


BTW, some of the perl substitions in Huffman/document/build no longer 
work, because the format of the generated LaTeX has changed slightly over 
the years.


 	Makarius



More information about the isabelle-dev mailing list