Commit 3b8f70f8 authored by MARCHE Claude's avatar MARCHE Claude

doc: update of getting started with IDE, part 1

parent d781a155
......@@ -67,7 +67,8 @@
* Final preparation: put on the web page
** why3-0.70.tar.gz
** manual in PDF
** manual in PDF: TODO: check that macro \todo can be commented out
from ./macros.tex
** API doc in HTML (suggestion: http://why3.lri.fr/api/)
Note: check that URL of API doc is correct in doc/api.tex line 9.
** What to put in the annoucement
......@@ -84,6 +85,8 @@
* document new IDE features (C)
* update IDE section of starting.tex (C)
* document "Make obsolete" (A)
* Distribution of examples: we should distribute those who have an xml file
......
\newcommand{\todo}[1]{{\Huge\bfseries #1}}
\newcommand{\todo}[1]{{\Huge\bfseries TODO: #1}}
\newcommand{\why}{\textsf{Why3}\xspace}
\newcommand{\whyml}{\textsf{Why3ML}\xspace}
......
......@@ -36,7 +36,7 @@ friendly way. This section presents the basic use of this GUI. Please
refer to Section~\ref{sec:ideref} for a more complete description.
\begin{figure}[tbp]
\includegraphics[width=\textwidth]{gui1.png}
\includegraphics[width=\textwidth]{gui-0-70-1.png}
\caption{The GUI when started the very first time}
\label{fig:gui1}
\end{figure}
......@@ -46,34 +46,36 @@ The GUI is launched on the file above as follows.
why3ide hello_proof.why
\end{verbatim}
When the GUI is started for the first time, you should get a window
which looks like the screenshot of Figure~\ref{fig:gui1}. First of
all, the left column is a tool bar which provides different actions to
apply on goals. In this case, the section ``Provers'' is empty, which
means that you have not performed prover detection yet. You should do it
now using the menu \textsf{File/Detect provers}. Second, the middle
part is a tree view that allows to browse inside the
theories. Initially, the item of this tree are closed. We can
expand this view using the menu \textsf{View/Expand all} or its
shortcut \textsf{Ctrl-E}. This will result is something like the
screenshot of Figure~\ref{fig:gui2}.
which looks like the screenshot of Figure~\ref{fig:gui1}.
The left column is a tool bar which provides different actions to
apply on goals. The section ``Provers'' displays the provers that were
detected as installed on your computer\footnote{If not done yet, you
must perform prover autodetection using \texttt{why3config
--detect-provers}}. Three provers were detected, in this case
these are Alt-Ergo~\cite{ergo}, Coq~\cite{CoqArt} and
Simplify~\cite{simplify05}.
The middle part is a tree view that
allows to browse inside the theories.
% Initially, the item of this tree
% are closed. We can expand this view using the menu \textsf{View/Expand
% all} or its shortcut \textsf{Ctrl-E}. This will result is something
% like the screenshot of Figure~\ref{fig:gui2}.
In this tree view, we have a structured view of the file: this file
contains one theory, itself containg three goals.
\begin{figure}[tbp]
\includegraphics[width=\textwidth]{gui2.png}
\caption{The GUI with provers detected and tree view expanded}
\includegraphics[width=\textwidth]{gui-0-70-2.png}
\caption{The GUI with goal G1 selected}
\label{fig:gui2}
\end{figure}
In the tree view, we have now a strctured view of the file: this file
contains one theory, itself containg three goals. In
Figure~\ref{fig:gui2}, we also clicked on the row corresponding to
In Figure~\ref{fig:gui2}, we clicked on the row corresponding to
goal $G_1$. The \emph{task} associated with this goal is then
displayed on the top right, and the corresponding part of the input
file is shown on the bottom right part.
Notice also that three provers were detected, and are now shown
in the ``provers'' section of the left toolbar. In this example,
detected provers are Alt-Ergo~\cite{ergo}, Coq~\cite{CoqArt} and
Simplify~\cite{simplify05}.
\subsection{Calling provers on goals}
......@@ -87,7 +89,7 @@ click on the \textsf{Simplify} button. After a short time, you should
get the display of Figure~\ref{fig:gui3}.
\begin{figure}[tbp]
\includegraphics[width=\textwidth]{gui3.png}
\todo{update \includegraphics[width=\textwidth]{gui3.png}}
\caption{The GUI after Simplify prover is run on each goal}
\label{fig:gui3}
\end{figure}
......@@ -112,7 +114,7 @@ Simplify. Assuming we expand everything again, you should see now what
is displayed on Figure~\ref{fig:gui4}.
\begin{figure}[tbp]
\includegraphics[width=\textwidth]{gui4.png}
\todo{update \includegraphics[width=\textwidth]{gui4.png}}
\caption{The GUI after splitting goal $G_2$}
\label{fig:gui4}
\end{figure}
......@@ -133,7 +135,7 @@ part you modify, in order to regenerate the file if the goal is
changed.
\begin{figure}[tbp]
\includegraphics[width=\textwidth]{coqide.png}
\todo{update \includegraphics[width=\textwidth]{coqide.png}}
\caption{CoqIDE on subgoal 1 of $G_2$}
\label{fig:coqide}
\end{figure}
......@@ -153,7 +155,7 @@ Starting the IDE on the modified file and expanding everything with
\textsf{Ctrl-E}, we get the tree view shown on Figure~\ref{fig:gui5}.
\begin{figure}[tbp]
\includegraphics[width=\textwidth]{gui5.png}
\todo{update \includegraphics[width=\textwidth]{gui5.png}}
\caption{The GUI restarted after modifying goal $G_2$}
\label{fig:gui5}
\end{figure}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment