coqmktop(1) [debian man page]
COQ(1) General Commands Manual COQ(1) NAME
coqmktop - The Coq Proof Assistant user-tactics linker SYNOPSIS
coqmktop [ options ] files DESCRIPTION
coqmktop builds a new Coq toplevel extended with user-tactics. files are the Objective Caml object or library files (i.e. with suffix .cmo, .cmx, .cma or .cmxa) to link with the Coq system. The linker produces an executable Coq toplevel which can be called directly or through coqc(1), using the -image option. OPTIONS
-h Help. List the available options. -srcdir dir Specify where the Coq source files are -o exec-file Specify the name of the resulting toplevel -opt Compile in native code -full Link high level tactics -top Build Coq on a ocaml toplevel (incompatible with -opt) -searchisos Build a toplevel for SearchIsos -ide Build a toplevel for the Coq IDE -R dir Specify recursively directories for Ocaml -v8 Link with V8 grammar SEE ALSO
coqtop(1), ocamlmktop(1). ocamlc(1). ocamlopt(1). The Coq Reference Manual. The Coq web site: http://coq.inria.fr April 25, 2001 COQ(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)