COQ(1)

NAME
coqtop - The Coq toplevel system

SYNOPSIS
coqtop [ -batch ] [ -debug ] [ -emacs ] [ -full ] [ -image filename ] [ -include directory ] [ -init-file filename ] [ -is state ] [ -load-ml-object filename ] [ -load-ml-source filename ] [ -load-vernac-object filename ] [ -load-vernac-source filename ] [ -nois ] [ -notactics ] [ -opt ] [ -preload filename ] [ -q ] [ -require filename ] [ -searchisos ] [ -user name ] [ -where ] [ -v ] [ -I directory ] [ -bindir directory ] [ -libdir directory ]

DESCRIPTION
coqtop is the toplevel system of Coq, for interactive use. It reads phrases on the standard input, and prints results on the standard output. There are two versions of the Coq toplevel: a bytecode version and a native-code version. The default version is the bytecode one. It is built on a Caml toplevel. It is possible to switch to the Caml toplevel with the command Drop. and to come back to the Coq toplevel with the command Coqtoplevel.go();; This is useful for tactic debugging purposes. The native-code version is launched with the -opt option (or with the option -full to get a complete system with all tactics). Therefore, it does not allow nor to access a Caml toplevel neither to load Caml code (through the Declare ML Module command). But it runs significantly faster than the bytecode toplevel. For batch-oriented use of Coq, see coqc(1).

OPTIONS

-batch
    Batch mode. Options are parsed and executed, and the command coqtop immediately returns. Mainly used by coqc(1).

-debug
    Debugging mode (for developping purpose).

-emacs
    Tells Coq it is executed under Emacs.

-full
    Use the native-code version of Coq with all tactics.

-image filename
    Take filename as the Caml customized toplevel. The default value is coq.out.

-include directory, -I directory
    Adds directory to the path of directories searched for Coq files (.vo, .vi) and Caml files.

-bindir directory
    Forces coqtop to search the executable in the given directory. By default, coqtop searches it in the the directory given by the $COQBIN environment variable. If this variable is not defined, it searches it in the directory where coq.out was installed.

-libdir directory
    Forces coqtop to search the Coq standard library in the given directory. By default, coqtop searches it in the the directory given by the $COQLIB environment variable. If this variable is not defined, it searches it in the directory where the standard library of Coq was installed.

-init-file filename
    Takes filename as init file. If the init file is not specified with this option, the default value is $HOME/.coqrc.5.10, or $HOME/.coqrc if the first one does not exist.

-is state
    Takes state as initial state. Adds the suffix .coq if needed. The default state is tactics.coq.

-load-ml-object filename
    Load the Caml object file filename. Adds the .zo suffix if needed.

-load-ml-source filename
    Load the Caml source file filename. Adds the .ml suffix if needed.

-load-vernac-object filename
    Load the Coq compiled file filename. Adds the suffix .vo if needed.

-load-vernac-source filename
    Load the Coq vernacular file filename. Adds the suffix .v if needed.

-nois
    No input state. Mainly used to build a first state.

-notactics
    Do not load high level tactics, such as Program, Prolog, Tauto, etc. Start on the initial state state.coq instead of tactics.coq.

-opt
    Use the native-code version of Coq or Coq_SearchIsos.

-q  Do not load an init file.

-require filename
    Load the Coq compiled file filename.vo.

-searchisos
    Run Coq_SearchIsos.

-user name
    Load user name 's init file.

-where
    Print the location of the Coq standard library and exit.

-v  Print the Coq version and exit.

FILES
tactics.coq    the default initial state
coqc    the Coq batch compiler
$HOME/.coqrc    user's init file

SEE ALSO
coqc(1), coqdep(1).
The Coq Reference Manual.