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 pro- duced 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 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 re- questing 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 veri- fied: 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.0.quarterly>