diff options
| -rw-r--r-- | doc/Makefile | 6 | ||||
| -rw-r--r-- | doc/RefMan-ide.tex | 127 | ||||
| -rw-r--r-- | doc/RefMan-modr.tex | 4 | ||||
| -rw-r--r-- | doc/coqide.png | bin | 35357 -> 20953 bytes |
4 files changed, 83 insertions, 54 deletions
diff --git a/doc/Makefile b/doc/Makefile index 6f7f1fc70..3e1e14f81 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -1,6 +1,7 @@ # Makefile for the Coq documentation -# You need the environment variables COQTOP and COQBIN to be correctly set +# You need the environment variable COQBIN to be correctly set +# (COQTOP is autodetected) # (some files are preprocessed using Coq and some part of the documentation # is automatically built from the theories sources) @@ -15,6 +16,7 @@ DOCCOQTOP=$(COQBIN)/coqtop #.byte DOCCOQC=$(COQBIN)/coqc +COQTOP=`$(DOCCOQC) -where` COQTEX=$(COQBIN)/coq-tex -image $(DOCCOQTOP) -v -sl -small #COQWEBSTY=$(HOME)/lib/tex/ COQWEBSTY=/usr/share/texmf/tex/latex/misc/ @@ -95,7 +97,7 @@ version.tex: Makefile #image coqide coqide.eps: coqide.png - pngtopnm coqide.png | pnmtops -noturn -rle > coqide.eps + pngtopnm coqide.png | pnmtops -equalpixels -noturn -rle > coqide.eps # dvips et dviselect existent sur loupiac diff --git a/doc/RefMan-ide.tex b/doc/RefMan-ide.tex index b610b7cc0..02b82985d 100644 --- a/doc/RefMan-ide.tex +++ b/doc/RefMan-ide.tex @@ -27,59 +27,86 @@ obviously no meaning for \coqide{} being ignored. \label{fig:coqide} \end{figure} -\coqide{} main screen is shown on Figure~\ref{fig:coqide}. (Attention -il manque la toolbar sur cet ecran car je l'ai enleve par defaut) At -the top is a menu bar, the left window is displaying the various -buffers, the upper right window is the ``goal window'', where goals to -prove are displayed. The lower right window is the ``message window'', +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{The \texttt{File} menu} - -Open/Create - -Save - -Save as - -Save all - -Revert All Buffers - -Close Buffer - -Print - -Export to - -Rehighlight - -Quit - -\section{The \texttt{Edit} menu} - - -\section{The \texttt{Navigation} menu} - -Remplacer forward to et backward to par goto ? -idem pour la toolbar - -\section{The \texttt{Try Tactics} menu} - -Is it useful ? - -\section{The \texttt{Templates} menu} - -Need update to V8 syntax - -\section{The \texttt{Commands} menu} - -\section{The \texttt{Externals} menu} - -\section{The \texttt{Configuration} menu} - -\section{The \texttt{Help} menu} +\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$ diff --git a/doc/RefMan-modr.tex b/doc/RefMan-modr.tex index 127b8830c..47699df60 100644 --- a/doc/RefMan-modr.tex +++ b/doc/RefMan-modr.tex @@ -404,14 +404,14 @@ section~\ref{delta} \item [ACC-INDP] \inference{% \frac{ - \WT{E}{}{p:\sig{\Spec_1;\dots;\Spec_n;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}} + \WT{E}{}{p}{\sig{\Spec_1;\dots;\Spec_n;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}} }{ \WTRED{E}{}{p.I_i}{\triangleright_\delta}{p'.I_i} } } \inference{% \frac{ - \WT{E}{}{p:\sig{\Spec_1;\dots;\Spec_n;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}} + \WT{E}{}{p}{\sig{\Spec_1;\dots;\Spec_n;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}} }{ \WTRED{E}{}{p.c_i}{\triangleright_\delta}{p'.c_i} } diff --git a/doc/coqide.png b/doc/coqide.png Binary files differindex d2f1e5d9b..a6a0f5850 100644 --- a/doc/coqide.png +++ b/doc/coqide.png |
