coqchk (1)

coqchk [ 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.

-Idir,--includedir

add directory dir in the include path

-Rdircoqdir

recursively map physical dir to logical coqdir

-silent

makes coqchk less verbose.

-admitmodule

tag the specified module and all its dependencies as trusted, and will not be rechecked, unless explicitly requested by other options.

-norecmodule

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 accept libraries that have been compiled with this flag.

-v

print coqchk version and exit.

-coqlibdir

overrides the default location of the standard library.

-where

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: http://coq.inria.fr