coqchk - The Coq Proof Checker compiled libraries verifier
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 logical name, or by their filename.
- -I dir, --include dir
- add directory dir in the include path
- -Q dir coqdir
- map physical dir to logical coqdir
- -R dir coqdir
- synonymous for -Q
- -silent
- 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.
- -impredicative-set
- allows the checker to accept libraries that have been compiled with this
flag.
- -v
- print coqchk version and exit.
- -coqlib dir
- 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