\chapter{The \Coq~commands}\label{Addoc-coqc}
\ttindex{coqtop}
\ttindex{coqc}

There are two \Coq~commands: 

\bigskip
\begin{tabular}{l@{\quad:\quad}l}
  -- {\tt coqtop} & The \Coq\ toplevel (interactive mode) ; \\[1em]
  -- {\tt coqc}   & The \Coq\ compiler (batch compilation).
\end{tabular}
\bigskip

The options are (basically) the same for the two commands, and
roughly described below. You can also look at the \verb!man! pages of
\verb!coqtop! and \verb!coqc! for more details.


\section{Interactive use ({\tt coqtop})}
In the interactive mode, also known as the \Coq~toplevel, the user can
develop his theories and proofs step by step.  The \Coq~toplevel is
run by the command {\tt coqtop}. 

\index{byte-code}
\index{native code}
\label{binary-images}
They are two different binary images of \Coq: the byte-code one and
the native-code one (if Objective Caml provides a native-code compiler
for your platform, which is supposed in the following).  When invoking
\verb!coqtop! or \verb!coqc!, the native-code version of the system is
used.  The command-line options \verb!-byte! and \verb!-opt! explicitly
select the byte-code and the native-code versions, respectively.

The byte-code toplevel is based on a Caml
toplevel (to allow the dynamic link of tactics).  You can switch to
the Caml toplevel with the command \verb!Drop.!, and come back to the
\Coq~toplevel with the command \verb!Toplevel.loop();;!.

% The command \verb!coqtop -searchisos! runs the search tool {\sf
%   Coq\_SearchIsos} (see section~\ref{coqsearchisos},
% page~\pageref{coqsearchisos}) and, as the \Coq~system, can be combined
% with the option \verb!-opt!.

\section{Batch compilation ({\tt coqc})}
The {\tt coqc} command takes a name {\em file} as argument.  Then it
looks for a vernacular file named {\em file}{\tt .v}, and tries to
compile it into a {\em file}{\tt .vo} file (See ~\ref{compiled}).

\Warning The name {\em file} must be a regular {\Coq} identifier, as
defined in the section \ref{lexical}. It
must only contain letters, digits or underscores
(\_). Thus it can be \verb+/bar/foo/toto.v+ but cannot be
\verb+/bar/foo/to-to.v+ . 

Notice that the \verb!-byte! and \verb!-opt! options are still
available with \verb!coqc!  and allow you to select the byte-code or
native-code versions of the system.


\section{Resource file}
\index{Resource file}

When \Coq\ is launched, with either {\tt coqtop} or {\tt coqc}, the
resource file \verb:$HOME/.coqrc.7.0: is loaded, where \verb:$HOME: is
the home directory of the user.  If this file is not found, then the
file \verb:$HOME/.coqrc: is searched. You can also specify an
arbitrary name for the resource file (see option \verb:-init-file:
below), or the name of another user to load the resource file of
someone else (see option \verb:-user:).

This file may contain, for instance, \verb:Add LoadPath: commands to add
directories to the load path of \Coq.
It is possible to skip the loading of the resource file with the
option \verb:-q:.

\section{Environment variables}
\label{EnvVariables}
\index{Environment variables}

There are three environment variables used by the \Coq\ system.
\verb:$COQBIN: for the directory where the binaries are,
\verb:$COQLIB: for the directory whrer the standard library is, and 
\verb:$COQTOP: for the directory of the sources. The latter is useful
only for developers that are writing their own tactics and are using
\texttt{coq\_makefile} (see \ref{Makefile}). If \verb:$COQBIN: or
\verb:$COQLIB: are not defined, \Coq\ will use the default values
(defined at installation time). So these variables are useful only if
you move the \Coq\ binaries and library after installation.

\section{Options}
\index{Options of the command line}

The following command-line options are recognized by the commands {\tt
  coqc} and {\tt coqtop}:

\begin{description}
\item[{\tt -byte}]\ \\
  Run the byte-code version of \Coq{}.

\item[{\tt -opt}]\ \\
  Run the native-code version of \Coq{}.

\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\ \\
  Add {\em directory} to the searched directories when looking for a
  file.

\item[{\tt -R} {\em directory} {\dirpath}]\ \\
  This maps the subdirectory structure of physical {\em directory} to
  logical {\dirpath} and adds {\em directory} and its subdirectories
  to the searched directories when looking for a file.

\item[{\tt -is} {\em file}, {\tt -inputstate} {\em file}]\ \\
  Cause \Coq~to use the state put in the file {\em file} as its input
  state. The default state is {\em initial.coq}.
  Mainly useful to build the standard input state.

\item[{\tt -nois}]\ \\
  Cause \Coq~to begin with an empty state. Mainly useful to build the
  standard input state.

\item[{\tt -notactics}]\ \\
  Forbid the dynamic loading of tactics.

\item[{\tt -init-file} {\em file}]\ \\
  Take {\em file} as the resource file.

\item[{\tt -q}]\ \\
  Cause \Coq~not to load the resource file.

\item[{\tt -user} {\em username}]\ \\
  Take resource file of user {\em username} (that is 
  \verb+~+{\em username}{\tt /.coqrc.7.0}) instead of yours.

\item[{\tt -load-ml-source} {\em file}]\ \\
  Load the Caml source file {\em file}.

\item[{\tt -load-ml-object} {\em file}]\ \\
  Load the Caml object file {\em file}.

\item[{\tt -load-vernac-source} {\em file}]\ \\
  Load \Coq~file {\em file}{\tt .v}

\item[{\tt -load-vernac-object} {\em file}]\ \\
  Load \Coq~compiled file {\em file}{\tt .vo}

%\item[{\tt -preload} {\em file}]\ \\
%Add {\em file}{\tt .vo} to the files to be loaded and opened
%before making the initial state.
%
\item[{\tt -require} {\em file}]\ \\
  Load \Coq~compiled file {\em file}{\tt .vo} and import it ({\tt
    Require} {\em file}).

\item[{\tt -compile} {\em file}]\ \\
  This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo}.
  This option implies options {\tt -batch} and {\tt -silent}. It is
  only available for {\tt coqtop}.

%\item[{\tt -compile-verbose} {\em file}]\ \\
%  This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo} with
%  a copy of the contents of the file on standard input.
%  This option implies options {\tt -batch} and {\tt -silent}. It is
%  only available for {\tt coqtop}.

\item[{\tt -batch}]\ \\
  Batch mode : exit just after arguments parsing. This option is only
  used by {\tt coqc}.

\item[{\tt -debug}]\ \\
  Switch on the debug flag.

\item[{\tt -emacs}]\ \\
  Tells \Coq\ it is executed under Emacs.

\item[{\tt -db}]\ \\
  Launch \Coq\ under the Objective Caml debugger (provided that \Coq\
  has been compiled for debugging; see next chapter).

\item[{\tt -impredicative-set}]\ \\
  Change the logical theory of {\Coq} by declaring the sort {\tt Set}
  impredicative; warning: this is known to be inconsistent with
  some standard axioms of classical mathematics such as the functional
  axiom of choice or the principle of description\\

\item[{\tt -dont-load-proofs}]\ \\
  This avoids loading in memory the proofs of opaque theorems
  resulting in a smaller memory requirement and faster compilation;
  warning: this invalidates some features such as the extraction tool.

\item[{\tt -image} {\em file}]\ \\
  This option sets the binary image to be used to be {\em file}
  instead of the standard one. Not of general use.

\item[{\tt -bindir} {\em directory}]\ \\
  Set the directory containing \Coq\ binaries.
  It is equivalent to do \texttt{export COQBIN=}{\em directory}
  before lauching \Coq.

\item[{\tt -libdir} {\em file}]\ \\
  Set the directory containing \Coq\ libraries.
  It is equivalent to do \texttt{export COQLIB=}{\em directory}
  before lauching \Coq.

\item[{\tt -where}]\ \\
  Print the \Coq's standard library location and exit.

\item[{\tt -v}]\ \\
  Print the \Coq's version and exit.

\item[{\tt -h}, {\tt --help}]\ \\
  Print a short usage and exit.
\end{description}

% {\tt coqtop} owns an additional option:

% \begin{description}
% \item[{\tt -searchisos}]\ \\
%   Launch the {\sf Coq\_SearchIsos} toplevel
%   (see section~\ref{coqsearchisos}, page~\pageref{coqsearchisos}).
% \end{description}

% $Id$ 

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End: