Skip to content

why3
why3
Commit 032fe771 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

doc, update uses of HelloProof example

parent e27d6aee
Hide whitespace changes
Inline Side-by-side
Showing with 115 additions and 175 deletions
doc/HelloProof.tex
View file @ 032fe771
\begin{tabular}{| l |c |c |c |c |c |}
\hline \multicolumn{2}{|c|}{Proof obligations } & \provername{Alt-Ergo 0.93} & \provername{Coq 8.2pl1} & \provername{Simplify 1.5.4} \\
\hline \multicolumn{2}{|c|}{Proof obligations } & \provername{Alt-Ergo (0.93)} & \provername{Coq (8.3pl3)} & \provername{Simplify (1.5.4)} \\
\hline
\explanation{G1} & \explanation{ }& \noresult& \noresult& \valid{0.01} \\
\hline
\explanation{G2} & \explanation{ }& \noresult& \noresult& \unknown \\
\explanation{G2} & \explanation{ }& \unknown & \noresult& \unknown \\
\cline{2-4}
\explanation{ }& \explanation{ }\explanation{G2.0} & \unknown & \unknown & \unknown \\
\cline{2-5}
\explanation{ }& \explanation{ }\explanation{G2.1} & \unknown & \unknown & \unknown \\
\cline{2-5}
\explanation{ }& \explanation{ }\explanation{G2.2} & \valid{0.02} & \noresult& \valid{0.01} \\
\explanation{ }& \explanation{ }\explanation{G2.1} & \valid{0.02} & \noresult& \valid{0.01} \\
\hline
\explanation{G3} & \explanation{ }& \valid{0.02} & \noresult& \unknown \\
\hline \end{tabular}
doc/hello_proof.png
View replaced file @ e27d6aee View file @ 032fe771
doc/hello_proof.png

21.4 KB | W: | H:

doc/hello_proof.png

21.8 KB | W: | H:

doc/hello_proof.png
doc/hello_proof.png
doc/hello_proof.png
doc/hello_proof.png
  • 2-up
  • Swipe
  • Onion skin
doc/install.tex
View file @ 032fe771
......@@ -138,6 +138,7 @@ Appendix~\ref{sec:proverdetecttiondata} for details.
\section{Session Update after Prover Upgrade}
\label{sec:uninstalledprovers}
If you happen to upgrade a prover, e.g. installing CVC3 2.4.1 in place
of CVC3 2.2, then the proof sessions formerly recorded will still
......@@ -167,10 +168,11 @@ discard these choices via the \textsf{Preferences} dialog.
Outside the GUI, the prover upgrades are handled as follows. The
\texttt{why3replayer} tool will just ignore proof attempts marked as
archived. Conversely, a non-archived proof attempt with a
non-existent prover will be reported as a replay failure. The tool
archived. Conversely, a non-archived proof attempt with a non-existent
prover will be reported as a replay failure. The tool
\texttt{why3session} allows you to perform move or copy operations on
proof attempts in a fine-grain way, using filters, as detailed in Section~\ref{sec:why3session}.
proof attempts in a fine-grain way, using filters, as detailed in
Section~\ref{sec:why3session}.
\todo{que devient l'option -to-known-prover de why3session ?
......
doc/manpages.tex
View file @ 032fe771
......@@ -18,7 +18,7 @@ provided by the \why environment. These are as follows:
\end{description}
All these tools accept a common subset of command-line options. In
particular the option -help which displays the usage and options.
particular the option \verb|-help| which displays the usage and options.
\begin{description}
\item[\texttt{-L} $d$]
adds $d$ in the load path, to search for theories.
......@@ -257,15 +257,38 @@ A copy of the tools already available in the left toolbar, plus:
A very short online help, and some information about this software.
\end{description}
\subsection{Preferences}
\subsection{Preferences Dialog}
The preferences window allows you customize
The preferences dialog allows you to customize various settings. These
are groups together under several tabs
\begin{description}
\item[\textsf{General Settings} tab]
\begin{itemize}
\item the default editor to use when the \textsf{Edit} button is
pressed\footnote{This might be overridden for a specific prover. The only way
to do that for the moment is to manually edit the configuration file.}
\item the time limit given to provers, in seconds
\item the maximal number of simultaneous provers allowed to run in parallel.
\item the maximal number of simultaneous provers allowed to run in
parallel.
\item A few display settings:
\begin{itemize}
\item introduce premises: if selected, the goal of the task shownin
top-right window is displayed after introduction of universally
quantified variables and implications, e.g. a goal of the form
$\forall x: t. P \rightarrow Q$ is displayed as
\[
\begin{array}{l}
x : t \\
H : P \\
\hline
Q
\end{array}
\]
\item show labels in formulas
\item show source locations in formulas
\item show time limit for each proof
\end{itemize}
\item the policy for saving session:
\begin{itemize}
\item always save on exit (default): the current state of the proof session is saving on exit
......@@ -273,9 +296,16 @@ The preferences window allows you customize
\item ask whether to save: on exit, a popup window ask whether you
want to save or not.
\end{itemize}
\todo{manque des choses}
\end{itemize}
\item[\textsf{Provers} tab]
Here you can selected which of the installed provers you want to see
as buttons in the left toolbar
\item[\textsf{Uninstalled Provers} tab]
Here are shown all the decision previously taken for uninstalled
provers, as described in
Section~\ref{sec:uninstalledprovers}. You can remove any recorded
decision by clicking on it.
\end{description}
\section{The \texttt{why3ml} tool}
......@@ -558,7 +588,29 @@ The proof statistics given by option \verb|--stats| are as follows:
goals \emph{where the prover was successfull}.
\end{itemize}
\todo{Example}
For example, here are the session statistics produced on the ``hello
proof'' example of Section~\ref{chap:starting}.
\begin{verbatim}
== Number of goals ==
total: 5 proved: 3
== Goals not proved ==
+-- file ../hello_proof.why
+-- theory HelloProof
+-- goal G2
+-- transformation split_goal
+-- goal G2.0
== Goals proved by only one prover ==
+-- file ../hello_proof.why
+-- theory HelloProof
+-- goal G1: Simplify (1.5.4) (0.01)
+-- goal G3: Alt-Ergo (0.93) (0.02)
== Statistics per prover: number of proofs, time (minimum/maximum/average) in seconds ==
Alt-Ergo (0.93) : 2 0.02 0.02 0.02
Simplify (1.5.4) : 2 0.01 0.01 0.01
\end{verbatim}
\subsection{Command \texttt{latex}}
......
examples/hello_proof/why3session.xml
View file @ 032fe771
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="./hello_proof/why3session.xml">
name="examples/hello_proof/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
version="0.93"/>
<prover
id="1"
name="CVC3"
version="2.2"/>
<prover
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="3"
name="Coq"
version="8.3pl3"/>
<prover
id="4"
id="2"
name="Simplify"
version="1.5.4"/>
<prover
id="5"
name="Z3"
version="2.19"/>
<prover
id="6"
name="Z3"
version="3.2"/>
<file
name="../hello_proof.why"
verified="false"
expanded="false">
expanded="true">
<theory
name="HelloProof"
locfile="./hello_proof/../hello_proof.why"
locfile="examples/hello_proof/../hello_proof.why"
loclnum="1" loccnumb="7" loccnume="17"
verified="false"
expanded="true">
......@@ -44,221 +28,123 @@
name="My very first Why3 theory"/>
<goal
name="G1"
locfile="./hello_proof/../hello_proof.why"
locfile="examples/hello_proof/../hello_proof.why"
loclnum="3" loccnumb="7" loccnume="9"
sum="4daf9675e70ee6481b1153fe95f7c750"
proved="true"
expanded="true"
shape="t">
<proof
prover="5"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="2"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="10"
timelimit="4"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="G2"
locfile="./hello_proof/../hello_proof.why"
locfile="examples/hello_proof/../hello_proof.why"
loclnum="5" loccnumb="7" loccnume="9"
sum="b16d2c9608c416dc0059ba3e95264abe"
proved="false"
expanded="true"
shape="fOtAfIt">
<proof
prover="4"
timelimit="10"
prover="2"
timelimit="4"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="0"
timelimit="4"
obsolete="false"
archived="false">
<result status="unknown" time="0.03"/>
</proof>
<transf
name="split_goal"
proved="false"
expanded="true">
<goal
name="G2.1"
locfile="./hello_proof/../hello_proof.why"
name="G2.0"
locfile="examples/hello_proof/../hello_proof.why"
loclnum="5" loccnumb="7" loccnume="9"
sum="b84cad55140412a1b6f988cba7a0ebd1"
proved="false"
expanded="true"
shape="fIt">
<proof
prover="5"
timelimit="5"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="5"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="3"
edited="hello_proof_HelloProof_G2_1.v"
prover="1"
timelimit="4"
edited="hello_proof_HelloProof_G2_3.v"
obsolete="false"
archived="false">
<result status="unknown" time="0.48"/>
<result status="unknown" time="0.76"/>
</proof>
<proof
prover="6"
timelimit="2"
prover="2"
timelimit="4"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="10"
prover="0"
timelimit="4"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="unknown" time="0.03"/>
</proof>
</goal>
<goal
name="G2.2"
locfile="./hello_proof/../hello_proof.why"
name="G2.1"
locfile="examples/hello_proof/../hello_proof.why"
loclnum="5" loccnumb="7" loccnume="9"
sum="fdf75c799e5829c6e57c69e76f88886a"
proved="true"
expanded="true"
shape="fOt">
<proof
prover="5"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="2"
timelimit="4"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="10"
prover="0"
timelimit="4"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="G3"
locfile="./hello_proof/../hello_proof.why"
locfile="examples/hello_proof/../hello_proof.why"
loclnum="9" loccnumb="7" loccnume="9"
sum="d89b799516da55943a55251953e1068e"
proved="true"
expanded="true"
shape="ainfix >=ainfix *V0V0c0F">
<proof
prover="5"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
shape="ainfix &gt;=ainfix *V0V0c0F">
<proof
prover="2"
timelimit="5"
timelimit="4"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="2"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="3"
prover="0"
timelimit="4"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
......
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