NAME¶
coqchk - The Coq Proof Assistant compiled libraries verifier
SYNOPSIS¶
coqchk [
options ]
files-or-modules
DESCRIPTION¶
coqchk is the standalone checker of compiled libraries (.vo files
produced by coqc) for the Coq Proof Assistant. See the 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.
files-or-modules is a list of modules to be checked. Modules can be
referred to either by a filename (without the .vo suffix) or by their
(possibly qualified) module name.
OPTIONS¶
- -I dir, --include dir
- add directory dir in the include path
- -R dir coqdir
- recursively map physical dir to logical
coqdir
- -where
- print Coq's standard library location and exit
- -silent
- makes coqchk less verbose.
- -admit file-or-module
- tag the specified module and all its dependencies as
trusted, and will not be rechecked, unless explicitly requested by other
options.
- -norec file-or-module
- specifies that the given module shall be verified without
requesting to check its dependencies
- -m, --memory
- displays a summary of the memory used by the checker
- -o, --output-context
- displays a summary of the logical content that have been
verified: assumptions and usage of impredicativity
- -impredicative-set
- allows the checker to verify libraries that have been
compiled with this flag.
- -v
- print Coq version and exit
- -where
- print Coq's standard library location and exit
- -h, --help
- print list of options
SEE ALSO¶
coqtop(1),
coqc(1),
coq_makefile(1),
coqdep(1).
The Coq Reference Manual. The Coq web site:
http://coq.inria.fr
