The Coq documentation ===================== The Coq documentation includes - A Reference Manual - A document presenting the Coq standard library The reference manual is written is reStructuredText and compiled using Sphinx (see `doc/sphinx/README.rst`) to learn more. The documentation for the standard library is generated from the `.v` source files using coqdoc. Prerequisite ------------ To produce all the documents, the following tools are needed: - latex (latex2e) - pdflatex - dvips - makeindex - Python 3 - Sphinx 1.6.5 (http://www.sphinx-doc.org/en/stable/) - sphinx_rtd_theme - pexpect - beautifulsoup4 - Antlr4 runtime for Python 3 Under recent Debian based operating systems (Debian 10 "Buster", Ubuntu 18.04, ...) a working set of packages for compiling the documentation for Coq is: texlive-latex-extra texlive-fonts-recommended python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex python3-pip Then, install the Python3 Antlr4 package: pip3 install antlr4-python3-runtime Nix users should get the correct development environment to build the HTML documentation from Coq's `default.nix`. [Note Nix setup doesn't include the LaTeX packages needed to build the full documentation.] If you are in an older/different distribution you can install the Python packages required to build the user manual using python3-pip: 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 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 defaults to /usr/share/doc/coq