1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
\chapter{\Coq{} Integrated Development Environment}
%\label{Addoc-coqide}
\ttindex{coqide}
The \Coq{} Integrated Development Environment is a graphical tool, to
be used as a user-friendly replacement to \texttt{coqtop}. Its main
purpose is to allow the user to navigate forward and backward into a
\Coq{} vernacular file, executing corresponding commands or undoing
them respectively. CREDITS ? Proof general, lablgtk, ...
\coqide{} is run by typing the command \verb|coqide| on the command
line. Without argument, the main screen is displayed with an ``unnamed
buffer'', and with a file name as argument, another buffer displaying
the contents of that file. Additionally, coqide accepts the same
options as coqtop, given in Chapter~\ref{Addoc-coqc}, the ones having
obviously no meaning for \coqide{} being ignored.
\begin{figure}[t]
\begin{center}
\ifx\pdfoutput\undefined % si on est pas en pdflatex
\includegraphics[width=1.0\textwidth]{coqide.eps}
\else
\includegraphics[width=1.0\textwidth]{coqide.png}
\fi
\end{center}
\caption{Coqide main screen}
\label{fig:coqide}
\end{figure}
A sample \coqide{} main screen, while navigating into a file
\verb|Fermat.v|, is shown on Figure~\ref{fig:coqide}. At
the top is a menu bar, and a tool bar below it. The large window on
the left is displaying the various \emph{script buffers}. The upper right
window is the \emph{goal window}, where goals to
prove are displayed. The lower right window is the \emph{message window},
where various messages resulting from commands are displayed. At the
bottom is the status bar.
\section{Managing files and buffers}
In the script window, you may open arbitrarily many buffers to
edit. The \emph{File} menu allows you to open files or create some,
save them, print or export them into various formats. Among all these
buffers, there is always one which is the current \emph{running
buffer}, whose name is displayed on a green background, which is the
one where Coq commands are currently executed.
\section{Interactive navigation into \Coq{} scripts}
The running buffer is the one where navigation takes place. The
toolbar proposes five basic commands for this. The first one,
represented by a down arrow icon, is for going forward executing one
command. If that command is successful, the part of the script that
has been executed is displayed on a green background. If that command
fails, the error message is displayed in the message window, and the
location of the error is emphasized by a red underline.
On Figure~\ref{fig:coqide}, the running buffer is \verb|Fermat.v|, all
commands until the \verb|Theorem| have been already executed, and the
user tried to go forward executing \verb|Induction n|. That command
failed because no such tactic exist (you remember that tactics in V8.0
are lowercase, right ?), and the wrong word is underlined.
Notice that the green part of the running buffer is not editable. If
you ever want to modify something you have to go backward using the up
arrow tool, or even better, put the cursor where you want to go back
and use the \textsf{goto} button. Unlike with \verb|coqtop|, you
should never use \verb|Undo| to go backward.
Two additional tool buttons exist, one to go directly to the end and
one to go back to the beginning. If you try to go to the end, or in
general to run several commands using the \textsf{goto} button, the
execution will stop whenever an error is found.
If you ever try to execute a long-running command, such as an
\verb|intuition eauto with *|, and would like to abort it before its
end, you may use the interrupt button, the red cross-like.
Finally, notice that these navigation buttons are also available in
the menu, where their keyboard shortcuts are given.
\section{Try tactics automatically}
The menu \texttt{Try Tactics} provides some features for automatically
trying to solve the current goal using simple tactics. If such a
tactics succeeds in solving the goal, then its text is automatically
inserted into the script. There is finally a combination of these
tactics, called the \emph{proof wizard} which will try each of them in
turn. This wizard is also available as a tool button, with a light
bulb shape. The set of tactics tried by the wizard is customizable in
the preferences.
\section{Vernacular commands, templates}
The \texttt{Templates} menu allows to use shortcuts to insert
vernacular commands. This is a nice menu to use if you are not sure of
the spelling of the command you want.
Moreover, this menu offers some \emph{templates} which will automatic
insert a complex command like Fixpoint with a convenient shape for its
arguments.
\section{Queries}
\section{Compilation}
\section{Preferences}
auto save, auto revert, delays
% $Id$
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End:
|
