From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 14 Oct 2010 17:51:11 +0200
Subject: Imported Upstream version 8.3

---
 doc/refman/RefMan-ide.tex | 322 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 322 insertions(+)
 create mode 100644 doc/refman/RefMan-ide.tex

(limited to 'doc/refman/RefMan-ide.tex')

diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
new file mode 100644
index 00000000..04830531
--- /dev/null
+++ b/doc/refman/RefMan-ide.tex
@@ -0,0 +1,322 @@
+\chapter[\Coq{} Integrated Development Environment]{\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, \verb|coqide| accepts the same
+options as \verb|coqtop|, given in Chapter~\ref{Addoc-coqc}, the ones having
+obviously no meaning for \CoqIDE{} being ignored. Additionally, \verb|coqide| accepts the option \verb|-enable-geoproof| to enable the support for \emph{GeoProof} \footnote{\emph{GeoProof} is dynamic geometry software which can be used in conjunction with \CoqIDE{} to interactively build a Coq statement corresponding to a geometric figure. More information about \emph{GeoProof} can be found here: \url{http://home.gna.org/geoproof/} }. 
+  
+
+\begin{figure}[t]
+\begin{center}
+%HEVEA\imgsrc{coqide.png}
+%BEGIN LATEX
+\ifpdf   % si on est en pdflatex
+\includegraphics[width=1.0\textwidth]{coqide.png}
+\else
+\includegraphics[width=1.0\textwidth]{coqide.eps}
+\fi
+%END LATEX
+\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, basic edition}
+
+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. 
+
+Buffers may be edited as in any text editor, and classical basic
+editing commands (Copy/Paste, \ldots) are available in the \emph{Edit}
+menu. \CoqIDE{} offers only basic editing commands, so if you need
+more complex editing commands, you may launch your favorite text
+editor on the current buffer, using the \emph{Edit/External Editor}
+menu. 
+
+\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 (tactics are now in
+lowercase\ldots), 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 command which happens to run during a
+long time, and would like to abort it before its
+termination, you may use the interrupt button (the white cross on a red circle).
+ 
+Finally, notice that these navigation buttons are also available in
+the menu, where their keyboard shortcuts are given.
+
+\section[Try tactics automatically]{Try tactics automatically\label{sec:trytactics}}
+
+The menu \texttt{Try Tactics} provides some features for automatically
+trying to solve the current goal using simple tactics. If such a
+tactic 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 (the light
+bulb).  The set of tactics tried by the wizard is customizable in
+the preferences.
+
+These tactics are general ones, in particular they do not refer to
+particular hypotheses. You may also try specific tactics related to
+the goal or one of the hypotheses, by clicking with the right mouse
+button on the goal or the considered hypothesis. This is the
+``contextual menu on goals'' feature, that may be disabled in the
+preferences if undesirable.
+
+\section{Proof folding}
+
+As your script grows bigger and bigger, it might be useful to hide the proofs
+of your theorems and lemmas.
+
+This feature is toggled via the \texttt{Hide} entry of the \texttt{Navigation}
+menu. The proof shall be enclosed between \texttt{Proof.} and \texttt{Qed.},
+both with their final dots. The proof that shall be hidden or revealed is the
+first one whose beginning statement (such as \texttt{Theorem}) precedes the
+insertion cursor.
+ 
+\section{Vernacular commands, templates}
+
+The \texttt{Templates} menu allows to use shortcuts to insert
+vernacular commands. This is a nice way to proceed 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}
+
+\begin{figure}[t]
+\begin{center}
+%HEVEA\imgsrc{coqide-queries.png}
+%BEGIN LATEX
+\ifpdf  % si on est en pdflatex
+\includegraphics[width=1.0\textwidth]{coqide-queries.png}
+\else
+\includegraphics[width=1.0\textwidth]{coqide-queries.eps}
+\fi
+%END LATEX
+\end{center}
+\caption{\CoqIDE{}: the query window}
+\label{fig:querywindow}
+\end{figure}
+
+
+We call \emph{query} any vernacular command that do not change the
+current state, such as \verb|Check|, \verb|SearchAbout|, etc. Those
+commands are of course useless during compilation of a file, hence
+should not be included in scripts. To run such commands without
+writing them in the script, \CoqIDE{} offers another input window
+called the \emph{query window}. This window can be displayed on
+demand, either by using the \texttt{Window} menu, or directly using
+shortcuts given in the \texttt{Queries} menu. Indeed, with \CoqIDE{}
+the simplest way to perform a \texttt{SearchAbout} on some identifier
+is to select it using the mouse, and pressing \verb|F2|. This will
+both make appear the query window and run the \texttt{SearchAbout} in
+it, displaying the result. Shortcuts \verb|F3| and \verb|F4| are for
+\verb|Check| and \verb|Print| respectively.
+Figure~\ref{fig:querywindow} displays the query window after selection
+of the word ``mult'' in the script windows, and pressing \verb|F4| to
+print its definition.
+
+\section{Compilation}
+
+The \verb|Compile| menu offers direct commands to:
+\begin{itemize}
+\item compile the current buffer
+\item run a compilation using \verb|make|
+\item go to the last compilation error
+\item create a \verb|makefile| using \verb|coq_makefile|.
+\end{itemize}
+
+\section{Customizations}
+
+You may customize your environment using menu
+\texttt{Edit/Preferences}. A new window will be displayed, with
+several customization sections presented as a notebook. 
+
+The first section is for selecting the text font used for scripts, goal
+and message windows. 
+
+The second section is devoted to file management: you may
+configure automatic saving of files, by periodically saving the
+contents into files named \verb|#f#| for each opened file
+\verb|f|. You may also activate the \emph{revert} feature: in case a
+opened file is modified on the disk by a third party, \CoqIDE{} may read
+it again for you. Note that in the case you edited that same file, you
+will be prompt to choose to either discard your changes or not. The
+\texttt{File charset encoding} choice is described below in
+Section~\ref{sec:coqidecharencoding}
+ 
+
+The \verb|Externals| section allows to customize the external commands
+for compilation, printing, web browsing. In the browser command, you
+may use \verb|%s| to denote the URL to open, for example: %
+\verb|mozilla -remote "OpenURL(%s)"|. 
+
+The \verb|Tactics Wizard| section allows to defined the set of tactics
+that should be tried, in sequence, to solve the current goal.
+
+The last section is for miscellaneous boolean settings, such as the
+``contextual menu on goals'' feature presented in
+Section~\ref{sec:trytactics}. 
+
+Notice that these settings are saved in the file \verb|.coqiderc| of
+your home directory. 
+
+A gtk2 accelerator keymap is saved under the name \verb|.coqide.keys|.
+This file should not be edited manually: to modify a given menu
+shortcut, go to the corresponding menu item without releasing the
+mouse button, press the key you want for the new shortcut, and release
+the mouse button afterwards.
+
+For experts: it is also possible to set up a specific gtk resource
+file, under the name \verb|.coqide-gtk2rc|, following the gtk2
+resources syntax
+\url{http://developer.gnome.org/doc/API/2.0/gtk/gtk-Resource-Files.html}.
+Such a default resource file can be found in the subdirectory
+\verb=lib/coq/ide= of the root installation directory of \Coq{}
+(alternatively, it can be found in the subdirectory \verb=ide= of the
+source archive of \Coq{}). You may
+copy this file into your home directory, and edit it using any text
+editor, \CoqIDE{} itself for example.
+
+\section{Using unicode symbols}
+
+\CoqIDE{} supports unicode character encoding in its text windows,
+consequently a large set of symbols is available for notations.
+
+\subsection{Displaying unicode symbols}
+
+You just need to define suitable notations as described in
+Chapter~\ref{Addoc-syntax}. For example, to use the mathematical symbols
+$\forall$ and $\exists$, you may define 
+\begin{quote}\tt
+Notation "$\forall$ x : t, P" := \\
+\qquad  (forall x:t, P) (at level 200, x ident).\\
+Notation "$\exists$ x : t, P" := \\
+\qquad  (exists x:t, P) (at level 200, x ident).
+\end{quote}
+There exists a small set of such notations already defined, in the
+file \verb|utf8.v| of \Coq{} library, so you may enable them just by 
+\verb|Require utf8| inside \CoqIDE{}, or equivalently, by starting
+\CoqIDE{} with \verb|coqide -l utf8|.
+
+However, there are some issues when using such unicode symbols: you of
+course need to use a character font which supports them. In the Fonts
+section of the preferences, the Preview line displays some unicode symbols, so
+you could figure out if the selected font is OK. Related to this, one
+thing you may need to do is choose whether Gtk should use antialiased
+fonts or not, by setting the environment variable \verb|GDK_USE_XFT|
+to 1 or 0 respectively.
+
+\subsection{Defining an input method for non ASCII symbols}
+
+To input an Unicode symbol, a general method is to press both the
+CONTROL and the SHIFT keys, and type the hexadecimal code of the
+symbol required, for example \verb|2200| for the $\forall$ symbol.
+A list of symbol codes is available at \url{http://www.unicode.org}. 
+
+This method obviously doesn't scale, that's why the preferred alternative is to
+use an Input Method Editor. On POSIX systems (Linux distros, BSD variants and
+MacOS X), you can use \texttt{uim} version 1.6 or later which provides a \LaTeX{}-style
+input method.
+
+To configure \texttt{uim}, execute \texttt{uim-pref-gtk} as your regular user.
+In the "Global Settings" group set the default Input Method to "ELatin" (don't
+forget to tick the checkbox "Specify default IM"). In the "ELatin" group set the
+layout to "TeX", and remember the content of the "[ELatin] on" field (by default
+"<Control>\"). You can now execute CoqIDE with the following commands (assuming
+you use a Bourne-style shell):
+
+\begin{verbatim}
+$ export GTK_IM_MODULE=uim
+$ coqide
+\end{verbatim}
+
+Activate the ELatin Input Method with Ctrl-\textbackslash, then type the
+sequence "\verb=\Gamma=". You will see the sequence being
+replaced by $\Gamma$ as soon as you type the second "a".
+
+\subsection[Character encoding for saved files]{Character encoding for saved files\label{sec:coqidecharencoding}}
+
+In the \texttt{Files} section of the preferences, the encoding option
+is related to the way files are saved. 
+
+If you have no need to exchange files with non UTF-8 aware
+applications, it is better to choose the UTF-8 encoding, since it
+guarantees that your files will be read again without problems. (This
+is because when \CoqIDE{} reads a file, it tries to automatically
+detect its character encoding.) 
+
+If you choose something else than UTF-8, then missing characters will
+be written encoded by \verb|\x{....}| or \verb|\x{........}| where
+each dot is an hexadecimal digit: the number between braces is the
+hexadecimal UNICODE index for the missing character.
+
+
+\section{Building a custom \CoqIDE{} with user \textsc{ML} code}
+
+You can do this as described in Section~\ref{Coqmktop} for a
+custom coq text toplevel, simply by adding 
+option \verb|-ide| to \verb|coqmktop|, that is something like
+\begin{quote}
+\texttt{coqmktop -ide -byte $m_1$.cmo \ldots{} $m_n$.cmo}
+\end{quote}
+or 
+\begin{quote}
+\texttt{coqmktop -ide -opt $m_1$.cmx \ldots{} $m_n$.cmx}
+\end{quote}
+
+    
+
+% $Id: RefMan-ide.tex 13477 2010-09-30 16:50:00Z vgross $ 
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: 
-- 
cgit v1.2.3

