NAMEcoqchk - The Coq Proof Checker compiled libraries verifier
SYNOPSIScoqchk [ options ] modules
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.
modules is a list of modules to be checked. Modules can be referred to by a short or qualified name.
- -I dir, --include dir
in the include path
- -R dir coqdir
recursively map physical
makes coqchk less verbose.
- -admit module
tag the specified module and all its dependencies as trusted, and will
not be rechecked, unless explicitly requested by other options.
- -norec 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.
allows the checker to accept libraries that have been compiled with
print coqchk version and exit.
- -coqlib dir
overrides the default location of the standard library.
print coqchk standard library location and exit.
- -h, --help
print list of options
coqtop(1), coqc(1), coq_makefile(1), coqdep(1).
The Coq Reference Manual. The Coq web site: coq.inria.fr