Commit 2cd501bf authored by MARCHE Claude's avatar MARCHE Claude

Finished doc update for IDE and why3replayer

parent b14f084c
......@@ -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
......
\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}}
......
......@@ -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}
......
......@@ -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}
......
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