Linux and UNIX Man Pages

Linux & Unix Commands - Search Man Pages

coqide(1) [debian man page]

COQIDE(1)						      General Commands Manual							 COQIDE(1)

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.mimram@ens-lyon.org>, for the Debian project (but may be used by others). July 16, 2004 COQIDE(1)

Check Out this Related Man Page

COQ(1)							      General Commands Manual							    COQ(1)

NAME
coqtop - The Coq Proof Assistant toplevel system SYNOPSIS
coqtop [ options ] DESCRIPTION
coqtop is the toplevel system of Coq, for interactive use. It reads phrases on the standard input, and prints results on the standard out- put. For batch-oriented use of Coq, see coqc(1). OPTIONS
-h, --help Help. Will give you the complete list of options accepted by coqtop. -I dir, --include dir add directory dir in the include path -R dir coqdir recursively map physical dir to logical coqdir -top coqdir set the toplevel name to be coqdir instead of Top -inputstate filename, -is filename read state from file filename.coq -nois start with an empty initial state -outputstatefilename write state in file filename.coq -load-ml-object filename load ML object file filenname -load-ml-source filename load ML file filename -load-vernac-source filename, -l filename load Coq file filename.v (Load filename.) -load-vernac-source-verbose filename, -lv filename load verbosely Coq file filename.v (Load Verbose filename.) -load-vernac-object filename load Coq object file filename.vo -require filename load Coq object file filename.vo and import it (Require Import filename.) -compile filename compile Coq file filename.v (implies -batch ) -compile-verbose filename verbosely compile Coq file filename.v (implies -batch ) -opt run the native-code version of Coq -byte run the bytecode version of Coq -where print Coq's standard library location and exit -v print Coq version and exit -q skip loading of rcfile -init-file filename set the rcfile to filename -user uid use the rcfile of user uid -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 filename dump globalizations in file f (to be used by coqdoc(1) ) -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes ) -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) -quality improve the legibility of the proof terms produced by some tactics SEE ALSO
coqc(1), coq-tex(1), coqdep(1). The Coq Reference Manual. The Coq web site: http://coq.inria.fr October 11, 2006 COQ(1)
Man Page