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

coqdoc(1)						      General Commands Manual							 coqdoc(1)

NAME
coqdoc - A documentation tool for the Coq proof assistant SYNOPSIS
coqdoc [ options ] files DESCRIPTION
coqdoc is a documentation tool for the Coq proof assistant. It creates LaTeX or HTML documents from a set of Coq files. See the Coq ref- erence manual for documentation (url below). OPTIONS
Overall options -h Help. Will give you the complete list of options accepted by coqdoc. --html Select a HTML output. --latex Select a LATEX output. --dvi Select a DVI output. --ps Select a PostScript output. --texmacs Select a TeXmacs output. --stdout Redirect the output to stdout -o file,--output file Redirect the output into the file file. -d dir, --directory dir Output files into directory dir instead of current directory (option -d does not change the filename specified with option -o, if any). -s, --short Do not insert titles for the files. The default behavior is to insert a title like ``Library Foo'' for each file. -t string, --title string Set the document title. --body-only Suppress the header and trailer of the final document. Thus, you can insert the resulting document into a larger one. -p string, --preamble string Insert some material in the LATEX preamble, right before egin{document} (meaningless with -html). --vernac-file file, --tex-file file Considers the file `file' respectively as a .v (or .g) file or a .tex file. --files-from file Read file names to process in file `file' as if they were given on the command line. Useful for program sources split in several directories. -q, --quiet Be quiet. Do not print anything except errors. -h, --help Give a short summary of the options and exit. -v, --version Print the version and exit. Index options Default behavior is to build an index, for the HTML output only, into index.html. --no-index Do not output the index. --multi-index Generate one page for each category and each letter in the index, together with a top page index.html. Table of contents option -toc, --table-of-contents Insert a table of contents. For a LATEX output, it inserts a ableofcontents at the beginning of the document. For a HTML output, it builds a table of contents into toc.html. Hyperlinks options --glob-from file Make references using Coq globalizations from file file. (Such globalizations are obtained with Coq option -dump-glob). --no-externals Do not insert links to the Coq standard library. --external url libroot Set base URL for the external library whose root prefix is libroot. --coqlib url Set base URL for the Coq standard library (default is http://coq.inria.fr/library/). --coqlib_path dir Set the base path where the Coq files are installed, especially style files coqdoc.sty and coqdoc.css. -R dir coqdir Map physical directory dir to Coq logical directory coqdir (similarly to Coq option -R). Note: option -R only has effect on the files following it on the command line, so you will probably need to put this option first. Contents options -g, --gallina Do not print proofs. -l, --light Light mode. Suppress proofs (as with -g) and the following commands: * [Recursive] Tactic Definition * Hint / Hints * Require * Transparent / Opaque * Implicit Argument / Implicits * Section / Variable / Hypothesis / End The behavior of options -g and -l can be locally overridden using the (* begin show *) ... (* end show *) environment (see above). Language options Default behavior is to assume ASCII 7 bits input files. -latin1, --latin1 Select ISO-8859-1 input files. It is equivalent to --inputenc latin1 --charset iso-8859-1. -utf8, --utf8 Select UTF-8 (Unicode) input files. It is equivalent to --inputenc utf8 --charset utf-8. LATEX UTF-8 support can be found at http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/. --inputenc string Give a LATEX input encoding, as an option to LATEX package inputenc. --charset string Specify the HTML character set, to be inserted in the HTML header. SEE ALSO
The Coq Reference Manual from http://coq.inria.fr/ April, 2006 coqdoc(1)
Man Page

Featured Tech Videos