ROCQCHK(1) General Commands Manual ROCQCHK(1)

# [NAME](#NAME)

rocqchk - verify compiled Rocq libraries

# [SYNOPSIS](#SYNOPSIS)

**rocqchk** \[ options ] *modules*

# [DESCRIPTION](#DESCRIPTION)

**rocqchk** is the standalone checker of compiled libraries (.vo files produced by **rocq**compile**)** 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.

# [OPTIONS](#OPTIONS)

[**-I dir, --include dir**](#I)

Add directory *dir* to the include path.

[**-Q dir rocqdir**](#Q)

Map physical *dir* to logical *rocqdir.*

[**-R dir rocqdir**](#R)

Synonymous to **-Q**.

[**-silent**](#silent)

Be less verbose.

[**-admit module**](#admit)

Tag the specified module and all its dependencies as trusted, and will not be rechecked, unless explicitly requested by other options.

[**-norec module**](#norec)

Specifies that the given module shall be verified without requesting to check its dependencies.

[**-m**, **--memory**](#m)

Displays a summary of the memory used by the checker.

[**-o**, **--output-context**](#o)

Displays a summary of the logical content that have been verified: assumptions and usage of impredicativity.

[**-impredicative-set**](#impredicative)

Allows the checker to accept libraries that have been compiled with this flag.

[**-v**](#v)

Print **rocqchk** version and exit.

[**-coqlib dir**](#coqlib)

Overrides the default location of the standard library.

[**-where**](#where)

Print rocqchk standard library location and exit.

[**-h**, **--help**](#h)

Print list of options.

# [SEE ALSO](#SEE_ALSO)

[**rocq**(1)](/man/os/rocq/rocq.1),

*The Rocq Reference Manual.*

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

---

Document: rocqchk(1) from rocq 9.2.0-r0 (Chainguard OS)