sourCEntral - mobile manpages

pdf

COQIDE

NAME

coqide − The Coq Proof Assistant graphical interface

SYNOPSIS

coqide [ options ]

DESCRIPTION

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

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

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.

−is f, −inputstate f

Read state from f.coq.

−nois

Start with an empty state.

−outputstate f

Write state in file f.coq.

−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 f

Load Coq object file f.vo.

−require f

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

−compile f

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

−compile−verbose f

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−file f

Set the rcfile to f.

−user u

Use the rcfile of user u.

−batch

Batch mode (exits just after arguments parsing).

−boot

Boot mode (implies −q and −batch).

−emacs

Tells Coq it is executed under Emacs.

−dump−glob f

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

SEE ALSO

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.

AUTHOR

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

pdf