1COQ(1)                      General Commands Manual                     COQ(1)
2
3
4

NAME

6       coqchk - The Coq Proof Checker compiled libraries verifier
7
8
9

SYNOPSIS

11       coqchk [ options ] modules
12
13
14

DESCRIPTION

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 logical name, or by their filename.
25
26

OPTIONS

28       -I dir, --include dir
29              add directory dir in the include path
30
31
32       -Q dir coqdir
33              map physical dir to logical coqdir
34
35
36       -R dir coqdir
37              synonymous for -Q
38
39
40       -silent
41              makes coqchk less verbose.
42
43
44       -admit module
45              tag  the  specified  module and all its dependencies as trusted,
46              and will not be rechecked, unless explicitly requested by  other
47              options.
48
49
50       -norec module
51              specifies  that  the  given  module  shall  be  verified without
52              requesting to check its dependencies.
53
54
55       -m, --memory
56              displays a summary of the memory used by the checker.
57
58
59       -o, --output-context
60              displays a summary of the logical content that have  been  veri‐
61              fied: assumptions and usage of impredicativity.
62
63
64       -impredicative-set
65              allows  the  checker to accept libraries that have been compiled
66              with this flag.
67
68
69       -v     print coqchk version and exit.
70
71
72       -coqlib dir
73              overrides the default location of the standard library.
74
75
76       -where print coqchk standard library location and exit.
77
78
79       -h, --help
80              print list of options
81
82

SEE ALSO

84       coqtop(1), coqc(1), coq_makefile(1), coqdep(1).
85       The Coq Reference Manual.  The Coq web site: http://coq.inria.fr
86
87
88
89                                                                        COQ(1)
Impressum