summaryrefslogtreecommitdiff
path: root/INSTALL.doc
diff options
context:
space:
mode:
Diffstat (limited to 'INSTALL.doc')
-rw-r--r--INSTALL.doc105
1 files changed, 0 insertions, 105 deletions
diff --git a/INSTALL.doc b/INSTALL.doc
deleted file mode 100644
index f8a08528..00000000
--- a/INSTALL.doc
+++ /dev/null
@@ -1,105 +0,0 @@
- 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 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 hevea 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
-Sphinx 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 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
-
-
-