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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
|
The Coq documentation
=====================
The Coq documentation includes
- A Reference Manual
- A document presenting the Coq standard library
The documentation of the latest released version is available on the Coq
web site at [coq.inria.fr/documentation](http://coq.inria.fr/documentation).
Additionally, you can view the reference manual for the development version
at <https://coq.github.io/doc/master/refman/>, and the documentation of the
standard library for the development version at
<https://coq.github.io/doc/master/stdlib/>.
The reference manual is written is reStructuredText and compiled
using Sphinx. See [`sphinx/README.rst`](sphinx/README.rst)
to learn more about the format that is used.
The documentation for the standard library is generated from
the `.v` source files using coqdoc.
Dependencies
------------
### HTML documentation
To produce the complete documentation in HTML, you will need Coq dependencies
listed in [`INSTALL.md`](../INSTALL.md). Additionally, the Sphinx-based
reference manual requires Python 3, and the following Python packages:
- sphinx >= 3.0.2
- sphinx_rtd_theme >= 0.4.3
- beautifulsoup4 >= 4.0.6
- antlr4-python3-runtime >= 4.7.1
- pexpect >= 4.2.1
- sphinxcontrib-bibtex >= 0.4.2
To install them, you should first install pip and setuptools (for instance,
with `apt install python3-pip python3-setuptools` on Debian / Ubuntu) then run:
pip3 install sphinx sphinx_rtd_theme beautifulsoup4 \
antlr4-python3-runtime==4.7.1 pexpect sphinxcontrib-bibtex
Nix users should get the correct development environment to build the
HTML documentation from Coq's [`default.nix`](../default.nix) (note this
doesn't include the LaTeX packages needed to build the full documentation).
### Other formats
To produce the documentation in PDF and PostScript formats, the following
additional tools are required:
- latex (latex2e)
- pdflatex
- dvips
- makeindex
- xelatex
- latexmk
All of them are part of the TexLive distribution. E.g. on Debian / Ubuntu,
install them with:
apt install texlive-full
Or if you want to use less disk space:
apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \
latexmk fonts-freefont-otf
### Setting the locale for Python
Make sure that the locale is configured on your platform so that Python encodes
printed messages with utf-8 rather than generating runtime exceptions
for non-ascii characters. The `.UTF-8` in `export LANG=C.UTF-8` sets UTF-8 encoding.
The `C` can be replaced with any supported language code. You can set the default
for a Docker build with `ENV LANG C.UTF-8`. (Python may look at other
environment variables to determine the locale; see the
[Python documentation](https://docs.python.org/3/library/locale.html#locale.getdefaultlocale)).
Compilation
-----------
To produce all documentation about Coq in all formats, 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 refman`
to produce the HTML and PDF versions of the reference manual
- `make refman-{html,pdf}`
to produce only one format of the reference manual
- `make doc-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.
To build the Sphinx documentation without stopping at the first
warning with the legacy Makefile, set `SPHINXWARNERROR` to 0 as such:
```
SPHINXWARNERROR=0 make refman-html
```
To do the same with the Dune build system, change the value of the
`SPHINXWARNOPT` variable (default is `-W`). The following will build
the Sphinx documentation without stopping at the first warning, and
store all the warnings in the file `/tmp/warn.log`:
```
SPHINXWARNOPT="-w/tmp/warn.log" dune build @refman-html
```
Installation
------------
To install all produced documents, do:
make install-doc
This will install the documentation in `/usr/share/doc/coq` unless you
specify another value through the `-docdir` option of `./configure` or
the `DOCDIR` environment variable. Note that `DOCDIR` controls the
root of the documentation, that is to say, in the example above, the
root is `/usr/share/doc`.
|
