rocqide - Man Page

graphical interface for the Rocq Prover

Synopsis

rocqide [ options ]

rocqide is a gtk graphical interface for the Rocq Prover.

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

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

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