From 2cd501bf50e735362d1c29bf6cb16015ceaab97a Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Mon, 4 Jul 2011 16:23:20 +0200 Subject: [PATCH] Finished doc update for IDE and why3replayer --- ROADMAP | 6 ++---- doc/macros.tex | 4 ++-- doc/manpages.tex | 27 +++++------------------- doc/starting.tex | 53 +++++++++++++++++++++++++++++++++++++++++------- 4 files changed, 55 insertions(+), 35 deletions(-) diff --git a/ROADMAP b/ROADMAP index 737359581..cbde96e5c 100644 --- a/ROADMAP +++ b/ROADMAP @@ -99,11 +99,9 @@ under git, and distribute the XML and Coq proofs (JC) -* (partially done) update IDE section of starting.tex (C) - - not done: Replay, clean et remove +* DONE update IDE section of starting.tex (C) -* (partially done) update doc for why3replayer - - not done: parler des examples distribues ci dessus +* DONE update doc for why3replayer * DONE fix bug 12934 : Coq syntax https://gforge.inria.fr/tracker/index.php?func=detail&aid=12934&group_id=2990&atid=10293 diff --git a/doc/macros.tex b/doc/macros.tex index ed0685312..f66b96ec8 100644 --- a/doc/macros.tex +++ b/doc/macros.tex @@ -1,9 +1,9 @@ -\newcommand{\todo}[1]{{\Huge\bfseries TODO: #1}} +% \newcommand{\todo}[1]{{\Huge\bfseries TODO: #1}} \newcommand{\why}{\textsf{Why3}\xspace} \newcommand{\whyml}{\textsf{Why3ML}\xspace} -\newcommand{\eg}{\emph{e.g.}} +\newcommand{\eg}{\emph{e.g.}\xspace} % BNF grammar \newcommand{\keyword}[1]{\texttt{#1}} diff --git a/doc/manpages.tex b/doc/manpages.tex index a1709da99..4d3791906 100644 --- a/doc/manpages.tex +++ b/doc/manpages.tex @@ -410,10 +410,13 @@ why3bench -B path_to_my_bench.rc \end{verbatim} \section{The \texttt{why3replayer} tool} +\label{sec:why3replayer} The purpose of the \texttt{why3replayer} tool is to execute the proofs stored in a \why session file, as the one produced by the IDE. Its -main goal is to play non-regression tests. +main goal is to play non-regression tests, \eg you can find in +\texttt{examples/regtests.sh} a script that runs regression tests on +all the examples. The tool is inkoved in a terminal or a script using \begin{flushleft}\ttfamily @@ -422,7 +425,7 @@ The tool is inkoved in a terminal or a script using The session file \texttt{why3session.xml} stored in the given directory is loaded and all the proofs it contains are rerun. Then, any difference between the information stored in the session file and -the new run are shown. +the new run are shown. Nothing is shown when there is no change in the results, independently of the fact the considered goal is proved or not. When all the proof @@ -431,26 +434,6 @@ tree-shape pretty print, similar to the IDE tree view after doing ``Collapse proved goals'', that is when a goal, a theory or a file is fully proved the subtree is not shown. -For example, running the replayer on the \texttt{hello\_proof} example -of Section~\ref{chap:starting} is as follows. -\begin{verbatim} -$ why3replayer hello_proof -Info: found directory 'hello_proof' for the project -Opening session...[Xml warning] prolog ignored -[Reload] file '../hello_proof.why' -[Reload] theory 'HelloProof' -[Reload] transformation split_goal for goal G2 - done -Progress: 9/9 - 2/3 - +--file ../hello_proof.why: 2/3 - +--theory HelloProof: 2/3 - +--goal G2 not proved -Everything OK. -\end{verbatim} -The last line tells us that no difference was detected between the -current run and the informations in the XML file. The tree above -reminds us that the G2 is not proved. \paragraph{Exit code and options} \begin{itemize} diff --git a/doc/starting.tex b/doc/starting.tex index 5f20b4e6b..d1fe87b62 100644 --- a/doc/starting.tex +++ b/doc/starting.tex @@ -46,7 +46,7 @@ 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}. +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 @@ -57,13 +57,13 @@ 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. +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. +contains one theory, itself containg three goals. \begin{figure}[tbp] @@ -168,14 +168,53 @@ 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} +remains unproved using any of the provers. + +\subsection{Replaying obsolete proofs} + +Instead of pushing a prover's button to rerun its proofs, you can +\emph{replay} the existing but obsolete proof attempts, by clicking on +the \textsf{Replay} button. By default, \textsf{Replay} only replays +proofs that were successful before. If you want to replay all of them, +you must select the context \textsf{all goals} at the top of the left +tool bar. + +Notice that replaying can be done in batch mode, using the +\texttt{why3replayer} tool (see Section~\ref{sec:why3replayer}) For +example, running the replayer on the \texttt{hello\_proof} example is +as follows (assuming $G_2$ still is \texttt{(true -> false) /\ (true + \/ false)}). +\begin{verbatim} +$ why3replayer hello_proof +Info: found directory 'hello_proof' for the project +Opening session...[Xml warning] prolog ignored +[Reload] file '../hello_proof.why' +[Reload] theory 'HelloProof' +[Reload] transformation split_goal for goal G2 + done +Progress: 9/9 + 2/3 + +--file ../hello_proof.why: 2/3 + +--theory HelloProof: 2/3 + +--goal G2 not proved +Everything OK. +\end{verbatim} +The last line tells us that no difference was detected between the +current run and the informations in the XML file. The tree above +reminds us that the G2 is not proved. \subsection{Cleaning} -\todo{expliquer Clean et Remove} +You may want to clean some the proof attempts, \eg removing the +unsuccessful ones when a project is finally fully proved. + +A proof or a transformation can be removed by selecting it and +clicking on button \textsf{Remove}. You must confirm the +removal. Beware that there is no way to undo such a removal. -See also: why3replayer +The \textsf{Clean} button performs an automatic removal of all proofs +attempts that are unsuccessful, while there exists a successful proof +attempt for the same goal. \section{Getting Started with the \why Command} \label{sec:batch} -- GitLab