Query: coqchk
OS: debian
Section: 1
Format: Original Unix Latex Style Formatted with HTML and a Horizontal Scroll Bar
COQ(1) General Commands Manual COQ(1)NAMEcoqchk - The Coq Proof Assistant compiled libraries verifierSYNOPSIScoqchk [ options ] files-or-modulesDESCRIPTIONcoqchk 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 optionsSEE ALSOcoqtop(1), coqc(1), coq_makefile(1), coqdep(1). The Coq Reference Manual. The Coq web site: http://coq.inria.fr February 9, 2009 COQ(1)