diff options
Diffstat (limited to 'doc/Makefile')
| -rw-r--r-- | doc/Makefile | 300 |
1 files changed, 300 insertions, 0 deletions
diff --git a/doc/Makefile b/doc/Makefile new file mode 100644 index 00000000..07b13039 --- /dev/null +++ b/doc/Makefile @@ -0,0 +1,300 @@ +# Makefile for the Coq documentation + +# COQTOP needs to be set to a coq source repository + +# To compile documentation, you need the following tools: +# Dvi: latex (latex2e), bibtex, makeindex +# Pdf: pdflatex +# Html: hevea (http://hevea.inria.fr) >= 1.05 + +include ../config/Makefile + + +LATEX=latex +BIBTEX=bibtex -min-crossrefs=10 +MAKEINDEX=makeindex +PDFLATEX=pdflatex + +HEVEALIB=/usr/local/lib/hevea:/usr/lib/hevea +TEXINPUTS=$(HEVEALIB):.: + +DOCCOQTOP=$(COQTOP)/bin/coqtop +COQTEX=$(COQTOP)/bin/coq-tex -n 72 -image $(DOCCOQTOP) -v -sl -small +COQDOC=$(COQTOP)/bin/coqdoc + +#VERSION=POSITIONNEZ-CETTE-VARIABLE + +###################################################################### +### General rules +###################################################################### + +all: all-html all-pdf all-ps + +all-html:\ + tutorial/Tutorial.v.html refman/html/index.html \ + faq/html/index.html stdlib/html/index.html RecTutorial/RecTutorial.v.html + +all-pdf:\ + tutorial/Tutorial.v.pdf refman/Reference-Manual.pdf \ + faq/FAQ.v.pdf stdlib/Library.pdf RecTutorial/RecTutorial.v.pdf + +all-ps:\ + tutorial/Tutorial.v.ps refman/Reference-Manual.ps \ + faq/FAQ.v.ps stdlib/Library.ps RecTutorial/RecTutorial.v.ps + +refman:\ + refman/html/index.html refman/Reference-Manual.ps refman/Reference-Manual.pdf + +tutorial:\ + tutorial/Tutorial.v.html tutorial/Tutorial.v.ps tutorial/Tutorial.v.pdf + +stdlib:\ + stdlib/html/index.html stdlib/Library.ps stdlib/Library.pdf + +faq:\ + faq/html/index.html faq/FAQ.v.ps faq/FAQ.v.pdf + +rectutorial:\ + RecTutorial/RecTutorial.v.html \ + RecTutorial/RecTutorial.v.ps RecTutorial/RecTutorial.v.pdf + +###################################################################### +### Implicit rules +###################################################################### + +.SUFFIXES: .dvi .tex .v.tex .ps .pdf .eps .png + +%.v.tex: %.tex + (cd `dirname $<`; $(COQTEX) `basename $<`) + +%.ps: %.dvi + (cd `dirname $<`; dvips -o `basename $@` `basename $<`) + +%.eps: %.png + pngtopnm $< | pnmtops -equalpixels -noturn -rle > $@ + +clean: + rm -f */*.dvi */*.aux */*.log */*.bbl */*.blg */*.toc \ + */*.idx */*~ */*.ilg */*.ind */*.dvi.gz */*.ps.gz */*.pdf.gz\ + */*.???idx */*.???ind */*.v.tex */*.atoc */*.lof\ + */*.hatoc */*.haux */*.hcomind */*.herrind */*.hidx */*.hind \ + */*.htacind */*.htoc */*.v.html + rm -f stdlib/index-list.html stdlib/index-body.html \ + stdlib/Library.coqdoc.tex stdlib/library.files \ + stdlib/library.files.ls + rm -f refman/euclid.ml{,i} refman/heapsort.ml{,i} + rm -f common/version.tex + rm -f refman/*.eps refman/Reference-Manual.html + +cleanall: clean + rm -f */*.ps */*.pdf + rm -rf refman/html stdlib/html faq/html tutorial/tutorial.v.html + +###################################################################### +# Common +###################################################################### + +COMMON=common/version.tex common/title.tex common/macros.tex + +### Version + +common/version.tex: Makefile + echo "\newcommand{\coqversion}{$(VERSION)}" > common/version.tex + +###################################################################### +# Reference Manual +###################################################################### + +REFMANCOQTEXFILES=\ + refman/RefMan-gal.v.tex refman/RefMan-ext.v.tex \ + refman/RefMan-mod.v.tex refman/RefMan-tac.v.tex \ + refman/RefMan-cic.v.tex refman/RefMan-lib.v.tex \ + refman/RefMan-tacex.v.tex refman/RefMan-syn.v.tex \ + refman/RefMan-oth.v.tex \ + refman/Cases.v.tex refman/Coercion.v.tex refman/Extraction.v.tex \ + refman/Program.v.tex refman/Omega.v.tex refman/Polynom.v.tex \ + refman/Setoid.v.tex refman/Helm.tex # refman/Natural.v.tex + +REFMANTEXFILES=\ + refman/headers.tex \ + refman/Reference-Manual.tex refman/RefMan-pre.tex \ + refman/RefMan-int.tex refman/RefMan-pro.tex \ + refman/RefMan-com.tex refman/RefMan-ltac.tex \ + refman/RefMan-uti.tex refman/RefMan-ide.tex \ + refman/RefMan-add.tex refman/RefMan-modr.tex \ + $(REFMANCOQTEXFILES) \ + +REFMANEPSFILES= refman/coqide.eps refman/coqide-queries.eps + +REFMANFILES=\ + $(REFMANTEXFILES) $(COMMON) $(REFMANEPSFILES) refman/biblio.bib + +REFMANPNGFILES=$(REFMANEPSFILES:.eps=.png) + +### Reference Manual (printable format) + +# The second LATEX compilation is necessary otherwise the pages of the index +# are not correct (don't know why...) - BB +refman/Reference-Manual.dvi: $(REFMANFILES) + (cd refman;\ + $(LATEX) Reference-Manual;\ + $(BIBTEX) Reference-Manual;\ + $(LATEX) Reference-Manual;\ + $(MAKEINDEX) Reference-Manual;\ + $(MAKEINDEX) Reference-Manual.tacidx -o Reference-Manual.tacind;\ + $(MAKEINDEX) Reference-Manual.comidx -o Reference-Manual.comind;\ + $(MAKEINDEX) Reference-Manual.erridx -o Reference-Manual.errind;\ + $(LATEX) Reference-Manual;\ + $(LATEX) Reference-Manual) + +refman/Reference-Manual.pdf: refman/Reference-Manual.tex + (cd refman; $(PDFLATEX) Reference-Manual.tex) + +### Reference Manual (browsable format) + +refman/Reference-Manual.html: refman/Reference-Manual.dvi # to ensure bbl file + (cd refman; hevea -fix -exec xxdate.exe ./Reference-Manual.tex) + +refman/html/index.html: refman/Reference-Manual.html $(REFMANPNGFILES) \ + refman/cover.html refman/index.html + - rm -rf refman/html + mkdir refman/html + cp $(REFMANPNGFILES) refman/html + (cd refman/html; hacha -o toc.html ../Reference-Manual.html) + cp refman/cover.html refman/html + cp refman/index.html refman/html + +###################################################################### +# Tutorial +###################################################################### + +tutorial/Tutorial.v.dvi: common/version.tex common/title.tex tutorial/Tutorial.v.tex + (cd tutorial; $(LATEX) Tutorial.v) + +tutorial/Tutorial.v.pdf: common/version.tex common/title.tex tutorial/Tutorial.v.dvi + (cd tutorial; $(PDFLATEX) Tutorial.v.tex) + +tutorial/Tutorial.v.html: tutorial/Tutorial.v.tex + (cd tutorial; hevea -exec xxdate.exe Tutorial.v) + + +###################################################################### +# FAQ +###################################################################### + +faq/FAQ.v.dvi: common/version.tex common/title.tex faq/FAQ.v.tex + (cd faq;\ + $(LATEX) FAQ.v;\ + $(BIBTEX) FAQ.v;\ + $(LATEX) FAQ.v;\ + $(LATEX) FAQ.v) + +faq/FAQ.v.pdf: common/version.tex common/title.tex faq/FAQ.v.dvi faq/axioms.png + (cd faq; $(PDFLATEX) FAQ.v.tex) + +faq/FAQ.v.html: faq/FAQ.v.dvi # to ensure FAQ.v.bbl + (cd faq; hevea -fix FAQ.v.tex) + +faq/html/index.html: faq/FAQ.v.html + - rm -rf faq/html + mkdir faq/html + cp faq/interval_discr.v faq/axioms.png faq/html + cp faq/FAQ.v.html faq/html/index.html + +###################################################################### +# Standard library +###################################################################### + +GLOBDUMP=$(COQTOP)/glob.dump + +LIBDIRS= Logic Bool Arith ZArith Reals Lists Sets Relations Sorting Wellfounded IntMap FSets + +### Standard library (browsable html format) + +stdlib/index-body.html: $(GLOBDUMP) + - rm -rf stdlib/html + mkdir stdlib/html + (cd stdlib/html;\ + $(COQDOC) -q --multi-index --html --glob-from $(GLOBDUMP)\ + -R $(COQTOP)/theories Coq $(COQTOP)/theories/*/*.v) + mv stdlib/html/index.html stdlib/index-body.html + +stdlib/index-list.html: stdlib/index-list.html.template + COQTOP=$(COQTOP) ./stdlib/make-library-index stdlib/index-list.html + +stdlib/html/index.html: stdlib/index-list.html stdlib/index-body.html stdlib/index-trailer.html + cat stdlib/index-list.html > $@ + sed -n -e '/<table>/,/<\/table>/p' stdlib/index-body.html >> $@ + cat stdlib/index-trailer.html >> $@ + +### Standard library (printable format - produces > 350 pages) + +stdlib/Library.coqdoc.tex: + (for dir in $(LIBDIRS) ; do \ + $(COQDOC) -q --gallina --body-only --latex --stdout \ + -R $(COQTOP)/theories Coq "$(COQTOP)/theories/$$dir/"*.v >> $@ ; done) + +stdlib/Library.dvi: $(COMMON) stdlib/Library.coqdoc.tex stdlib/Library.tex + (cd stdlib;\ + $(LATEX) Library;\ + $(LATEX) Library) + +stdlib/Library.pdf: $(COMMON) stdlib/Library.coqdoc.tex stdlib/Library.dvi + (cd stdlib; $(PDFLATEX) Library) + +###################################################################### +# Tutorial on inductive types +###################################################################### + +RecTutorial/RecTutorial.v.dvi: common/version.tex common/title.tex RecTutorial/RecTutorial.v.tex + (cd RecTutorial;\ + $(LATEX) RecTutorial.v;\ + $(BIBTEX) RecTutorial.v;\ + $(LATEX) RecTutorial.v;\ + $(LATEX) RecTutorial.v) + +RecTutorial/RecTutorial.v.pdf: common/version.tex common/title.tex RecTutorial/RecTutorial.v.dvi + (cd RecTutorial; $(PDFLATEX) RecTutorial.v.tex) + +RecTutorial/RecTutorial.v.html: RecTutorial/RecTutorial.v.tex + (cd RecTutorial; hevea -exec xxdate.exe RecTutorial.v) + + +###################################################################### +# Install all documentation files +###################################################################### + +COQINSTALLPREFIX= +DOCDIR=/usr/local/share/doc/coq-8.0 +FULLDOCDIR=$(COQINSTALLPREFIX)$(DOCDIR) +HTMLINSTALLDIR=$(FULLDOCDIR)/html +PRINTABLEINSTALLDIR=$(FULLDOCDIR)/ps + +install-doc: install-meta install-doc-html install-doc-printable + +install-meta: + mkdir $(DOCDIC) + cp LICENCE $(DOCDIC)/LICENCE.doc +# cp $(COQTOP)/LICENCE $(COQTOP)/CREDITS $(COQTOP)/COPYRIGHT $(DOCDIC) +# cp $(COQTOP)/README $(COQTOP)/CHANGES $(DOCDIC) + +install-doc-html: all-html + mkdir $(HTMLINSTALLDIR) + cp -r refman/html $(HTMLINSTALLDIR)/refman + cp -r stdlib/html $(HTMLINSTALLDIR)/stdlib + cp -r tutorial/tutorial.html $(HTMLINSTALLDIR)/ + cp -r RecTutorial/RecTutorial.html $(HTMLINSTALLDIR)/ + cp -r faq/html $(HTMLINSTALLDIR)/faq + +install-doc-printable: all-pdf all-ps + mkdir $(PRINTABLEINSTALLDIR) + cp -r refman/Reference-manual.pdf $(PRINTABLEINSTALLDIR) + cp -r stdlib/Library.pdf $(PRINTABLEINSTALLDIR) + cp -r tutorial/Tutorial.v.pdf $(PRINTABLEINSTALLDIR)/Tutorial.pdf + cp -r RecTutorial/RecTutorial.v.pdf $(PRINTABLEINSTALLDIR)/RecTutorial.pdf + cp -r faq/FAQ.v.pdf $(PRINTABLEINSTALLDIR)/FAQ.pdf + cp -r refman/Reference-manual.ps $(PRINTABLEINSTALLDIR) + cp -r stdlib/Library.ps $(PRINTABLEINSTALLDIR) + cp -r tutorial/Tutorial.v.ps $(PRINTABLEINSTALLDIR)/Tutorial.ps + cp -r RecTutorial/RecTutorial.v.ps $(PRINTABLEINSTALLDIR)/RecTutorial.ps + cp -r faq/FAQ.v.ps $(PRINTABLEINSTALLDIR)/FAQ.ps |