When you start CtCoq two windows appear on the screen. Each of these
window is equipped with a "File" pulldown menu where you can also find an option
to terminate the system. The two windows have the following aspect:
- A "Centaur messages" window, with the following aspect:
This window will display all the error messages, whether they come
from a misuse of CtCoq or from a misuse of Coq. However, it may
happen that the Coq messages are incomplete, due to errors in the
communication protocol between the two processes. To work around this
problem, see the page on extra tools.
The File menu of this messages window is quite important. It
contains options that will come handy when you want to change
resources in the middle of a session.
- A main CtCoq window
with the following aspect:
The grey lines between each area can be used to change the respective side of each window. These windows are not equipped with
horizontal scrollbars, but you can make them scroll by clicking with the left button inside the window and dragging the mouse
outside the window. As soon as the mouse crosses the border, this provokes a scrolling of the window content.
contains a lot of active areas that are described in other
- The menu
bar. This window provides a variety of pull down menus to act on the data
in the Commands window.
Commands window. This window will contain the sequence of all the commands
you send to the proof engine.
- The Tool bar This window provides a handfull
of tools for quick interaction
with the proof engine.
- The State window.
This window contains the current set of goals when you perform goal
direct proofs. It is also used for proof-by-pointing
and drag and drop rewrite.
- The Theorems
This window contains the results of Check and Search queries. It is also used for proof-by-pointing.
- Auxiliary CtCoq windows can be obtained when selecting the "New Proof Window"
option in the File menu of the main CtCoq window. Auxiliary CtCoq windows
have basically the same look as the main window, but they have a few extra
features: they are equipped with a kill box, a small square displayed at the
extreme left of the menu bar, this kill box makes it possible to remove these
windows from the screen without terminating the system. They also provide
more options in the File menu, that make it possible to move data from one
CtCoq window to another will respecting the coherence of the script. To
know more about this, please refer to the page on
script management. Auxiliary CtCoq windows have been introduced to make
it easier to prove extra lemmas on the side when attempting a large proof.
- Proof text windows can be obtained when you
request to display the text of a proof.
These windows are organized to make it easy to browse through proofs containing
several theorems, with a cache to ensure quick interaction. All this behavior
is described in the page on textual explanation.
- Library windows are created when you want to keep the contents of the
Theorems window on the side, in a more permanent place than the Theorems window.
They can be used to organize little menus of commonly used theorems, as described
in another page. This is especially useful as
these windows can also be used for proof by pointing.
- Goal windows make it possible to visualize a single goal in a separate window.
These windows are created when you go back in history and
request to see the
goal on which a past command worked. It should also be used to see
the current goals one by one, but this is not done in the current version.