FreeBSD Manual Pages
COQCHK(1) General Commands Manual COQCHK(1) NAME coqchk - verify compiled Coq libraries SYNOPSIS coqchk [ options ] 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 suc- ceeded. A non-zero return code means that something went wrong: some li- brary 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 to the include path. -Q dir coqdir Map physical dir to logical coqdir. -R dir coqdir Synonymous to -Q. -silent Be 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 COQCHK(1)
NAME | SYNOPSIS | DESCRIPTION | OPTIONS | SEE ALSO
Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=coqchk&sektion=1&manpath=FreeBSD+Ports+15.1.quarterly>