---
name: "coqchk.opt"
section: "1"
platform: "linux"
package: "coq"
version: "8.20.1+dfsg-1+b1"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/coqchk"
---

# coqchk.opt(1)

verify compiled Coq libraries

Part of [coqchk(1)](/coqchk/1.md).

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

## SEE ALSO

[**coqtop**(1)](/coqtop/1.md), [**coqc**(1)](/coqc/1.md), [**coq\_makefile**(1)](/coq_makefile/1.md), [**coqdep**(1)](/coqdep/1.md)

*The Coq Reference Manual.*

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