blob: 2472d2b2a6e67cf0e68ee75e5a99feb5e90d60af (
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
|
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
- fig2dev (transfig)
- convert (ImageMagick)
- hevea
- hacha
Under Debian based operating systems (Debian, Ubuntu, ...) a
working set of packages for compiling the documentation for Coq is:
texlive texlive-latex-extra texlive-math-extra texlive-fonts-extra
texlive-humanities texlive-pictures latex-xcolor hevea transfig
imagemagick
Compilation
-----------
To produce all documentation about Coq, just run:
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 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 stdlib
to produce all formats of the Coq standard library
Installation
------------
To install all produced documents, do:
make DOCDIR=/some/directory/for/documentation install-doc
DOCDIR defauts to /usr/share/doc/coq
|
