coqtop(1) [debian 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)
Check Out this Related Man Page
COQ(1) General Commands Manual COQ(1) NAME
coqdep - Compute inter-module dependencies for Coq and Caml programs SYNOPSIS
coqdep [ -w ] [ -I directory ] [ -coqlib directory ] [ -c ] [ -i ] [ -D ] [ -slash ] filename ... directory ... DESCRIPTION
coqdep compute inter-module dependencies for Coq and Caml programs, and prints the dependencies on the standard output in a format readable by make. When a directory is given as argument, it is recursively looked at. Dependencies of Coq modules are computed by looking at Require commands (Require, Require Export, Require Import), Declare ML Module com- mands and Load commands. Dependencies relative to modules from the Coq library are not printed. Dependencies of Caml modules are computed by looking at open directives and the dot notation module.value. OPTIONS
-c Prints the dependencies of Caml modules. (On Caml modules, the behaviour is exactly the same as ocamldep). -w Prints a warning if a Coq command Declare ML Module is incorrect. (For instance, you wrote `Declare ML Module "A".', but the module A contains #open "B"). The correct command is printed (see option -D). The warning is printed on standard error. -D This commands looks for every command Declare ML Module of each Coq file given as argument and complete (if needed) the list of Caml modules. The new command is printed on the standard output. No dependency is computed with this option. -slash Prints paths using a slash instead of the OS specific separator. This option is useful when developping under Cygwin. -I directory The files .v .ml .mli of the directory directory are taken into account during the calculus of dependencies, but their own dependen- cies are not printed. -coqlib directory Indicates where is the Coq library. The default value has been determined at installation time, and therefore this option should not be used under normal circumstances. SEE ALSO
ocamlc(1), coqc(1), make(1). NOTES
Lexers (for Coq and Caml) correctly handle nested comments and strings. The treatment of symbolic links is primitive. If two files have the same name, in two different directories, a warning is printed on standard error. There is no way to limit the scope of the recursive search for directories. EXAMPLES
Consider the files (in the same directory): A.ml B.ml C.ml D.ml X.v Y.v and Z.v where + D.ml contains the commands `open A', `open B' and `type t = C.t' ; + Y.v contains the command `Require X' ; + Z.v contains the commands `Require X' and `Declare ML Module "D"'. To get the dependencies of the Coq files: example% coqdep -I . *.v Z.vo: Z.v ./X.vo ./D.cmo Y.vo: Y.v ./X.vo X.vo: X.v With a warning: example% coqdep -w -I . *.v Z.vo: Z.v ./X.vo ./D.cmo Y.vo: Y.v ./X.vo X.vo: X.v ### Warning : In file Z.v, the ML modules declaration should be ### Declare ML Module "A" "B" "C" "D". To get only the Caml dependencies: example% coqdep -c -I . *.ml D.cmo: D.ml ./A.cmo ./B.cmo ./C.cmo D.cmx: D.ml ./A.cmx ./B.cmx ./C.cmx C.cmo: C.ml C.cmx: C.ml B.cmo: B.ml B.cmx: B.ml A.cmo: A.ml A.cmx: A.ml BUGS
Please report any bug to coq-bugs@pauillac.inria.fr Coq tools 28 March 1995 COQ(1)