#######################################################################
#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
# <O___,, #        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              #
#   \VV/  #############################################################
#    //   #      This file is distributed under the terms of the      #
#         #       GNU Lesser General Public License Version 2.1       #
#######################################################################

# Makefile for the Coq documentation

# To compile documentation, you need the following tools:
# Dvi: latex (latex2e), bibtex, makeindex
# Pdf: pdflatex
# Html: hevea (http://hevea.inria.fr) >= 1.05

# The main entry point :

documentation: doc-$(WITHDOC)  ## see $(WITHDOC) in config/Makefile
doc-all: doc
doc-no:

.PHONY: documentation doc-all doc-no

######################################################################
### Variables
######################################################################

LATEX:=latex
BIBTEX:=BIBINPUTS=.: bibtex -min-crossrefs=10
MAKEINDEX:=makeindex
PDFLATEX:=pdflatex
DVIPS:=dvips
FIG2DEV:=fig2dev
CONVERT:=convert
HEVEA:=hevea
HACHA:=hacha
HEVEAOPTS:=-fix -exec xxdate.exe
HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea
HTMLSTYLE:=simple
export TEXINPUTS:=$(HEVEALIB):
COQTEXOPTS:=-boot -n 72 -sl -small

DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex

REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
  RefMan-gal.v.tex RefMan-ext.v.tex \
  RefMan-mod.v.tex RefMan-tac.v.tex \
  RefMan-cic.v.tex RefMan-lib.v.tex \
  RefMan-tacex.v.tex RefMan-syn.v.tex \
  RefMan-oth.v.tex RefMan-ltac.v.tex \
  RefMan-decl.v.tex RefMan-pro.v.tex RefMan-sch.v.tex \
  Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
  Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
  Setoid.v.tex Classes.v.tex Universes.v.tex \
  Misc.v.tex)

REFMANTEXFILES:=$(addprefix doc/refman/, \
  headers.sty Reference-Manual.tex \
  RefMan-pre.tex RefMan-int.tex RefMan-com.tex \
  RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex \
  AsyncProofs.tex ) \
  $(REFMANCOQTEXFILES) \

REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps

REFMANFILES:=$(REFMANTEXFILES) $(DOCCOMMON) $(REFMANEPSFILES) doc/refman/biblio.bib

REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png)


######################################################################
### General rules
######################################################################

.PHONY: doc doc-html doc-pdf doc-ps refman refman-quick tutorial
.PHONY: stdlib full-stdlib faq rectutorial refman-html-dir

INDEXURLS:=doc/refman/html/index_urls.txt

doc: refman faq tutorial rectutorial stdlib $(INDEXURLS)

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.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.pdf

doc-ps:\
  doc/tutorial/Tutorial.v.ps doc/refman/Reference-Manual.ps \
  doc/faq/FAQ.v.ps doc/stdlib/Library.ps doc/RecTutorial/RecTutorial.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

full-stdlib: \
  doc/stdlib/html/index.html doc/stdlib/FullLibrary.ps doc/stdlib/FullLibrary.pdf

faq: doc/faq/html/index.html doc/faq/FAQ.v.ps doc/faq/FAQ.v.pdf

rectutorial: doc/RecTutorial/RecTutorial.html \
  doc/RecTutorial/RecTutorial.ps doc/RecTutorial/RecTutorial.pdf

######################################################################
### Implicit rules
######################################################################

ifdef QUICK
%.v.tex: %.tex
	$(COQTEX) $(COQTEXOPTS) $<
else
%.v.tex: %.tex $(COQTEX) $(COQTOPEXE) $(ALLVO)
	$(COQTEX) $(COQTEXOPTS) $<
endif

%.ps: %.dvi
	(cd `dirname $<`; $(DVIPS) -q -o `basename $@` `basename $<`)

%.png: %.fig
	$(FIG2DEV) -L png -m 2 $< $@

%.pdf: %.fig
	$(FIG2DEV) -L pdftex $< $@
	$(FIG2DEV) -L pdftex_t -p `basename $@` $< $@_t

%.eps: %.fig
	$(FIG2DEV) -L pstex $< $@
	$(FIG2DEV) -L pstex_t -p `basename $@` $< $@_t

%.eps: %.png
	$(CONVERT) $< $@

######################################################################
# Macros for filtering outputs
######################################################################

HIDEBIBTEXINFO=| grep -v "^A level-1 auxiliary file"
SHOWMAKEINDEXERROR=egrep '^!! Input index error|^\*\* Input style error|^   --'

# Empty subsection levels in faq are on purpose
HEVEAFAQFILTER=2>&1 | grep -v "^Warning: List with no item"

######################################################################
# Common
######################################################################

### Version

doc/common/version.tex: config/Makefile
	printf '\\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) doc/refman/Reference-Manual.tex
	@(cd doc/refman;\
	$(LATEX) -interaction=batchmode Reference-Manual;\
	$(BIBTEX) -terse Reference-Manual $(HIDEBIBTEXINFO);\
	$(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\
	$(MAKEINDEX) -q Reference-Manual;\
	$(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\
	$(MAKEINDEX) -q Reference-Manual.tacidx -o Reference-Manual.tacind;\
	$(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\
	$(MAKEINDEX) -q Reference-Manual.comidx -o Reference-Manual.comind;\
	$(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\
	$(MAKEINDEX) -q Reference-Manual.optidx -o Reference-Manual.optind;\
	$(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\
	$(MAKEINDEX) -q Reference-Manual.erridx -o Reference-Manual.errind;\
	$(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\
	$(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\
	$(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\
	../tools/show_latex_messages -no-overfull Reference-Manual.log)

doc/refman/Reference-Manual.pdf: doc/refman/Reference-Manual.dvi $(REFMANPNGFILES)
	(cd doc/refman;\
	$(PDFLATEX) -interaction=batchmode Reference-Manual.tex;\
	../tools/show_latex_messages -no-overfull Reference-Manual.log)

### Reference Manual (browsable format)

doc/refman/Reference-Manual.html: doc/refman/styles.hva doc/refman/headers.hva doc/refman/Reference-Manual.dvi # to ensure bbl file
	(cd doc/refman; BIBINPUTS=.: $(HEVEA) $(HEVEAOPTS) ./styles.hva ./Reference-Manual.tex)

doc/refman/cover.html: doc/common/styles/html/$(HTMLSTYLE)/cover.html
	sed -e "s/COQVERSION/$(VERSION)/g" $< > $@

doc/refman/styles.hva: doc/common/styles/html/$(HTMLSTYLE)/styles.hva
	$(INSTALLLIB) $< doc/refman

INDEXES:= doc/refman/html/command-index.html doc/refman/html/tactic-index.html
ALLINDEXES:= doc/refman/html/index.html $(INDEXES)

refman-html-dir $(ALLINDEXES): doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
	       doc/refman/cover.html doc/refman/styles.hva doc/refman/index.html
	- rm -rf doc/refman/html
	$(MKDIR) doc/refman/html
	$(INSTALLLIB) $(REFMANPNGFILES) doc/refman/html
	(cd doc/refman/html; $(HACHA) -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html)
	$(INSTALLLIB) doc/refman/cover.html doc/refman/html/index.html
	-$(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html

refman-quick:
	(cd doc/refman;\
	$(PDFLATEX) -interaction=batchmode Reference-Manual.tex;\
	../tools/show_latex_messages -no-overfull Reference-Manual.log && \
	$(HEVEA) $(HEVEAOPTS) ./Reference-Manual.tex)

######################################################################
# Index file for CoqIDE
######################################################################

$(INDEXURLS): $(INDEXES)
	cat $< | grep li-indexenv | grep href= | sed -e 's@.*>\([^<]*\)</span>.*, <a href="\([^"]*\)">.*@\1,\2@' > $@


######################################################################
# Tutorial
######################################################################

doc/tutorial/Tutorial.v.dvi: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex
	(cd doc/tutorial;\
	$(LATEX) -interaction=batchmode Tutorial.v;\
	../tools/show_latex_messages Tutorial.v.log)

doc/tutorial/Tutorial.v.pdf: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex
	(cd doc/tutorial;\
	$(PDFLATEX) -interaction=batchmode Tutorial.v.tex;\
	../tools/show_latex_messages Tutorial.v.log)

doc/tutorial/Tutorial.v.html: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex
	(cd doc/tutorial; $(HEVEA) $(HEVEAOPTS) Tutorial.v)


######################################################################
# FAQ
######################################################################

doc/faq/FAQ.v.dvi: doc/common/version.tex doc/common/title.tex doc/faq/FAQ.v.tex doc/faq/axioms.eps
	(cd doc/faq;\
	$(LATEX) -interaction=batchmode FAQ.v;\
	$(BIBTEX) -terse FAQ.v;\
	$(LATEX) -interaction=batchmode FAQ.v > /dev/null;\
	$(LATEX) -interaction=batchmode FAQ.v > /dev/null;\
	../tools/show_latex_messages FAQ.v.log)

doc/faq/FAQ.v.pdf: doc/common/version.tex doc/common/title.tex doc/faq/FAQ.v.dvi doc/faq/axioms.pdf
	(cd doc/faq;\
        $(PDFLATEX) -interaction=batchmode FAQ.v.tex;\
	../tools/show_latex_messages FAQ.v.log)

doc/faq/FAQ.v.html: doc/faq/FAQ.v.dvi doc/faq/axioms.png # to ensure FAQ.v.bbl
	(cd doc/faq; ($(HEVEA) $(HEVEAOPTS) FAQ.v.tex $(HEVEAFAQFILTER)))

doc/faq/html/index.html: doc/faq/FAQ.v.html
	- rm -rf doc/faq/html
	$(MKDIR) doc/faq/html
	$(INSTALLLIB) doc/faq/interval_discr.v doc/faq/axioms.png doc/faq/html
	$(INSTALLLIB) doc/faq/FAQ.v.html doc/faq/html/index.html

######################################################################
# Standard library
######################################################################

### Standard library (browsable html format)

ifdef QUICK
doc/stdlib/html/genindex.html:
else
doc/stdlib/html/genindex.html: | $(COQDOC) $(ALLVO)
endif
	- rm -rf doc/stdlib/html
	$(MKDIR) doc/stdlib/html
	$(COQDOC) -q -d doc/stdlib/html --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \
	  -R theories Coq -R plugins Coq $(VFILES)
	mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html

doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index
	./doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/hidden-files

doc/stdlib/html/index.html: doc/stdlib/html/genindex.html doc/stdlib/index-list.html
	cat doc/common/styles/html/$(HTMLSTYLE)/header.html doc/stdlib/index-list.html > $@
	cat doc/common/styles/html/$(HTMLSTYLE)/footer.html >> $@

### Standard library (light version, full version is definitely too big)

ifdef QUICK
doc/stdlib/Library.coqdoc.tex:
else
doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO)
endif
	$(COQDOC) -q -boot --gallina --body-only --latex --stdout \
            -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@

doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex
	(cd doc/stdlib;\
	$(LATEX) -interaction=batchmode Library;\
	$(LATEX) -interaction=batchmode Library > /dev/null;\
	../tools/show_latex_messages -no-overfull Library.log)

doc/stdlib/Library.pdf: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.dvi
	(cd doc/stdlib;\
	$(PDFLATEX) -interaction=batchmode Library;\
	../tools/show_latex_messages -no-overfull Library.log)

### Standard library (full version if you're crazy enouth to try)

doc/stdlib/FullLibrary.tex: doc/stdlib/Library.tex
	sed -e 's/Library.coqdoc/FullLibrary.coqdoc/g;s/\\begin{document}/\\newcommand{\\textlambda}{\\ensuremath{\\lambda}}\\newcommand{\\textPi}{\\ensuremath{\\Pi}}\\begin{document}/' $< > $@

ifdef QUICK
doc/stdlib/FullLibrary.coqdoc.tex:
	$(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \
            -R theories Coq -R plugins Coq $(VFILES) > $@
	sed -i.tmp -e 's///g' $@ && rm $@.tmp
else
doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) $(ALLVO)
	$(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \
            -R theories Coq -R plugins Coq $(VFILES) > $@
	sed -i.tmp -e 's///g' $@ && rm $@.tmp
endif

doc/stdlib/FullLibrary.dvi: $(DOCCOMMON) doc/stdlib/FullLibrary.coqdoc.tex doc/stdlib/FullLibrary.tex
	(cd doc/stdlib;\
	$(LATEX) -interaction=batchmode FullLibrary;\
	$(LATEX) -interaction=batchmode FullLibrary > /dev/null;\
	../tools/show_latex_messages -no-overfull FullLibrary.log)

doc/stdlib/FullLibrary.pdf: $(DOCCOMMON) doc/stdlib/FullLibrary.coqdoc.tex doc/stdlib/FullLibrary.dvi
	(cd doc/stdlib;\
	$(PDFLATEX) -interaction=batchmode FullLibrary;\
	../tools/show_latex_messages -no-overfull FullLibrary.log)

######################################################################
# Tutorial on inductive types
######################################################################

doc/RecTutorial/RecTutorial.dvi: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.tex
	(cd doc/RecTutorial;\
	$(LATEX) -interaction=batchmode RecTutorial;\
	$(BIBTEX) -terse RecTutorial;\
	$(LATEX) -interaction=batchmode RecTutorial > /dev/null;\
	$(LATEX) -interaction=batchmode RecTutorial > /dev/null;\
	../tools/show_latex_messages RecTutorial.log)

doc/RecTutorial/RecTutorial.pdf: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.dvi
	(cd doc/RecTutorial;\
	$(PDFLATEX) -interaction=batchmode RecTutorial.tex;\
	../tools/show_latex_messages RecTutorial.log)

doc/RecTutorial/RecTutorial.html: doc/RecTutorial/RecTutorial.tex
	(cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial)

######################################################################
# Install all documentation files
######################################################################

.PHONY: install-doc install-doc-meta install-doc-html install-doc-printable install-doc-index-urls

install-doc: install-doc-meta install-doc-html install-doc-printable install-doc-index-urls

install-doc-meta:
	$(MKDIR) $(FULLDOCDIR)
	$(INSTALLLIB) doc/LICENSE $(FULLDOCDIR)/LICENSE.doc

install-doc-html: 
	$(MKDIR) $(addprefix $(FULLDOCDIR)/html/, refman stdlib faq)
	$(INSTALLLIB) doc/refman/html/* $(FULLDOCDIR)/html/refman 
	$(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib 
	$(INSTALLLIB) doc/RecTutorial/RecTutorial.html $(FULLDOCDIR)/html/RecTutorial.html
	$(INSTALLLIB) doc/faq/html/* $(FULLDOCDIR)/html/faq
	$(INSTALLLIB) doc/tutorial/Tutorial.v.html $(FULLDOCDIR)/html/Tutorial.html

install-doc-printable: 
	$(MKDIR) $(FULLDOCDIR)/ps $(FULLDOCDIR)/pdf
	$(INSTALLLIB) doc/refman/Reference-Manual.pdf \
		doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf
	$(INSTALLLIB) doc/refman/Reference-Manual.ps \
		doc/stdlib/Library.ps $(FULLDOCDIR)/ps
	$(INSTALLLIB) doc/tutorial/Tutorial.v.pdf $(FULLDOCDIR)/pdf/Tutorial.pdf
	$(INSTALLLIB) doc/RecTutorial/RecTutorial.pdf $(FULLDOCDIR)/pdf/RecTutorial.pdf
	$(INSTALLLIB) doc/faq/FAQ.v.pdf $(FULLDOCDIR)/pdf/FAQ.pdf
	$(INSTALLLIB) doc/tutorial/Tutorial.v.ps $(FULLDOCDIR)/ps/Tutorial.ps
	$(INSTALLLIB) doc/RecTutorial/RecTutorial.ps $(FULLDOCDIR)/ps/RecTutorial.ps
	$(INSTALLLIB) doc/faq/FAQ.v.ps $(FULLDOCDIR)/ps/FAQ.ps

install-doc-index-urls:
	$(MKDIR) $(FULLDATADIR)
	$(INSTALLLIB) $(INDEXURLS) $(FULLDATADIR)


###########################################################################
# Documentation of the source code (using ocamldoc)
###########################################################################

OCAMLDOCDIR=dev/ocamldoc

DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \
	./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \
	./parsing/*.mli ./proofs/*.mli \
	./tactics/*.mli ./stm/*.mli ./toplevel/*.mli ./ltac/*.mli)

# Defining options to generate dependencies graphs
DOT=dot
ODOCDOTOPTS=-dot -dot-reduce

.PHONY: source-doc mli-doc ml-doc

source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf

$(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi)
	$(SHOW)'OCAMLDOC -latex -o $@'
	$(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
	$(DOCMLIS) -noheader -t "Coq mlis documentation" \
	-intro $(OCAMLDOCDIR)/docintro -o $@.tmp
	$(SHOW)'OCAMLDOC utf8 fix'
	$(HIDE)$(OCAMLDOCDIR)/fix-ocamldoc-utf8 $@.tmp
	$(HIDE)cat $(OCAMLDOCDIR)/header.tex $@.tmp > $@
	rm $@.tmp

mli-doc: $(DOCMLIS:.mli=.cmi)
	$(SHOW)'OCAMLDOC -html'
	$(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \
	$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
	-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
	-css-style style.css

ml-dot: $(MLFILES)
	$(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES) \
	$(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot

%_dep.png: %.dot
	$(DOT) -Tpng $< -o $@

%_types.dot: %.mli
	$(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $<

OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
  $(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib))))

%.dot: | %.mllib.d
	$(OCAMLDOC_MLLIBD)

ml-doc:
	$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES)

parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d
	$(OCAMLDOC_MLLIBD)

grammar/grammar.dot : | grammar/grammar.mllib.d
	$(OCAMLDOC_MLLIBD)

tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d
	$(OCAMLDOC_MLLIBD)

%.dot: %.mli
	$(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $<

$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
	$(SHOW)'PDFLATEX $*.tex'
	$(HIDE)(cd $(OCAMLDOCDIR) ; pdflatex -interaction=batchmode $*.tex && pdflatex -interaction=batchmode $*.tex)
	$(HIDE)(cd doc/tools/; show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log)


# For emacs:
# Local Variables:
# mode: makefile
# End: