11.1 Interactive use (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 ran by the command coqtop. This toplevel is based on a Caml toplevel (to allow the dynamic link of tactics). You can switch to the Caml toplevel with the commandDrop., and come back to the
Coq toplevel with the command Coqtoplevel.go();;.They are three different binary images og Coq: the byte-code one, the native-code one and the full native-code one. When invoking
coqtop, the byte-code version of the system is used. The
command coqtop -opt runs a native-code version of the
Coq system, and the command coqtop -full a native-code version
with the implementation code of all the tactics (that is with the code
of the tactics Linear, Ring and Omega which then
can be required by Require) and tools (Extraction and
Natural which again become available through the command
Require). Those toplevels are significantly faster than the
byte-code one. Notice that it is no longer possible to access the
Caml toplevel, neither to load tactics.The command
coqtop -searchisos runs the search tool Coq_SearchIsos (see section 12.4,
page X) and, as the Coq system, can be combined with the
option -opt.