##########################################################################
##         #   The Coq Proof Assistant / The Coq Development Team       ##
##  v      #         Copyright INRIA, CNRS and contributors             ##
## <O___,, # (see version control and CREDITS file for authors & dates) ##
##   \VV/  ###############################################################
##    //   #    This file is distributed under the terms of the         ##
##         #     GNU Lesser General Public License Version 2.1          ##
##         #     (see LICENSE file for the text of the license)         ##
##########################################################################

# Makefile for the Coq documentation

# Read doc/README.md to learn about the dependencies

# 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
MAKEINDEX:=makeindex
PDFLATEX:=pdflatex
DVIPS:=dvips
HTMLSTYLE:=coqremote

# Sphinx-related variables
OSNAME:=$(shell uname -s)
ifeq ($(findstring CYGWIN,$(OSNAME)),CYGWIN)
WIN_CURDIR:=$(shell cygpath -w $(CURDIR))
SPHINXENV:=COQBIN="$(CURDIR)/bin/" COQLIB="$(WIN_CURDIR)"
else
SPHINXENV:=COQBIN="$(CURDIR)/bin/" COQLIB="$(CURDIR)"
endif
SPHINXWARNERROR ?= 1
ifeq ($(SPHINXWARNERROR),1)
SPHINXOPTS= -W
else
SPHINXOPTS=
endif
SPHINXBUILD= sphinx-build
SPHINXBUILDDIR= doc/sphinx/_build

# Internal variables.
ALLSPHINXOPTS= -d $(SPHINXBUILDDIR)/doctrees $(SPHINXOPTS)

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

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

.PHONY: doc doc-html doc-pdf doc-ps
.PHONY: doc-stdlib full-stdlib sphinx

doc: refman doc-stdlib

SPHINX_DEPS ?=
ifndef QUICK
SPHINX_DEPS := coq
endif

# refman-html and refman-latex
refman-%: $(SPHINX_DEPS) doc/unreleased.rst
	$(SHOW)'SPHINXBUILD doc/sphinx ($*)'
	$(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b $* \
		$(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/$*

COQREFMAN_FILES := $(wildcard $(SPHINXBUILDDIR)/latex/CoqRefMan*)
LATEX_REMOVE_FILES := $(filter-out $(SPHINXBUILDDIR)/latex/CoqRefMan.tex, $(COQREFMAN_FILES))
refman-pdf: refman-latex
	rm -f $(LATEX_REMOVE_FILES)
	+$(MAKE) -C $(SPHINXBUILDDIR)/latex LATEXMKOPTS=-silent

refman: $(SPHINX_DEPS)
	+$(MAKE) refman-html
	+$(MAKE) refman-pdf

# compatibility alias
sphinx: refman-html

doc-html:\
  doc/stdlib/html/index.html refman-html

doc-pdf:\
  doc/stdlib/Library.pdf refman-pdf

doc-ps:\
  doc/stdlib/Library.ps

doc-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

sphinx-clean:
	rm -rf $(SPHINXBUILDDIR)

.PHONY: plugin-tutorial
plugin-tutorial: states tools
	+$(MAKE) COQBIN=$(PWD)/bin/ -C $(PLUGINTUTO)

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

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

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

### Version

doc/common/version.tex: config/Makefile
	printf '\\newcommand{\\coqversion}{$(VERSION)}' > doc/common/version.tex

### Changelog

doc/unreleased.rst: $(wildcard doc/changelog/00-title.rst doc/changelog/*/*.rst)
	$(SHOW)'AGGREGATE $@'
	$(HIDE)cat doc/changelog/00-title.rst doc/changelog/*/*.rst > $@

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

DOCLIBS=-R theories Coq -Q user-contrib/Ltac2 Ltac2

### 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 \
	  $(DOCLIBS) $(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 enough 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 \
            $(DOCLIBS) $(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 \
            $(DOCLIBS) $(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)

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

.PHONY: install-doc install-doc-meta install-doc-html install-doc-printable \
	install-doc-sphinx install-doc-stdlib-html

install-doc: install-doc-meta install-doc-html install-doc-printable

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

install-doc-html: install-doc-stdlib-html install-doc-sphinx

install-doc-stdlib-html:
	$(MKDIR) $(FULLDOCDIR)/html/stdlib
	$(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib

install-doc-printable: 
	$(MKDIR) $(FULLDOCDIR)/ps $(FULLDOCDIR)/pdf
	$(INSTALLLIB) doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf
	$(INSTALLLIB) doc/stdlib/Library.ps $(FULLDOCDIR)/ps

install-doc-sphinx:
	$(MKDIR) $(FULLDOCDIR)/sphinx
	(for d in html latex; do \
	for f in `cd doc/sphinx/_build/$$d && find . -type f`; do \
		$(MKDIR) $$(dirname $(FULLDOCDIR)/sphinx/$$d/$$f);\
		$(INSTALLLIB) doc/sphinx/_build/$$d/$$f $(FULLDOCDIR)/sphinx/$$d/$$f;\
	done; done)

######################################################################
# doc_grammar tool
######################################################################

DOC_GRAMCMO := $(addsuffix .cmo, $(addprefix coqpp/, coqpp_parse coqpp_lex))

$(DOC_GRAM): $(DOC_GRAMCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml doc/tools/docgram/doc_grammar.ml
	$(SHOW)'OCAMLC -a $@'
	$(HIDE)$(OCAMLC) -I coqpp $^ -package str -linkall -linkpkg -o $@

# user-contrib/*/*.mlg omitted for now (e.g. ltac2)
PLUGIN_MLGS := $(wildcard plugins/*/*.mlg)
OMITTED_PLUGIN_MLGS := plugins/ssr/ssrparser.mlg plugins/ssr/ssrvernac.mlg plugins/ssrmatching/g_ssrmatching.mlg \
	plugins/ssrsearch/g_search.mlg
DOC_MLGS := $(wildcard */*.mlg) $(sort $(filter-out $(OMITTED_PLUGIN_MLGS), $(PLUGIN_MLGS)))
DOC_EDIT_MLGS := $(wildcard doc/tools/docgram/*.edit_mlg)
DOC_RSTS := $(wildcard doc/sphinx/*/*.rst) $(wildcard doc/sphinx/*/*/*.rst)

doc/tools/docgram/fullGrammar: $(DOC_GRAM) $(DOC_MLGS)
	$(SHOW)'DOC_GRAM'
	$(HIDE)$(DOC_GRAM) -short -no-warn $(DOC_MLGS)

#todo: add a dependency of sphinx on updated_rsts when we're ready
doc/tools/docgram/orderedGrammar doc/tools/docgram/updated_rsts: doc/tools/docgram/fullGrammar $(DOC_GRAM) $(DOC_EDIT_MLGS)
	$(SHOW)'DOC_GRAM_RSTS'
	$(HIDE)$(DOC_GRAM) -check-cmds -check-tacs $(DOC_MLGS) $(DOC_RSTS)

doc/tools/docgram/updated_rsts: doc/tools/docgram/orderedGrammar

.PHONY: doc_gram doc_gram_verify doc_gram_rsts

doc_gram: doc/tools/docgram/fullGrammar

doc_gram_verify: doc/tools/docgram/fullGrammar
	$(SHOW)'DOC_GRAM_VERIFY'
	$(HIDE)$(DOC_GRAM) -short -no-warn -verify $(DOC_MLGS) $(DOC_RSTS)

doc_gram_rsts: doc/tools/docgram/updated_rsts


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