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

# coqc(1)

Coq compiler

## NAME

coqc - Coq compiler

## SYNOPSIS

**coqc** \[ general Coq options \] *file*

## DESCRIPTION

**coqc** is the batch compiler for the Coq Proof Assistant. The options are basically the same as [**coqtop**(1)](/coqtop/1.md). *file.v* is the vernacular file to compile. *file* must be formed only with the characters \`a' to \`Z', \`0' to \`9' or \`\_' and must begin with a letter. The compiler produces an object file *file.vo*.

For interactive use of Coq, see [**coqtop**(1)](/coqtop/1.md).

## OPTIONS

**coqc** is a script that simply runs **coqtop** with option **-compile**. It accepts the same options as **coqtop**.

- **-image** *bin*

  Use *bin* as underlying **coqtop** instead of the default one.

- **-verbose**

  Print the compiled file on the standard output.

## SEE ALSO

[**coqtop**(1)](/coqtop/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