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

# coqnative(1)

native Coq compiler

## NAME

coqnative - native Coq compiler

## SYNOPSIS

**coqnative** \[ options \] *filename*

## DESCRIPTION

**coqnative** compiles vo files to binary files used by the native compute mechanism of 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.

*filename* is a Coq object file (a .vo) to compile to a native binary.

## OPTIONS

- **-Q** *dir coqdir*

  Map physical *dir* to logical *coqdir.*

- **-R** *dir coqdir*

  Synonymous to **-Q**.

- **-I** *dir*

  Ignored, for compatibility.

- **-noinit**

  Ignored, for compatibility.

- **-boot**

  Boot mode.

- **-coqlib** *dir*

  Override the default location of the standard library.

- **-nI** *dir*

  Add *dir* to the set of paths for the native files of the dependencies.

- **-native-output-dir** *dir*

  Output the generated files to *dir.*

- **-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 Rocq Prover Reference Manual.*

The Rocq Prover website: https://rocq-prover.org