##########################################################################
## # 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)/$(CBIN)" COQLIB="$(CURDIR)/$(VO_OUT_DIR)"
endif
SPHINXWARNERROR ?= 1
ifeq ($(SPHINXWARNERROR),1)
SPHINXOPTS= -W
else
SPHINXOPTS=
endif
SPHINXBUILD= sphinx-build
SPHINXBUILDDIR= doc/sphinx/_build
DOCGRAMWARN ?= 0
ifeq ($(DOCGRAMWARN),0)
DOCGRAMWARN=-no-warn
else
DOCGRAMWARN=
endif
# Internal variables.
ALLSPHINXOPTS= -d $(SPHINXBUILDDIR)/doctrees $(SPHINXOPTS)
# Output directory setup
ifdef INSIDE_DUNE
ROOT_DOC_BUILD_DIR=_build
else
ROOT_DOC_BUILD_DIR=_build_vo
endif
DOC_BUILD_DIR=$(ROOT_DOC_BUILD_DIR)/default/doc
DOC_STDLIB_DIR=$(DOC_BUILD_DIR)/stdlib/
DOC_STDLIB_HTML_DIR=$(DOC_BUILD_DIR)/stdlib/html/
DOC_COMMON_DIR=$(DOC_BUILD_DIR)/common
######################################################################
### General rules
######################################################################
.PHONY: doc doc-html doc-pdf doc-ps
.PHONY: doc-stdlib doc-stdlib-html full-stdlib sphinx
doc: refman doc-stdlib
SPHINX_DEPS ?=
ifndef QUICK
SPHINX_DEPS := coq $(VO_OUT_DIR)user-contrib/Ltac2/ltac2_plugin.cmxs
endif
# refman-html and refman-latex
refman-%: $(SPHINX_DEPS) $(DOC_BUILD_DIR)/unreleased.rst
$(SHOW)'SPHINXBUILD doc/sphinx ($*)'
$(HIDE)cp -a $(DOC_BUILD_DIR)/unreleased.rst doc # to fix when we move the sphinx build out-of-tree
$(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
DOCCOMMON:=$(DOC_COMMON_DIR)/version.tex $(DOC_COMMON_DIR)/title.tex $(DOC_COMMON_DIR)/macros.tex
$(DOC_COMMON_DIR)/%.tex: doc/common/%.tex
$(HIDE)mkdir -p $(DOC_COMMON_DIR)
$(HIDE)cp -a $< $@
doc-html:\
$(DOC_STDLIB_HTML_DIR)/index.html refman-html
doc-pdf:\
$(DOC_STDLIB_DIR)/Library.pdf refman-pdf
doc-ps:\
$(DOC_STDLIB_DIR)/Library.ps
doc-stdlib-html: $(DOC_STDLIB_HTML_DIR)/index.html
doc-stdlib: \
$(DOC_STDLIB_HTML_DIR)/index.html $(DOC_STDLIB_DIR)/Library.ps $(DOC_STDLIB_DIR)/Library.pdf
full-stdlib: \
$(DOC_STDLIB_HTML_DIR)/index.html $(DOC_STDLIB_DIR)/FullLibrary.ps $(DOC_STDLIB_DIR)/FullLibrary.pdf
sphinx-clean:
rm -rf $(SPHINXBUILDDIR) doc/sphinx/index.rst doc/sphinx/zebibliography.rst
# We now require a install layout to be available.
.PHONY: plugin-tutorial
plugin-tutorial: states $(BCONTEXT)/coq-core.install | $(VO_OUT_DIR)
mkdir -p $(VO_OUT_DIR)/tools/
cp tools/CoqMakefile.in $(VO_OUT_DIR)/tools/
+$(MAKE) COQBIN=$(shell pwd)/$(CBIN)/ COQCORELIB=$(shell pwd)/$(CONTEXT)/lib/coq-core COQLIB=$(shell pwd)/$(VO_OUT_DIR) -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_BUILD_DIR)/unreleased.rst: $(wildcard doc/changelog/00-title.rst doc/changelog/*/*.rst)
$(SHOW)'AGGREGATE $@'
$(HIDE)mkdir -p $(DOC_BUILD_DIR)
$(HIDE)cat doc/changelog/00-title.rst doc/changelog/*/*.rst > $@
######################################################################
# Standard library
######################################################################
DOCLIBS=-R $(VO_OUT_DIR)theories Coq -Q $(VO_OUT_DIR)user-contrib/Ltac2 Ltac2
### Standard library (browsable html format)
ifdef QUICK
$(DOC_STDLIB_HTML_DIR)/genindex.html:
else
$(DOC_STDLIB_HTML_DIR)/genindex.html: | $(COQDOC) $(COQDOCCSS) $(ALLVO)
endif
- rm -rf $(DOC_STDLIB_HTML_DIR)
$(MKDIR) -p $(DOC_STDLIB_HTML_DIR)
$(SHOW)'COQDOC VFILES'
$(HIDE)export COQLIB=$(CONTEXT)/lib/coq-core && $(COQDOC) -q -d $(DOC_STDLIB_HTML_DIR) --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \
$(DOCLIBS) $(BUILD_VFILES)
mv $(DOC_STDLIB_HTML_DIR)/index.html $(DOC_STDLIB_HTML_DIR)/genindex.html
$(DOC_STDLIB_DIR)/index-list.html.template: doc/stdlib/index-list.html.template
$(HIDE)mkdir -p $(DOC_STDLIB_DIR)
$(HIDE)cp -a $< $@
$(DOC_STDLIB_DIR)/index-list.html: $(DOC_STDLIB_DIR)/index-list.html.template doc/stdlib/make-library-index
./doc/stdlib/make-library-index $(DOC_STDLIB_DIR)/index-list.html doc/stdlib/hidden-files
$(DOC_STDLIB_HTML_DIR)/index.html: $(DOC_STDLIB_HTML_DIR)/genindex.html $(DOC_STDLIB_DIR)/index-list.html
$(MKDIR) -p $(DOC_STDLIB_HTML_DIR)
cat doc/common/styles/html/$(HTMLSTYLE)/header.html $(DOC_STDLIB_DIR)/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_DIR)/Library.coqdoc.tex:
else
$(DOC_STDLIB_DIR)/Library.coqdoc.tex: | $(COQDOC) $(COQDOCSTY) $(THEORIESLIGHTVO)
endif
export COQLIB=$(CONTEXT)/lib/coq-core && $(COQDOC) -q -boot --gallina --body-only --latex --stdout \
-R $(VO_OUT_DIR)theories Coq $(THEORIESLIGHTVO:.$(VO)=.v) >> $@
SHOW_LATEX_MESSAGES:=$(shell pwd)/doc/tools/show_latex_messages
$(DOC_STDLIB_DIR)/Library.dvi: $(DOCCOMMON) $(DOC_STDLIB_DIR)/Library.coqdoc.tex $(DOC_STDLIB_DIR)/Library.tex
(cd $(DOC_STDLIB_DIR);\
$(LATEX) -interaction=batchmode Library;\
$(LATEX) -interaction=batchmode Library > /dev/null;\
$(SHOW_LATEX_MESSAGES) -no-overfull Library.log)
$(DOC_STDLIB_DIR)/Library.pdf: $(DOCCOMMON) $(DOC_STDLIB_DIR)/Library.coqdoc.tex $(DOC_STDLIB_DIR)/Library.dvi
(cd $(DOC_STDLIB_DIR);\
$(PDFLATEX) -interaction=batchmode Library;\
$(SHOW_LATEX_MESSAGES) -no-overfull Library.log)
$(DOC_STDLIB_DIR)/Library.tex: doc/stdlib/Library.tex
$(HIDE)cp -a $< $@
### Standard library (full version if you're crazy enough to try)
$(DOC_STDLIB_DIR)/FullLibrary.tex: $(DOC_STDLIB_DIR)/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_DIR)/FullLibrary.coqdoc.tex:
export COQLIB=$(CONTEXT)/lib/coq-core && $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \
$(DOCLIBS) $(BUILD_VFILES) > $@
sed -i.tmp -e 's///g' $@ && rm $@.tmp
else
$(DOC_STDLIB_DIR)/FullLibrary.coqdoc.tex: $(COQDOC) $(COQDOCSTY) $(ALLVO)
export COQLIB=$(CONTEXT)/lib/coq-core && $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \
$(DOCLIBS) $(BUILD_VFILES) > $@
sed -i.tmp -e 's///g' $@ && rm $@.tmp
endif
$(DOC_STDLIB_DIR)/FullLibrary.dvi: $(DOCCOMMON) $(DOC_STDLIB_DIR)/FullLibrary.coqdoc.tex $(DOC_STDLIB_DIR)/FullLibrary.tex
(cd $(DOC_STDLIB_DIR);\
$(LATEX) -interaction=batchmode FullLibrary;\
$(LATEX) -interaction=batchmode FullLibrary > /dev/null;\
$(SHOW_LATEX_MESSAGES) -no-overfull FullLibrary.log)
$(DOC_STDLIB_DIR)/FullLibrary.pdf: $(DOCCOMMON) $(DOC_STDLIB_DIR)/FullLibrary.coqdoc.tex $(DOC_STDLIB_DIR)/FullLibrary.dvi
(cd $(DOC_STDLIB_DIR);\
$(PDFLATEX) -interaction=batchmode FullLibrary;\
$(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
# Due to Windows paths not starting with / we can't just set the
# default to / and always use --destdir
ifeq ($(DESTDIR),)
DOCDIRDEST=$(DOCDIR)
else
DOCDIRDEST=$(DESTDIR)/$(DOCDIR)
endif
install-doc: install-doc-meta install-doc-html install-doc-printable
install-doc-meta:
$(MKDIR) $(DOCDIRDEST)
$(INSTALLLIB) doc/LICENSE $(DOCDIRDEST)/LICENSE.doc
install-doc-html: install-doc-stdlib-html install-doc-sphinx
install-doc-stdlib-html:
$(MKDIR) $(DOCDIRDEST)/html/stdlib
$(INSTALLLIB) $(DOC_STDLIB_HTML_DIR)/* $(DOCDIRDEST)/html/stdlib
install-doc-printable:
$(MKDIR) $(DOCDIRDEST)/ps $(DOCDIRDEST)/pdf
$(INSTALLLIB) $(DOC_STDLIB_DIR)/Library.pdf $(DOCDIRDEST)/pdf
$(INSTALLLIB) $(DOC_STDLIB_DIR)/Library.ps $(DOCDIRDEST)/ps
install-doc-sphinx:
$(MKDIR) $(DOCDIRDEST)/sphinx
(for d in html latex; do \
for f in `cd doc/sphinx/_build/$$d && find . -type f`; do \
$(MKDIR) $$(dirname $(DOCDIRDEST)/sphinx/$$d/$$f);\
$(INSTALLLIB) doc/sphinx/_build/$$d/$$f $(DOCDIRDEST)/sphinx/$$d/$$f;\
done; done)
######################################################################
# doc_grammar tool
######################################################################
# user-contrib/*/*.mlg omitted for now (e.g. ltac2)
PLUGIN_MLGS := $(wildcard plugins/*/*.mlg)
OMITTED_PLUGIN_MLGS :=
DOC_MLGS := $(wildcard */*.mlg) $(sort $(filter-out $(OMITTED_PLUGIN_MLGS), $(PLUGIN_MLGS))) \
user-contrib/Ltac2/g_ltac2.mlg
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) $(DOCGRAMWARN) -check-cmds -check-tacs $(DOC_MLGS) $(DOC_RSTS)
.PRECIOUS: doc/tools/docgram/orderedGrammar
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_GRAM) $(DOC_MLGS)
$(SHOW)'DOC_GRAM_VERIFY'
$(HIDE)$(DOC_GRAM) -no-warn -verify $(DOC_MLGS) $(DOC_RSTS)
doc_gram_rsts: doc/tools/docgram/updated_rsts
# For emacs:
# Local Variables:
# mode: makefile
# End: