← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to man/coqdoc.1

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
man/coqdoc.1
 
1
.TH coqdoc 1 "April, 2006"
 
2
 
 
3
.SH NAME
 
4
coqdoc \- A documentation tool for the Coq proof assistant
 
5
 
 
6
 
 
7
.SH SYNOPSIS
 
8
.B coqdoc
 
9
[
 
10
.B options
 
11
]
 
12
.B files
 
13
 
 
14
 
 
15
.SH DESCRIPTION
 
16
 
 
17
.B coqdoc
 
18
is a documentation tool for the Coq proof assistant.
 
19
It creates LaTeX or HTML documents from a set of Coq files.
 
20
See the Coq reference manual for documentation (url below).
 
21
 
 
22
 
 
23
.SH OPTIONS
 
24
 
 
25
.SS Overall options
 
26
 
 
27
.TP
 
28
.BI \-h
 
29
Help. Will give you the complete list of options accepted by coqdoc.
 
30
.TP
 
31
.B \-\-html
 
32
Select a HTML output.
 
33
.TP
 
34
.B \-\-latex
 
35
Select a LATEX output.
 
36
.TP
 
37
.B \-\-dvi
 
38
Select a DVI output.
 
39
.TP
 
40
.B \-\-ps
 
41
Select a PostScript output.
 
42
.TP
 
43
.B \-\-texmacs
 
44
Select a TeXmacs output.
 
45
.TP
 
46
.B \-\-stdout
 
47
Redirect the output to stdout
 
48
.TP
 
49
.BI \-o \ file, \-\-output \ file
 
50
Redirect the output into the file 
 
51
.I file.
 
52
.TP
 
53
.BI \-d \ dir, \ \-\-directory \ dir
 
54
Output files into directory 
 
55
.I dir 
 
56
instead of current directory (option
 
57
\-d does not change the filename specified with option \-o, if any).
 
58
.TP
 
59
.B \-s, \ \-\-short
 
60
Do not insert titles for the files. The default behavior is to insert
 
61
a title like ``Library Foo'' for each file.
 
62
.TP
 
63
.BI \-t \ string, \ \-\-title \ string
 
64
Set the document title.
 
65
.TP
 
66
.B \-\-body\-only
 
67
Suppress the header and trailer of the final document. Thus, you can
 
68
insert the resulting document into a larger one.
 
69
.TP
 
70
.BI \-p \ string, \ \-\-preamble \ string
 
71
Insert some material in the LATEX preamble, right before \\begin{document} (meaningless with \-html).
 
72
.TP
 
73
.BI \-\-vernac\-file \ file, \ \-\-tex\-file \ file
 
74
Considers the file `file' respectively as a .v (or .g) file or a .tex file.
 
75
.TP
 
76
.BI \-\-files\-from \ file
 
77
Read file names to process in file `file' as if they were given on the
 
78
command line. Useful for program sources splitted in several
 
79
directories.
 
80
.TP
 
81
.B \-q, \ \-\-quiet
 
82
Be quiet. Do not print anything except errors.
 
83
.TP
 
84
.B \-h, \ \-\-help
 
85
Give a short summary of the options and exit.
 
86
.TP
 
87
.B
 
88
\-v, \ \-\-version
 
89
Print the version and exit.
 
90
 
 
91
.SS Index options
 
92
 
 
93
Default behavior is to build an index, for the HTML output only, into
 
94
index.html.
 
95
 
 
96
.TP
 
97
.B \-\-no\-index
 
98
Do not output the index.
 
99
.TP
 
100
.B \-\-multi\-index
 
101
Generate one page for each category and each letter in the index,
 
102
together with a top page index.html.
 
103
 
 
104
.SS Table of contents option
 
105
 
 
106
.TP
 
107
.B \-toc, \ \-\-table\-of\-contents
 
108
Insert a table of contents. For a LATEX output, it inserts a
 
109
\\tableofcontents at the beginning of the document. For a HTML output,
 
110
it builds a table of contents into toc.html.
 
111
 
 
112
.SS Hyperlinks options
 
113
 
 
114
.TP
 
115
.B \-\-glob\-from \ file
 
116
Make references using Coq globalizations from file file. (Such
 
117
globalizations are obtained with Coq option \-dump\-glob).
 
118
 
 
119
.TP
 
120
.B \-\-no\-externals
 
121
Do not insert links to the Coq standard library.
 
122
 
 
123
.TP
 
124
.BI \-\-coqlib \ url
 
125
Set base URL for the Coq standard library (default is http://coq.inria.fr/library/).
 
126
 
 
127
.TP
 
128
.BI \-\-coqlib_path \ dir
 
129
Set the base path where the Coq files are installed, especially style files coqdoc.sty and coqdoc.css.
 
130
 
 
131
.TP
 
132
.BI \-R \ dir \  coqdir
 
133
Map physical directory dir to Coq logical directory coqdir (similarly
 
134
to Coq option \-R).
 
135
.B Note: 
 
136
option \-R only has effect on the files following it on the command
 
137
line, so you will probably need to put this option first.
 
138
 
 
139
.SS Contents options
 
140
 
 
141
.TP
 
142
.B \-g, \ \-\-gallina
 
143
Do not print proofs.
 
144
 
 
145
.TP
 
146
.B \-l, \ \-\-light
 
147
Light mode. Suppress proofs (as with \-g) and the following commands:
 
148
 
 
149
        * [Recursive] Tactic Definition
 
150
        * Hint / Hints
 
151
        * Require
 
152
        * Transparent / Opaque
 
153
        * Implicit Argument / Implicits
 
154
        * Section / Variable / Hypothesis / End 
 
155
 
 
156
The behavior of options \-g and \-l can be locally overridden using the (* begin show *) ... (* end show *) environment (see above).
 
157
 
 
158
.SS Language options
 
159
 
 
160
Default behavior is to assume ASCII 7 bits input files.
 
161
 
 
162
.TP 
 
163
.B \-latin1, \ \-\-latin1
 
164
Select ISO-8859-1 input files. It is equivalent to \-\-inputenc latin1
 
165
\-\-charset iso\-8859\-1.
 
166
 
 
167
.TP 
 
168
.B \-utf8, \ \-\-utf8
 
169
Select UTF-8 (Unicode) input files. It is equivalent to \-\-inputenc
 
170
utf8 \-\-charset utf\-8. LATEX UTF-8 support can be found at
 
171
http://www.ctan.org/tex\-archive/macros/latex/contrib/supported/unicode/.
 
172
 
 
173
.TP 
 
174
.BI \-\-inputenc \ string
 
175
Give a LATEX input encoding, as an option to LATEX package inputenc.
 
176
 
 
177
.TP
 
178
.BI \-\-charset \ string
 
179
Specify the HTML character set, to be inserted in the HTML header.
 
180
 
 
181
 
 
182
.SH SEE ALSO
 
183
 
 
184
.I
 
185
The Coq Reference Manual from http://coq.inria.fr/
 
186