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

# rocqide(1)

graphical interface for the Rocq Prover

## NAME

rocqide - graphical interface for the Rocq Prover

## SYNOPSIS

**rocqide** \[ options \]

## DESCRIPTION

**rocqide** is a gtk graphical interface for the Rocq Prover.

For command-line-oriented or batch-oriented use of Rocq, see [**rocq**(1)](/rocq/1.md);

## OPTIONS

- **-h**

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

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

  Add directory *dir* in the include path.

- **-R** *dir rocqdir*

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

- **-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 Rocq file *f*.v (Load *f.*).

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

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

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

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

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

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

- **-compile** *f*

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

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

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

- **-where**

  Print Rocq's standard library location and exit.

- **-v**

  Print Rocq version and exit.

- **-q**

  Skip loading of rcfile.

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

  Set the rcfile to *f.*

- **-emacs**

  Tells Rocq it is executed under Emacs.

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

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

- **-impredicative-set**

  Set sort Set impredicative.

- **-dont-load-proofs**

  Don't load opaque proofs in memory.

## SEE ALSO

[**rocq**(1)](/rocq/1.md),

*The Rocq Reference Manual*

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

/usr/share/doc/rocqide/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).