blob: f8a0852805198bd9273fc9fd2d2ed9ac2cdb2f15 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
|
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
|
