The Coq documentation ===================== The Coq documentation includes - A Reference Manual - A Tutorial - A document presenting the Coq standard library - A list of questions/answers in the FAQ style The sources of the documents are mainly made of LaTeX code from which user-readable PostScript or PDF files, or a user-browsable bunch of html files are generated. Prerequisite ------------ To produce all the documents, the following tools are needed: - latex (latex2e) - pdflatex - dvips - bibtex - makeindex - hevea - Python 3 - Sphinx 1.6.5 (http://www.sphinx-doc.org/en/stable/) - sphinx_rtd_theme - pexpect - beautifulsoup4 - Antlr4 runtime for Python 3 Under Debian based operating systems (Debian, Ubuntu, ...) a working set of packages for compiling the documentation for Coq is: texlive texlive-latex-extra texlive-math-extra texlive-fonts-extra texlive-humanities texlive-pictures latex-xcolor hevea python3 python-pip3 To install the Python packages required to build the user manual, run: pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex Compilation ----------- To produce all documentation about Coq, just run: ./configure (if you hadn't already) make doc Alternatively, you can use some specific targets: make doc-ps to produce all PostScript documents make doc-pdf to produce all PDF documents make doc-html to produce all html documents make sphinx to produce the HTML version of the reference manual make tutorial to produce all formats of the tutorial make rectutorial to produce all formats of the tutorial on recursive types make faq to produce all formats of the FAQ make stdlib to produce all formats of the Coq standard library Also note the "-with-doc yes" option of ./configure to enable the build of the documentation as part of the default make target. Installation ------------ To install all produced documents, do: make DOCDIR=/some/directory/for/documentation install-doc DOCDIR defauts to /usr/share/doc/coq