COQ(1)

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