DragonFly On-Line Manual Pages

COQ(1)                 DragonFly 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
       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 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
              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                           COQ(1)