aboutsummaryrefslogtreecommitdiffhomepage
path: root/INSTALL.doc
diff options
context:
space:
mode:
Diffstat (limited to 'INSTALL.doc')
-rw-r--r--INSTALL.doc58
1 files changed, 25 insertions, 33 deletions
diff --git a/INSTALL.doc b/INSTALL.doc
index b71115bfa..13e6440d0 100644
--- a/INSTALL.doc
+++ b/INSTALL.doc
@@ -4,13 +4,13 @@
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.
+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
------------
@@ -20,12 +20,7 @@ To produce all the documents, the following tools are needed:
- latex (latex2e)
- pdflatex
- dvips
- - bibtex
- makeindex
- - fig2dev (transfig)
- - convert (ImageMagick)
- - hevea
- - hacha
- Python 3
- Sphinx 1.6.5 (http://www.sphinx-doc.org/en/stable/)
- sphinx_rtd_theme
@@ -34,17 +29,26 @@ To produce all the documents, the following tools are needed:
- Antlr4 runtime for Python 3
-Under Debian based operating systems (Debian, Ubuntu, ...) a
-working set of packages for compiling the documentation for Coq is:
+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:
- texlive texlive-latex-extra texlive-math-extra texlive-fonts-extra
- texlive-humanities texlive-pictures latex-xcolor hevea transfig
- imagemagick
- python3 python-pip3
+ pip3 install antlr4-python3-runtime
-To install the Python packages required to build the user manual, run:
- pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect
+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
-----------
@@ -66,17 +70,8 @@ Alternatively, you can use some specific targets:
make doc-html
to produce all html documents
- make refman
- to produce all formats 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 sphinx
+ to produce the HTML version of the reference manual
make stdlib
to produce all formats of the Coq standard library
@@ -93,7 +88,4 @@ To install all produced documents, do:
make DOCDIR=/some/directory/for/documentation install-doc
-DOCDIR defauts to /usr/share/doc/coq
-
-
-
+DOCDIR defaults to /usr/share/doc/coq