COQ(1)                      General Commands Manual                     COQ(1)



NAME
       coqchk - The Coq Proof Checker compiled libraries verifier



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 name.


OPTIONS
       -I dir, --include dir
              add directory dir in the include path


       -R dir coqdir
              recursively map physical dir to logical coqdir


       -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  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



                                  July 7, 201                           COQ(1)
