more doc on IDE

ROADMAP

@@ -77,6 +77,7 @@
    - incompatible changes in syntax: function, predicate, and, or
    - session database in XML format instead of sqlite3
    - threads problem in IDE solved (by not using threads anymore)
+   - IDE: not necessary to exit to change the input file: just use "reload"
 ** as soon as possible: update why3 output of Why2, release Why 2.30
 
 * increment the magic number in config (A)
@@ -85,8 +86,6 @@
 
 * 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
@@ -96,6 +95,8 @@
 * (done) update doc for why3replayer
  - not done: parler des examples distribues ci dessus
 
+* update IDE section of starting.tex (C)
+
 * DONE doc: citer l'article Boogie 2011 quelque part
 
 * DONE deplacer le bouton "Cancel" dans le menu "tools",

doc/macros.tex

@@ -33,7 +33,8 @@
 \newcommand{\emptystring}{$\epsilon$}
 \newcommand{\below}{See\; below}
 
-%%% Local Variables: 
+%%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "manual"
-%%% End: 
+%%% TeX-PDF-mode: t
+%%% End:

doc/manpages.tex

@@ -237,7 +237,7 @@ the actions of the various menus and buttons of the interface.
   conjunction of two or more goals.
 
 \item[Inline] If the goal is headed by a defined predicate symbol,
-  expands it with this definition. [NOT YET AVAILABLE]
+  expands it with this definition.
 
 \item[Edit] Start an editor on the selected task.
 
@@ -248,10 +248,17 @@ the actions of the various menus and buttons of the interface.
   corresponding proof script. The modifications are saved, and can be
   retrieved later even if the goal was modified.
 
-\item[Replay] replay all obsolete proofs [NOT YET AVAILABLE]
+\item[Replay] Replay all obsolete proofs
+
+  If ``only unproved goals'' is selected, only formerly successful
+  proofs are rerun. If ``all goals'', then all obsolete proofs are
+  rerun, successful or not.
 
 \item[Remove] Removes a proof attempt or a transformation.
 
+\item[Clean] Removes any unsuccessful proof attempt for which there is
+  another successful proof attempt for the same goal
+
 \end{description}
 
 \subsection{Menus}
@@ -259,9 +266,11 @@ the actions of the various menus and buttons of the interface.
 \paragraph{Menu \textsf{File}}
 \begin{description}
 \item[Add File] adds a file in the GUI
-\item[Detect provers] runs provers auto-detection
+%\item[Detect provers] runs provers auto-detection
 \item[Preferences] opens a window for modifying preferred
   configuration, see details below
+\item[Reload] \todo{}
+\item[Save session] \todo{}
 \item[Quit] exits the GUI
 \end{description}
 
@@ -270,8 +279,8 @@ the actions of the various menus and buttons of the interface.
 \item[Expand All] expands all the rows of the tree view
 \item[Collapse proved goals] closes all the rows of the tree view
   which are proved.
-\item[Hide proved goals] completely hides the proved rows of the tree
-  view [EXPERIMENTAL]
+% \item[Hide proved goals] completely hides the proved rows of the tree
+%   view [EXPERIMENTAL]
 \end{description}
 
 \paragraph{Menu \textsf{Tools}}
@@ -289,11 +298,12 @@ The preferences window allows you customize
   to do that for the moment is to manually edit the config file)
 \item the time limit given to provers, in seconds
 \item the maximal number of simultaneous provers allowed to run in parallel.
+\item The policy for saving session \todo{}
 \end{itemize}
 
 \subsection{Structure of the database file}
 
-[TO BE COMPLETED LATER]
+\todo{[TO BE COMPLETED LATER]}
 
 \section{The \texttt{why3ml} tool}
 

doc/starting.tex

@@ -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]{gui-0-70-1.png}
+  \includegraphics[width=\textwidth]{gui-0-70-1.png}
   \caption{The GUI when started the very first time}
   \label{fig:gui1}
 \end{figure}
@@ -89,15 +89,15 @@ click on the \textsf{Simplify} button. After a short time, you should
 get the display of Figure~\ref{fig:gui3}.
 
 \begin{figure}[tbp]
-\todo{update   \includegraphics[width=\textwidth]{gui3.png}}
+\includegraphics[width=\textwidth]{gui-0-70-3.png}
   \caption{The GUI after Simplify prover is run on each goal}
   \label{fig:gui3}
 \end{figure}
 
-The row corresponding to goal $G_1$ is now closed, and marked with
-green ``checked'' icon in the status column. This means that the goal
-is proved by the Simplify prover. On the contrary, the two other goals
-are not proved, they are marked with an orange question mark.
+The goal $G_1$ is now marked with a green ``checked'' icon in the
+status column. This means that the goal is proved by the Simplify
+prover. On the contrary, the two other goals are not proved, they remain
+marked with an orange question mark.
 
 You can immediately attempt to prove the remaining goals using another
 prover, {\eg} Alt-Ergo, by clicking on the corresponding button. The
@@ -110,12 +110,12 @@ to it.  Since $G_2$ is a conjunction, a possibility is to split it
 into subgoals. You can do that by clicking on the \textsf{Split}
 button of section ``Transformations'' of the left toolbar. Now you
 have two subgoals, and you can try again a prover on them, for example
-Simplify. Assuming we expand everything again, you should see now what
-is displayed on Figure~\ref{fig:gui4}.
+Simplify. We already have a lot of goals and proof attempts, so it is a good idea to close the sub-trees which are already proved: this can be done by the menu \textsf{View/Collapse proved goals}, or even better by its shortcut ``Ctrl-C''.
+You should see now what is displayed on Figure~\ref{fig:gui4}.
 
 \begin{figure}[tbp]
-\todo{update   \includegraphics[width=\textwidth]{gui4.png}}
-  \caption{The GUI after splitting goal $G_2$}
+ \includegraphics[width=\textwidth]{gui-0-70-4.png}
+  \caption{The GUI after splitting goal $G_2$ and collapsing proved goals}
   \label{fig:gui4}
 \end{figure}
 
@@ -127,7 +127,7 @@ now is editing the proof: select that row and then click on the
 \textsf{Edit} button in section ``Tools'' of the toolbar. This should
 launch the Coq proof editor, which is \texttt{coqide} by default (see
 Section~\ref{sec:ideref} for details on how to configure this). You get
-now a regular Coq file fo fill in, as shown on Figure~\ref{fig:coqide}.
+now a regular Coq file to fill in, as shown on Figure~\ref{fig:coqide}.
 Please take care of the comments of this file. Only the part between
 the two last comments can be modified. Moreover, these comments
 themselves should not be modified at all, they are used to mark the
@@ -135,7 +135,7 @@ part you modify, in order to regenerate the file if the goal is
 changed.
 
 \begin{figure}[tbp]
-\todo{update   \includegraphics[width=\textwidth]{coqide.png}}
+  \includegraphics[width=\textwidth]{coqide-0-70.png}
   \caption{CoqIDE on subgoal 1 of $G_2$}
   \label{fig:coqide}
 \end{figure}
@@ -147,28 +147,35 @@ explained below.
 \subsection{Modifying the input}
 
 Currently, the GUI does not allow to modify the input file. You must
-exit the GUI and modify the file by some editor of your choice. Let's assume we change the goal $G_2$ by replacing the first occurrence of true by false, \eg
+edit the file external by some editor of your choice. Let's assume we
+change the goal $G_2$ by replacing the first occurrence of true by
+false, \eg
 \begin{verbatim}
   goal G2 : (false -> false) /\ (true \/ false)
 \end{verbatim}
-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}.
+We can reload the modified file in the IDE using menu \textsf{File/Reload}, or the shortcut ``Ctrl-R''. We get the tree view shown on Figure~\ref{fig:gui5}.
 
 \begin{figure}[tbp]
-\todo{update   \includegraphics[width=\textwidth]{gui5.png}}
-  \caption{The GUI restarted after modifying goal $G_2$}
+  \includegraphics[width=\textwidth]{gui-0-70-5.png}
+  \caption{File reloaded after modifying goal $G_2$}
   \label{fig:gui5}
 \end{figure}
 
 The important feature to notice first is that all the previous proof
-attempts and transformations were saved in a database --- an SQLite3
-file created when the \why file was opened in the GUI for the first
-time. Then, for
-all the goals that remain unchanged, the previous proofs are shown
-again. For the parts that changed, the previous proofs attempts are
-shown but marked with "(obsolete)" so that you know the results are
-not accurate. You can now retry to prove all what remains unproved
-using any of the provers, using the button ``Replay''.
+attempts and transformations were saved in a database --- an XML file
+created when the \why file was opened in the GUI for the first
+time. Then, for all the goals that remain unchanged, the previous
+proofs are shown again. For the parts that changed, the previous
+proofs attempts are shown but marked with "(obsolete)" so that you
+know the results are not accurate. You can now retry to prove all what
+remains unproved using any of the provers, using the button
+``Replay''. \todo{Il faut selectioner all goals pour cela}
+
+\subsection{Cleaning}
+
+\todo{expliquer Clean et Remove}
+
+See also: why3replayer
 
 \section{Getting Started with the \why Command}
 \label{sec:batch}

examples/hello_proof.why

@@ -8,4 +8,4 @@ theory HelloProof "My very first Why3 theory"
 
   goal G3: forall x:int. x*x >= 0
 
-end  
+end

examples/hello_proof/hello_proof_HelloProof_G2_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Theorem G2 : False.
+(* YOU MAY EDIT THE PROOF BELOW *)
+intuition.
+
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/hello_proof/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
-<why3session name="examples/hello_proof/why3session.xml">
+<why3session name="hello_proof/why3session.xml">
  <file name="../hello_proof.why" verified="false" expanded="true">
   <theory name="HelloProof" verified="false" expanded="true">
-   <goal name="G1" sum="da0794d2f4de035d230d26e93d3e1afe" proved="false" expanded="true">
+   <goal name="G1" sum="da0794d2f4de035d230d26e93d3e1afe" proved="true" expanded="true">
+    <proof prover="simplify" timelimit="10" edited="" obsolete="false">
+     <result status="valid" time="0.01"/>
+    </proof>
    </goal>
    <goal name="G2" sum="07e54d9a25fa3174d5d5bf7ce71a13dc" proved="false" expanded="true">
+    <proof prover="simplify" timelimit="10" edited="" obsolete="true">
+     <result status="valid" time="0.01"/>
+    </proof>
    </goal>
-   <goal name="G3" sum="8813554ea4313f64f3efc3330036b5e9" proved="false" expanded="true">
+   <goal name="G3" sum="8813554ea4313f64f3efc3330036b5e9" proved="true" expanded="true">
+    <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+     <result status="valid" time="0.02"/>
+    </proof>
    </goal>
   </theory>
  </file>