coqide (1)

coqide [ options ]

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

For command-line-oriented use of Coq, see coqtop(1) ; for batch-oriented use of Coq, see coqc(1).

-h

Show the complete list of options accepted by coqide.

-Idir,-includedir

Add directory dir in the include path.

-Rdircoqdir

Recursively map physical dir to logical coqdir.

-src

Add source directories in the include path.

-isf,-inputstatef

Read state from f.coq.

-nois

Start with an empty state.

-outputstatef

Write state in file f.coq.

-load-ml-objectf

Load ML object file f.

-load-ml-sourcef

Load ML file f.

-lf,-load-vernac-sourcef

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

-lvf,-load-vernac-source-verbosef

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

-load-vernac-objectf

Load Coq object file f.vo.

-requiref

Load Coq object file f.vo and import it (Require f.).

-compilef

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

-compile-verbosef

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

-opt

Run the native-code version of Coq or Coq_SearchIsos.

-byte

Run the bytecode version of Coq or Coq_SearchIsos.

-where

Print Coq's standard library location and exit.

-v

Print Coq version and exit.

-q

Skip loading of rcfile.

-init-filef

Set the rcfile to f.

-batch

Batch mode (exits just after arguments parsing).

-boot

Boot mode (implies -q and -batch).

-emacs

Tells Coq it is executed under Emacs.

-dump-globf

Dump globalizations in file f (to be used by coqdoc(1)).

-impredicative-set

Set sort Set impredicative.

-dont-load-proofs

Don't load opaque proofs in memory.

-xml

Export XML files either to the hierarchy rooted in the directory COQ_XML_LIBRARY_ROOT (if set) or to stdout (if unset).

coqc(1), coqtop(1), coq-tex(1), coqdep(1).

The Coq Reference Manual, The Coq web site: http://coq.inria.fr, /usr/share/doc/coqide/FAQ.

This manual page was written by Samuel Mimram <[email protected]>, for the Debian project (but may be used by others).