diff options
| -rw-r--r-- | Makefile | 20 | ||||
| -rw-r--r-- | Makefile.build | 15 | ||||
| -rw-r--r-- | Makefile.common | 43 | ||||
| -rw-r--r-- | Makefile.doc | 240 | ||||
| -rw-r--r-- | Makefile.stage3 | 1 | ||||
| -rw-r--r-- | config/Makefile.template | 1 | ||||
| -rwxr-xr-x | configure | 39 | ||||
| -rw-r--r-- | doc/Makefile | 317 |
8 files changed, 330 insertions, 346 deletions
@@ -156,11 +156,21 @@ indepclean: rm -f revision docclean: -ifdef COQ_CONFIGURED - $(MAKE) -C doc clean -else - $(warning Clean of documentation requires "./configure" to be run; not done.) -endif + rm -f doc/*/*.dvi doc/*/*.aux doc/*/*.log doc/*/*.bbl doc/*/*.blg doc/*/*.toc \ + doc/*/*.idx doc/*/*~ doc/*/*.ilg doc/*/*.ind doc/*/*.dvi.gz doc/*/*.ps.gz doc/*/*.pdf.gz\ + doc/*/*.???idx doc/*/*.???ind doc/*/*.v.tex doc/*/*.atoc doc/*/*.lof\ + doc/*/*.hatoc doc/*/*.haux doc/*/*.hcomind doc/*/*.herrind doc/*/*.hidx doc/*/*.hind \ + doc/*/*.htacind doc/*/*.htoc doc/*/*.v.html + rm -f doc/stdlib/index-list.html doc/stdlib/index-body.html \ + doc/stdlib/Library.coqdoc.tex doc/stdlib/library.files \ + doc/stdlib/library.files.ls + rm -f doc/*/*.ps doc/*/*.pdf + rm -rf doc/refman/html doc/stdlib/html doc/faq/html doc/tutorial/tutorial.v.html + rm -f doc/stdlib/html/*.html + rm -f doc/refman/euclid.ml{,i} doc/refman/heapsort.ml{,i} + rm -f doc/common/version.tex + rm -f doc/refman/*.eps doc/refman/Reference-Manual.html + rm -f doc/coq.tex archclean: clean-ide cleantheories rm -f $(COQTOPOPT) $(BESTCOQTOP) $(COQC) $(COQMKTOP) diff --git a/Makefile.build b/Makefile.build index 86211d0c3..85bfb2e82 100644 --- a/Makefile.build +++ b/Makefile.build @@ -526,11 +526,6 @@ theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_STRICT) | $(HIDE)rm -f theories/Init/$*.glob $(HIDE)$(BOOTCOQTOP) -dump-glob theories/Init/$*.glob -nois -compile theories/Init/$* -# globalizations (for coqdoc) - -glob.dump: $(THEORIESVO:.vo=.glob) $(CONTRIBVO:.vo=.glob) - cat $^ > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) - ########################################################################### # tools ########################################################################### @@ -655,16 +650,6 @@ install-latex: # -$(UPDATETEX) ########################################################################### -# Documentation -# Literate programming (with ocamlweb) -########################################################################### - -.PHONY: doc - -doc: glob.dump | $(COQTEX) $(COQTOP) - $(MAKE) -C doc - -########################################################################### # Documentation of the source code (using ocamldoc) ########################################################################### diff --git a/Makefile.common b/Makefile.common index 8c87552ee..69bfe1fd8 100644 --- a/Makefile.common +++ b/Makefile.common @@ -53,6 +53,46 @@ TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) \ $(COQWC) $(COQDOC) ########################################################################### +# Documentation +########################################################################### + +LATEX:=latex +BIBTEX:=bibtex -min-crossrefs=10 +MAKEINDEX:=makeindex +PDFLATEX:=pdflatex +HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea +export TEXINPUTS:=$(COQSRC)/doc:$(HEVEALIB): +COQTEXOPTS:=-n 72 -image $(COQSRC)/$(COQTOP) -v -sl -small + +REFMANCOQTEXFILES:=\ + doc/refman/RefMan-gal.v.tex doc/refman/RefMan-ext.v.tex \ + doc/refman/RefMan-mod.v.tex doc/refman/RefMan-tac.v.tex \ + doc/refman/RefMan-cic.v.tex doc/refman/RefMan-lib.v.tex \ + doc/refman/RefMan-tacex.v.tex doc/refman/RefMan-syn.v.tex \ + doc/refman/RefMan-oth.v.tex doc/refman/RefMan-ltac.v.tex \ + doc/refman/RefMan-decl.v.tex \ + doc/refman/Cases.v.tex doc/refman/Coercion.v.tex doc/refman/Extraction.v.tex \ + doc/refman/Program.v.tex doc/refman/Omega.v.tex doc/refman/Polynom.v.tex \ + doc/refman/Setoid.v.tex doc/refman/Helm.tex # doc/refman/Natural.v.tex + +REFMANTEXFILES:=\ + doc/refman/headers.sty \ + doc/refman/Reference-Manual.tex doc/refman/RefMan-pre.tex \ + doc/refman/RefMan-int.tex doc/refman/RefMan-pro.tex \ + doc/refman/RefMan-com.tex \ + doc/refman/RefMan-uti.tex doc/refman/RefMan-ide.tex \ + doc/refman/RefMan-add.tex doc/refman/RefMan-modr.tex \ + $(REFMANCOQTEXFILES) \ + +REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps + +REFMANFILES:=$(REFMANTEXFILES) $(COMMON) $(REFMANEPSFILES) doc/refman/biblio.bib + +REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png) + + + +########################################################################### # Object and Source files ########################################################################### @@ -831,9 +871,10 @@ VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \ setoids sorting natural integer rational numbers noreal \ omega ring setoid_ring dp xml extraction field fourier jprover \ funind cc subtac rtauto +DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq rectutorial STAGE3_TARGETS:=world install coqide coqide-files coq coqlib \ coqlight states pcoq-files check init theories theories-light contrib \ - doc glob.dump $(VO_TARGETS) + $(DOC_TARGETS) $(VO_TARGETS) # For emacs: diff --git a/Makefile.doc b/Makefile.doc new file mode 100644 index 000000000..62b72d254 --- /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 diff --git a/Makefile.stage3 b/Makefile.stage3 index 1b9d880f0..1bd336d24 100644 --- a/Makefile.stage3 +++ b/Makefile.stage3 @@ -7,6 +7,7 @@ ####################################################################### include Makefile.stage2 +include Makefile.doc -include $(VFILES:.v=.v.d) .SECONDARY: $(VFILES:.v=.v.d) diff --git a/config/Makefile.template b/config/Makefile.template index 67c4c34d1..409e49467 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -30,6 +30,7 @@ LOCAL=LOCALINSTALLATION BINDIR="BINDIRDIRECTORY" COQLIB="COQLIBDIRECTORY" MANDIR="MANDIRDIRECTORY" +DOCDIR="DOCDIRDIRECTORY" EMACSLIB="EMACSLIBDIRECTORY" EMACS=EMACSCOMMAND @@ -35,7 +35,8 @@ usage () { echo "-bindir" echo "-libdir" echo "-mandir" - echo -e "\tSpecifies where to install bin/lib/man files resp.\n" + echo "-docdir" + echo -e "\tSpecifies where to install bin/lib/man/doc files resp.\n" echo "-emacslib" echo "-emacs" echo -e "\tSpecifies where emacs files are to be installed\n" @@ -101,6 +102,7 @@ prefix_spec=no bindir_spec=no libdir_spec=no mandir_spec=no +docdir_spec=no emacslib_spec=no emacs_spec=no camldir_spec=no @@ -141,6 +143,9 @@ while : ; do -mandir|--mandir) mandir_spec=yes mandir="$2" shift;; + -docdir|--mandir) docdir_spec=yes + docdir="$2" + shift;; -emacslib|--emacslib) emacslib_spec=yes emacslib="$2" shift;; @@ -540,7 +545,7 @@ esac #esac ########################################### -# bindir, libdir, mandir, etc. +# bindir, libdir, mandir, docdir, etc. case $src_spec in no) COQTOP=${COQSRC} @@ -556,14 +561,16 @@ case $ARCH in bindir_def='C:\coq\bin' libdir_def='C:\coq\lib' mandir_def='C:\coq\man' + docdir_def='C:\coq\doc' emacslib_def='C:\coq\emacs' coqdocdir_def='C:\coq\latex';; *) bindir_def=/usr/local/bin libdir_def=/usr/local/lib/coq mandir_def=/usr/local/man - emacslib_def=/usr/share/emacs/site-lisp - coqdocdir_def=/usr/share/texmf/tex/latex/misc;; + docdir_def=/usr/local/share/doc + emacslib_def=/usr/local/share/emacs/site-lisp + coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;; esac emacs_def=emacs @@ -608,6 +615,18 @@ case $mandir_spec/$prefix_spec/$local in esac;; esac +case $docdir_spec/$prefix_spec/$local in + yes/*/*) DOCDIR=$docdir;; + */yes/*) DOCDIR=$prefix/share/doc ;; + */*/true) DOCDIR=$COQTOP/man ;; + *) echo "Where should I install the Coq documentation [$docdir_def] ?" + read DOCDIR + case $DOCDIR in + "") DOCDIR=$docdir_def;; + *) true;; + esac;; +esac + case $emacslib_spec/$prefix_spec/$local in yes/*/*) EMACSLIB=$emacslib;; */yes/*) @@ -694,10 +713,11 @@ echo " CoqIde : $COQIDE" echo "" echo " Paths for true installation:" -echo " binaries will be copied in $BINDIR" -echo " library will be copied in $LIBDIR" -echo " man pages will be copied in $MANDIR" -echo " emacs mode will be copied in $EMACSLIB" +echo " binaries will be copied in $BINDIR" +echo " library will be copied in $LIBDIR" +echo " man pages will be copied in $MANDIR" +echo " documentation will be copied in $MANDIR" +echo " emacs mode will be copied in $EMACSLIB" echo "" ##################################################### @@ -720,6 +740,7 @@ case $ARCH in ESCCAMLDIR=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'` ESCCAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'` ESCMANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'` + ESCDOCDIR=`echo $DOCDIR |sed -e 's|\\\|\\\\\\\|g'` ESCEMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'` ESCCOQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'` ESCCAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'` @@ -733,6 +754,7 @@ case $ARCH in ESCCAMLDIR="$CAMLBIN" ESCCAMLLIB="$CAMLLIB" ESCMANDIR="$MANDIR" + ESCDOCDIR="$DOCDIR" ESCEMACSLIB="$EMACSLIB" ESCCOQDOCDIR="$COQDOCDIR" ESCCAMLP4BIN="$CAMLP4BIN" @@ -797,6 +819,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \ -e "s|BINDIRDIRECTORY|$ESCBINDIR|" \ -e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \ -e "s|MANDIRDIRECTORY|$ESCMANDIR|" \ + -e "s|DOCDIRDIRECTORY|$ESCDOCDIR|" \ -e "s|EMACSLIBDIRECTORY|$ESCEMACSLIB|" \ -e "s|EMACSCOMMAND|$EMACS|" \ -e "s|COQDOCDIRECTORY|$ESCCOQDOCDIR|" \ diff --git a/doc/Makefile b/doc/Makefile deleted file mode 100644 index 6e606ed19..000000000 --- a/doc/Makefile +++ /dev/null @@ -1,317 +0,0 @@ -# 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 ../config/Makefile - - -LATEX=latex -BIBTEX=bibtex -min-crossrefs=10 -MAKEINDEX=makeindex -PDFLATEX=pdflatex - -HEVEALIB=/usr/local/lib/hevea:/usr/lib/hevea -export TEXINPUTS=$(COQSRC)/doc:$(HEVEALIB): - -COQTOP=$(COQSRC)/bin/coqtop -COQTEX=$(COQSRC)/bin/coq-tex -n 72 -image $(COQTOP) -v -sl -small -COQDOC=$(COQSRC)/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 stdlib/html/*.html - rm -f refman/euclid.ml{,i} refman/heapsort.ml{,i} - rm -f common/version.tex - rm -f refman/*.eps refman/Reference-Manual.html - rm -f coq.tex - -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/RefMan-ltac.v.tex \ - refman/RefMan-decl.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.sty \ - refman/Reference-Manual.tex refman/RefMan-pre.tex \ - refman/RefMan-int.tex refman/RefMan-pro.tex \ - refman/RefMan-com.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/headers.hva 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/menu.html refman/html - cp refman/index.html refman/html - -refman-quick: - (cd refman; \ - $(PDFLATEX) Reference-Manual.tex; \ - hevea -fix -exec xxdate.exe ./Reference-Manual.tex) - - -###################################################################### -# 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 -###################################################################### - -LIBDIRS= Init Logic Bool Arith NArith ZArith QArith Relations Sets Setoids Lists Sorting Wellfounded IntMap FSets Reals Program -# We avoid Strings as String.v contains unicode caracters that make latex fail - -LIBDIRS+= Ints Ints/num Ints/Z -LIBDIRS+= Numbers Numbers/NatInt Numbers/Natural/Abstract Numbers/Natural/Binary Numbers/Natural/Peano Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary - - -ALLTHEORIES_VO=$(foreach dir, $(LIBDIRS), $(wildcard $(COQSRC)/theories/$(dir)/*.vo)) -ALLTHEORIES_V=$(ALLTHEORIES_VO:%.vo=%.v) -ALLTHEORIES_GLOB = $(ALLTHEORIES_V:%.v=%.glob) - -### Standard library (browsable html format) - -stdlib/index-body.html: $(ALLTHEORIES_V) - - rm -rf stdlib/html - mkdir stdlib/html - (cd stdlib/html;\ - $(COQDOC) -q --multi-index --html \ - -R $(COQSRC)/theories Coq $(ALLTHEORIES_V)) - mv stdlib/html/index.html stdlib/index-body.html - -stdlib/index-list.html: stdlib/index-list.html.template - COQTOP=$(COQSRC) ./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 \ - --coqlib_path $(COQSRC) \ - -R $(COQSRC)/theories Coq "$(COQSRC)/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 $(COQSRC)/LICENCE $(COQTOP)/CREDITS $(COQSRC)/COPYRIGHT $(DOCDIC) -# cp $(COQSRC)/README $(COQSRC)/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 |