[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