table of contents
COQ(1) | General Commands Manual | COQ(1) |
NAME¶
coqchk - The Coq Proof Checker compiled libraries verifierSYNOPSIS¶
coqchk [ options ] modulesDESCRIPTION¶
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.
OPTIONS¶
- -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
SEE ALSO¶
coqtop(1), coqc(1), coq_makefile(1), coqdep(1).The Coq Reference Manual. The Coq web site: http://coq.inria.fr
July 7, 201 |