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

# coqc.byte(1)

Coq compiler

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

## 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 Coq Reference Manual.*

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