---
name: "rocqchk"
section: "1"
platform: "linux"
package: "rocq"
version: "9.3.0-1"
release: "Arch Linux 2026-11-01"
platforms: ["linux"]
url: "https://new.carta.tech/rocqchk"
---

# rocqchk(1)

verify compiled Rocq libraries

## NAME

rocqchk - verify compiled Rocq libraries

## SYNOPSIS

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

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

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

## SEE ALSO

[**rocq**(1)](/rocq/1.md),

*The Rocq Reference Manual.*

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