Plongement de doc/Makefile dans la nouvelle architecutre des Makefile

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10570 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 240 insertions, 0 deletions

diff --git a/Makefile.doc b/Makefile.doc
new file mode 100644
index 0000000000..62b72d254b
--- /dev/null
+++ b/Makefile.doc
@@ -0,0 +1,240 @@
+# Makefile for the Coq documentation
+
+# COQSRC 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 Makefile.common
+
+######################################################################
+### General rules
+######################################################################
+
+.PHONY: doc doc-html doc-pdf doc-ps refman tutorial stdlib faq rectutorial
+
+doc: doc-html doc-pdf doc-ps
+
+doc-html:\
+  doc/tutorial/Tutorial.v.html doc/refman/html/index.html \
+  doc/faq/html/index.html doc/stdlib/html/index.html doc/RecTutorial/RecTutorial.v.html
+
+doc-pdf:\
+  doc/tutorial/Tutorial.v.pdf doc/refman/Reference-Manual.pdf \
+  doc/faq/FAQ.v.pdf doc/stdlib/Library.pdf doc/RecTutorial/RecTutorial.v.pdf
+
+doc-ps:\
+  doc/tutorial/Tutorial.v.ps doc/refman/Reference-Manual.ps \
+  doc/faq/FAQ.v.ps stdlib/Library.ps doc/RecTutorial/RecTutorial.v.ps
+
+refman:\
+  doc/refman/html/index.html doc/refman/Reference-Manual.ps doc/refman/Reference-Manual.pdf
+
+tutorial:\
+  doc/tutorial/Tutorial.v.html doc/tutorial/Tutorial.v.ps doc/tutorial/Tutorial.v.pdf
+
+stdlib:\
+  doc/stdlib/html/index.html doc/stdlib/Library.ps doc/stdlib/Library.pdf
+
+faq:\
+  doc/faq/html/index.html doc/faq/FAQ.v.ps doc/faq/FAQ.v.pdf
+
+rectutorial:\
+  doc/RecTutorial/RecTutorial.v.html \
+  doc/RecTutorial/RecTutorial.v.ps RecTutorial/RecTutorial.v.pdf
+
+######################################################################
+### Implicit rules
+######################################################################
+
+%.v.tex: %.tex
+	(cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`)
+
+%.ps: %.dvi
+	(cd `dirname $<`; dvips -o `basename $@` `basename $<`)
+
+%.eps: %.png
+	pngtopnm $< | pnmtops -equalpixels -noturn -rle > $@
+
+######################################################################
+# Common
+######################################################################
+
+COMMON=doc/common/version.tex doc/common/title.tex doc/common/macros.tex 
+
+### Version
+
+doc/common/version.tex: config/Makefile
+	echo "\newcommand{\coqversion}{$(VERSION)}" > doc/common/version.tex
+
+######################################################################
+# Reference Manual
+######################################################################
+
+
+### Reference Manual (printable format)
+
+# The second LATEX compilation is necessary otherwise the pages of the index
+# are not correct (don't know why...) - BB
+doc/refman/Reference-Manual.dvi: $(REFMANFILES)
+	(cd doc/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)
+
+doc/refman/Reference-Manual.pdf: doc/refman/Reference-Manual.tex
+	(cd doc/refman; $(PDFLATEX) Reference-Manual.tex)
+
+### Reference Manual (browsable format)
+
+doc/refman/Reference-Manual.html: doc/refman/headers.hva doc/refman/Reference-Manual.dvi # to ensure bbl file
+	(cd doc/refman; hevea -fix -exec xxdate.exe ./Reference-Manual.tex)
+
+doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
+                        doc/refman/cover.html doc/refman/index.html
+	- rm -rf doc/refman/html
+	mkdir doc/refman/html
+	cp $(REFMANPNGFILES) doc/refman/html
+	(cd doc/refman/html; hacha -o toc.html ../Reference-Manual.html)
+	cp doc/refman/cover.html doc/refman/menu.html doc/refman/html
+	cp doc/refman/index.html doc/refman/html
+
+doc/refman-quick:
+	(cd doc/refman; \
+	 $(PDFLATEX) Reference-Manual.tex; \
+	 hevea -fix -exec xxdate.exe ./Reference-Manual.tex)
+
+
+######################################################################
+# Tutorial
+######################################################################
+
+doc/tutorial/Tutorial.v.dvi: doc/common/version.tex doc/common/title.tex doc/tutorial/Tutorial.v.tex
+	(cd doc/tutorial; $(LATEX) Tutorial.v)
+
+doc/tutorial/Tutorial.v.pdf: doc/common/version.tex doc/common/title.tex doc/tutorial/Tutorial.v.dvi
+	(cd doc/tutorial; $(PDFLATEX) Tutorial.v.tex)
+
+doc/tutorial/Tutorial.v.html: tutorial/Tutorial.v.tex
+	(cd doc/tutorial; hevea -exec xxdate.exe Tutorial.v)
+
+
+######################################################################
+# FAQ
+######################################################################
+
+doc/faq/FAQ.v.dvi: doc/common/version.tex doc/common/title.tex doc/faq/FAQ.v.tex
+	(cd faq;\
+	$(LATEX) FAQ.v;\
+	$(BIBTEX) FAQ.v;\
+	$(LATEX) FAQ.v;\
+	$(LATEX) FAQ.v)
+
+doc/faq/FAQ.v.pdf: common/version.tex common/title.tex faq/FAQ.v.dvi faq/axioms.png
+	(cd faq; $(PDFLATEX) FAQ.v.tex)
+
+doc/faq/FAQ.v.html: doc/faq/FAQ.v.dvi # to ensure FAQ.v.bbl
+	(cd doc/faq; hevea -fix FAQ.v.tex)
+
+doc/faq/html/index.html: doc/faq/FAQ.v.html
+	- rm -rf doc/faq/html
+	mkdir doc/faq/html
+	cp doc/faq/interval_discr.v doc/faq/axioms.png doc/faq/html
+	cp doc/faq/FAQ.v.html doc/faq/html/index.html
+
+######################################################################
+# Standard library
+######################################################################
+
+### Standard library (browsable html format)
+
+doc/stdlib/index-body.html: $(THEORIESVO:.vo=.glob)
+	- rm -rf doc/stdlib/html
+	mkdir doc/stdlib/html
+	$(COQDOC) -q -d doc/stdlib/html --multi-index --html \
+	  -R theories Coq $(THEORIESVO:.vo=.v)
+	mv doc/stdlib/html/index.html doc/stdlib/index-body.html
+
+doc/stdlib/index-list.html: doc/stdlib/index-list.html.template
+	COQTOP=$(COQSRC) ./doc/stdlib/make-library-index doc/stdlib/index-list.html
+
+doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.html doc/stdlib/index-trailer.html
+	cat doc/stdlib/index-list.html > $@
+	sed -n -e '/<table>/,/<\/table>/p' doc/stdlib/index-body.html >> $@
+	cat doc/stdlib/index-trailer.html >> $@
+
+### Standard library (light version, full version is definitely too big)
+
+doc/stdlib/Library.coqdoc.tex: $(THEORIESLIGHTVO:.vo=.glob)
+	$(COQSRC)/$(COQDOC) -q --gallina --body-only --latex --stdout \
+            -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@
+
+doc/stdlib/Library.dvi: $(COMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex
+	(cd doc/stdlib;\
+	$(LATEX) Library;\
+	$(LATEX) Library)
+
+doc/stdlib/Library.pdf: $(COMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.dvi
+	(cd doc/stdlib; $(PDFLATEX) Library)
+
+######################################################################
+# Tutorial on inductive types
+######################################################################
+
+doc/RecTutorial/RecTutorial.v.dvi: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.v.tex
+	(cd RecTutorial;\
+	 $(LATEX) RecTutorial.v;\
+	 $(BIBTEX) RecTutorial.v;\
+	 $(LATEX) RecTutorial.v;\
+	 $(LATEX) RecTutorial.v)
+
+doc/RecTutorial/RecTutorial.v.pdf: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.v.dvi
+	(cd doc/RecTutorial; $(PDFLATEX) RecTutorial.v.tex)
+
+doc/RecTutorial/RecTutorial.v.html: doc/RecTutorial/RecTutorial.v.tex
+	(cd doc/RecTutorial; hevea -exec xxdate.exe RecTutorial.v)
+
+
+######################################################################
+# Install all documentation files
+######################################################################
+
+HTMLINSTALLDIR=$(DOCDIR)/html
+PRINTABLEINSTALLDIR=$(DOCDIR)/ps
+
+install-doc: install-doc-meta install-doc-html install-doc-printable
+
+install-doc-meta:
+	mkdir $(DOCDIR)
+	cp doc/LICENCE $(DOCDIR)/LICENCE.doc
+#	cp $(COQSRC)/doc/LICENCE $(COQTOP)/doc/CREDITS $(COQSRC)/doc/COPYRIGHT $(DOCDIR)
+#	cp $(COQSRC)/doc/README $(COQSRC)/doc/CHANGES $(DOCDIR)
+
+install-doc-html: doc-html
+	mkdir $(HTMLINSTALLDIR)
+	cp -r doc/refman/html $(HTMLINSTALLDIR)/refman
+	cp -r doc/stdlib/html $(HTMLINSTALLDIR)/stdlib
+	cp -r doc/tutorial/tutorial.html $(HTMLINSTALLDIR)/
+	cp -r doc/RecTutorial/RecTutorial.html $(HTMLINSTALLDIR)/
+	cp -r doc/faq/html $(HTMLINSTALLDIR)/faq
+
+install-doc-printable: doc-pdf doc-ps
+	mkdir $(PRINTABLEINSTALLDIR)
+	cp -r doc/refman/Reference-manual.pdf $(PRINTABLEINSTALLDIR)
+	cp -r doc/stdlib/Library.pdf $(PRINTABLEINSTALLDIR)
+	cp -r doc/tutorial/Tutorial.v.pdf $(PRINTABLEINSTALLDIR)/Tutorial.pdf
+	cp -r doc/RecTutorial/RecTutorial.v.pdf $(PRINTABLEINSTALLDIR)/RecTutorial.pdf
+	cp -r doc/faq/FAQ.v.pdf $(PRINTABLEINSTALLDIR)/FAQ.pdf
+	cp -r doc/refman/Reference-manual.ps $(PRINTABLEINSTALLDIR)
+	cp -r doc/stdlib/Library.ps $(PRINTABLEINSTALLDIR)
+	cp -r doc/tutorial/Tutorial.v.ps $(PRINTABLEINSTALLDIR)/Tutorial.ps
+	cp -r doc/RecTutorial/RecTutorial.v.ps $(PRINTABLEINSTALLDIR)/RecTutorial.ps
+	cp -r doc/faq/FAQ.v.ps $(PRINTABLEINSTALLDIR)/FAQ.ps