Man page - coqchk(1)

Packages contains this manual

Package: coq
apt-get install coq

Manuals in package:

Documentations in package:

Manual

COQCHK

NAME
SYNOPSIS
DESCRIPTION
OPTIONS
SEE ALSO

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