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
|
.TH COQCHK 1
.
.SH NAME
coqchk \- verify compiled Coq libraries
.
.
.SH SYNOPSIS
.B coqchk
[
options
]
.I modules
.
.
.SH DESCRIPTION
.
.B coqchk
is the standalone checker of compiled libraries (.vo files produced by
.BR coqc )
for the Coq Proof Assistant.
See the
.I Reference Manual
for more information.
It returns with exit code 0 if all the requested tasks succeeded.
A non-zero return code means that something went wrong: some
library was not found, corrupted content, type-checking failure, etc.
.PP
.I modules
is a list of modules to be checked.
Modules can be referred to by a short or qualified logical name,
or by their filename.
.
.SH OPTIONS
.
.TP
.BI \-I \ dir, \ \-\-include \ dir
Add directory
.I dir
to the include path.
.
.TP
.BI \-Q \ dir\ coqdir
Map physical
.I dir
to logical
.I coqdir.
.
.TP
.BI \-R \ dir\ coqdir
Synonymous to
.BR \-Q .
.
.TP
.B \-silent
Be less verbose.
.
.TP
.BI \-admit \ module
Tag the specified module and all its dependencies as trusted, and will
not be rechecked, unless explicitly requested by other options.
.
.TP
.BI \-norec \ module
Specifies that the given module shall be verified without requesting
to check its dependencies.
.
.TP
.BR \-m ,\ \-\-memory
Displays a summary of the memory used by the checker.
.
.TP
.BR \-o ,\ \-\-output\-context
Displays a summary of the logical content that have been
verified: assumptions and usage of impredicativity.
.
.TP
.B \-impredicative\-set
Allows the checker to accept libraries that have been compiled with
this flag.
.
.TP
.B \-v
Print
.B coqchk
version and exit.
.
.TP
.BI \-coqlib \ dir
Overrides the default location of the standard library.
.
.TP
.B \-where
Print coqchk standard library location and exit.
.
.TP
.BR \-h ,\ \-\-help
Print list of options.
.
.SH SEE ALSO
.
.BR coqtop (1),
.BR coqc (1),
.BR coq_makefile (1),
.BR coqdep (1)
.PP
.I
The Coq Reference Manual.
.PP
The Coq web site: http://coq.inria.fr
|
