rocqide1

Usage

Overview

rocqide is a gtk graphical interface for the Rocq Prover.

For command-line-oriented or batch-oriented use of Rocq, see rocq(1);

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)doc).

-impredicative-set

Set sort Set impredicative.

-dont-load-proofs

Don't load opaque proofs in memory.