diff options
Diffstat (limited to 'INSTALL.doc')
-rw-r--r-- | INSTALL.doc | 91 |
1 files changed, 0 insertions, 91 deletions
diff --git a/INSTALL.doc b/INSTALL.doc deleted file mode 100644 index 13e6440d0..000000000 --- a/INSTALL.doc +++ /dev/null @@ -1,91 +0,0 @@ - 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 |