1COQ(1) General Commands Manual COQ(1)
2
3
4
6 coqchk - The Coq Proof Checker compiled libraries verifier
7
8
9
11 coqchk [ options ] modules
12
13
14
16 coqchk is the standalone checker of compiled libraries (.vo files pro‐
17 duced by coqc) for the Coq Proof Assistant. See the Reference Manual
18 for more information. It returns with exit code 0 if all the requested
19 tasks succeeded. A non-zero return code means that something went
20 wrong: some library was not found, corrupted content, type-checking
21 failure, etc.
22
23 modules is a list of modules to be checked. Modules can be referred to
24 by a short or qualified name.
25
26
28 -I dir, --include dir
29 add directory dir in the include path
30
31
32 -R dir coqdir
33 recursively map physical dir to logical coqdir
34
35
36 -silent
37 makes coqchk less verbose.
38
39
40 -admit module
41 tag the specified module and all its dependencies as trusted,
42 and will not be rechecked, unless explicitly requested by other
43 options.
44
45
46 -norec module
47 specifies that the given module shall be verified without
48 requesting to check its dependencies.
49
50
51 -m, --memory
52 displays a summary of the memory used by the checker.
53
54
55 -o, --output-context
56 displays a summary of the logical content that have been veri‐
57 fied: assumptions and usage of impredicativity.
58
59
60 -impredicative-set
61 allows the checker to accept libraries that have been compiled
62 with this flag.
63
64
65 -v print coqchk version and exit.
66
67
68 -coqlib dir
69 overrides the default location of the standard library.
70
71
72 -where print coqchk standard library location and exit.
73
74
75 -h, --help
76 print list of options
77
78
80 coqtop(1), coqc(1), coq_makefile(1), coqdep(1).
81 The Coq Reference Manual. The Coq web site: http://coq.inria.fr
82
83
84
85 July 7, 201 COQ(1)