11.5 Options
The following command-line options are recognized by the commands coqc and coqtop:
-
-byte
Run the byte-code version of Coq.
- -opt
Run the native-code version of Coq.
- -I directory, -include directory
Add directory to the searched directories when looking for a
file.
- -R directory dirpath
This maps the subdirectory structure of physical directory to
logical dirpath and adds directory and its subdirectories
to the searched directories when looking for a file.
- -is file, -inputstate file
Cause Coq to use the state put in the file file as its input
state. The default state is initial.coq.
Mainly useful to build the standard input state.
- -nois
Cause Coq to begin with an empty state. Mainly useful to build the
standard input state.
- -notactics
Forbid the dynamic loading of tactics.
- -init-file file
Take file as the resource file.
- -q
Cause Coq not to load the resource file.
- -user username
Take resource file of user username (that is
~
username/.coqrc.7.0) instead of yours.
- -load-ml-source file
Load the Caml source file file.
- -load-ml-object file
Load the Caml object file file.
- -load-vernac-source file
Load Coq file file.v
- -load-vernac-object file
Load Coq compiled file file.vo
- -require file
Load Coq compiled file file.vo and import it (Require file).
- -compile file
This compiles file file.v into file.vo.
This option implies options -batch and -silent. It is
only available for coqtop.
- -batch
Batch mode : exit just after arguments parsing. This option is only
used by coqc.
- -debug
Switch on the debug flag.
- -emacs
Tells Coq it is executed under Emacs.
- -db
Launch Coq under the Objective Caml debugger (provided that Coq
has been compiled for debugging; see next chapter).
- -image file
This option sets the binary image to be used to be file
instead of the standard one. Not of general use.
- -bindir directory
Set the directory containing Coq binaries.
It is equivalent to do export COQBIN=directory
before lauching Coq.
- -libdir file
Set the directory containing Coq libraries.
It is equivalent to do export COQLIB=directory
before lauching Coq.
- -where
Print the Coq's standard library location and exit.
- -v
Print the Coq's version and exit.
- -h, --help
Print a short usage and exit.