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

# coqide(1)

graphical interface for the Coq proof assistant

## NAME

coqide - graphical interface for the Coq proof assistant

## SYNOPSIS

**coqide** \[ options \]

## DESCRIPTION

**coqide** is a gtk graphical interface for the Coq proof assistant.

For command-line-oriented use of Coq, see [**coqtop**(1)](/coqtop/1.md); for batch-oriented use of Coq, see [**coqc**(1)](/coqc/1.md).

## OPTIONS

- **-h**

  Show the complete list of options accepted by **coqide**.

- **-I** *dir,* **-include** *dir*

  Add directory *dir* in the include path.

- **-R** *dir coqdir*

  Recursively map physical *dir* to logical *coqdir.*

- **-src**

  Add source directories in the include path.

- **-nois**

  Start with an empty state.

- **-load-ml-object** *f*

  Load ML object file *f.*

- **-load-ml-source** *f*

  Load ML file *f.*

- **-l** *f,* **-load-vernac-source** *f*

  Load Coq file *f*.v (Load *f.*).

- **-lv** *f,* **-load-vernac-source-verbose** *f*

  Load Coq file *f*.v (Load Verbose *f.*).

- **-load-vernac-object** *path*

  Load Coq library *path* (Require *path.*).

- **-require-import** *path*

  Load Coq library *path* and import it (Require Import *path.*).

- **-compile** *f*

  Compile Coq file *f*.v (implies **-batch**).

- **-compile-verbose** *f*

  Verbosely compile Coq file *f*.v (implies **-batch**).

- **-where**

  Print Coq's standard library location and exit.

- **-v**

  Print Coq version and exit.

- **-q**

  Skip loading of rcfile.

- **-init-file** *f*

  Set the rcfile to *f.*

- **-emacs**

  Tells Coq it is executed under Emacs.

- **-dump-glob** *f*

  Dump globalizations in file *f* (to be used by [**coqdoc**(1)](/coqdoc/1.md)).

- **-impredicative-set**

  Set sort Set impredicative.

- **-dont-load-proofs**

  Don't load opaque proofs in memory.

## SEE ALSO

[**coqc**(1)](/coqc/1.md), [**coqtop**(1)](/coqtop/1.md), [**coq-tex**(1)](/coq-tex/1.md), [**coqdep**(1)](/coqdep/1.md)

*The Coq Reference Manual*

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

/usr/share/doc/coqide/FAQ

## AUTHOR

This manual page was written by Samuel Mimram \<samuel.mimram@ens-lyon.org\>, for the Debian project (but may be used by others).