rocqchk - Man Page

rocqchk [ options ] modules

rocqchk is the standalone checker of compiled libraries (.vo files produced by rocqcompile) for the Rocq Prover. 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.

-I dir, --include dir

Add directory dir to the include path.

-Q dir rocqdir

Map physical dir to logical rocqdir.

-R dir rocqdir

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 rocqchk version and exit.

-coqlib dir

Overrides the default location of the standard library.

-where

Print rocqchk standard library location and exit.

-h, --help

Print list of options.

rocq(1),

The Rocq Reference Manual.

The Rocq web site: http://coq.inria.fr