coqide − The Coq Proof Assistant graphical interface
coqide [ options ]
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).
−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). |
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 <samuel DOT mimram AT ens-lyon DOT org>, for the Debian project (but may be used by others).