Commit c8b62ca8 authored by MARCHE Claude's avatar MARCHE Claude

Improved doc for why3replauer -latex

parent 84dbdac2
\begin{tabular}{| l |c |c |c |c |c |}
\hline Proof obligations & \provername{Alt-Ergo 0.93} & \provername{Coq 8.2pl1} & \provername{Simplify 1.5.4} \\
\hline
\explanation{G1} & \noresult& \noresult& \valid{0.01} \\
\hline
\explanation{G2} & \noresult& \noresult& \unknown \\
\hline
\explanation{G3} & \valid{0.02} & \noresult& \unknown \\
\hline \end{tabular}
......@@ -490,62 +490,49 @@ not and you have to use the IDE to update it.
\item option \texttt{-s}: suppresses the output of the final tree view
\item option \texttt{-I \textsl{<path>}}: add \textsl{<path>} to the loadpath
\item option \texttt{-force}: force writing a new session file even if some proofs did not replay correctly.
\item option \texttt{-latex \textsl{<file.tex>}}: produce a summary of the replay
under the form of a tabular environment in LaTeX, one tabular for each theory, in the file \texttt{\textsl{<file.tex>}}.
\item option \texttt{-html \textsl{<file.html>}}: produce a summary of the replay in
HTML syntax.
\item option \texttt{-latex \textsl{<dir>}}: produce a summary of
the replay under the form of a tabular environment in LaTeX, one
tabular for each theory, one per file, in directory \texttt{\textsl{<dir>}}.
\item option \texttt{-latex2 \textsl{<dir>}}: alternate version of
LaTeX output, with a different layout of the tables.
% \item option \texttt{-html \textsl{<file.html>}}: produce a summary of
% the replay in HTML syntax.
\end{itemize}
About \texttt{latex} output, we propose another option
\texttt{-latex2} with the same parameters. The difference between
these two options is the layout of the tabular.
Generated \latex files contain a set of macros. Definitions of these macros is left to the care of user depending on what he wants, or not, highlight.
In the following, we will give some suggestions for these macros:
\paragraph{Customizing LaTeX output}
The generated LaTeX files contain some macros that must be defined
externally. Various definitions can be given to them to customize the
output.
\begin{itemize}
\item For columns names which correspond to the prover names:
\begin{verbatim}
\usepackage{rotating}
\newcommand{\provername}[1]{\cellcolor{yellow!25}\begin{sideways}\textbf{#1}~~\end{sideways}}|
\end{verbatim}
\item \verb|\provername|: macro with one parameter, a prover name
\item \verb|\valid|: macro with one parameter, used where the corresponding prover answers that the goal is valid. The parameter is the time in seconds.
\item \verb|\noresult|: macro without parameter, used where no result
exists for the corresponding prover
\item \verb|\timeout|: macro without parameter, used where the corresponding prover reached the time limit
\item \verb|\explanation|: macro with one parameter, the goal name or its explnation
\end{itemize}
\begin{figure}[t]
\begin{center}
\input{HelloProof.tex}
\end{center}
\verbatiminput{./replayer_macros.tex}
\caption{Sample macros for the LaTeX option of why3replayer}
\label{fig:replayer}
\end{figure}
Figure~\ref{fig:replayer} proposes some suggestions for these macros, together
with the table obtained from the hello proof example of Section~\ref{chap:starting}.
\item For regrouping the empty cells. That is where no result is informed for the corresponding prover:
\begin{verbatim}
\usepackage{colortbl}
\newcommand{\noresult}{\multicolumn{1}{>{\columncolor[gray]{0.8}}c|}{~}}
\end{verbatim}
\item When the prover reachs the timeout:
\begin{verbatim}
\usepackage{wasysym}
\newcommand{\timeout}{\cellcolor{red!20}\clock}
\end{verbatim}
\item For explanations associating to the proof obligations:
\begin{verbatim}
\newcommand{\explanation}[1]{\cellcolor{yellow!13}\textsl{#1}}
\end{verbatim}
\section{The \texttt{why3.conf} configuration file}
\label{sec:whyconffile}
One can use a custom configuration file. \texttt{why3config}
and other \texttt{why3} tools use priorities for which
user's configuration file to consider:
\begin{itemize}
\item the file specified by the \texttt{-C} or \texttt{-{}-config} options,
\item the file specified by the environment variable
\texttt{WHY3CONFIG} if set.
\item the file \texttt{\$HOME/.why3.conf}
(\texttt{\$USERPROFILE/.why3.conf} under Windows) or, in the case of
local installation, \texttt{why3.conf} in Why3 sources top directory.
\end{itemize}
If none of these files exists, a built-in default configuration is used.
The configuration file is a human-readable text file, which consists
of association pairs arranged in sections. Here follows an example of
configuration file.
\begin{figure}[t]
\begin{verbatim}
[main ]
loadpath = "/usr/local/share/why3/theories"
......@@ -576,6 +563,28 @@ editor = ""
name = "Alt-Ergo"
version = "0.91"
\end{verbatim}
\caption{Sample why3.conf file}
\label{fig:why3conf}
\end{figure}
One can use a custom configuration file. \texttt{why3config}
and other \texttt{why3} tools use priorities for which
user's configuration file to consider:
\begin{itemize}
\item the file specified by the \texttt{-C} or \texttt{-{}-config} options,
\item the file specified by the environment variable
\texttt{WHY3CONFIG} if set.
\item the file \texttt{\$HOME/.why3.conf}
(\texttt{\$USERPROFILE/.why3.conf} under Windows) or, in the case of
local installation, \texttt{why3.conf} in Why3 sources top directory.
\end{itemize}
If none of these files exists, a built-in default configuration is used.
The configuration file is a human-readable text file, which consists
of association pairs arranged in sections. Figure~\ref{fig:why3conf}
shows an example of configuration file.
A section begins with a header inside square brackets and ends at the
beginning of the next section. The header of a
......
......@@ -31,6 +31,7 @@
\usepackage{ifthen}
\input{./macros.tex}
\input{./replayer_macros.tex}
\input{./version.tex}
......
\usepackage{xcolor}
\usepackage{rotating}
\newcommand{\provername}[1]{\cellcolor{yellow!25}
\begin{sideways}\textbf{#1}~~\end{sideways}}
\usepackage{colortbl}
\newcommand{\noresult}{\multicolumn{1}{>{\columncolor[gray]{0.8}}c|}{~}}
\usepackage{wasysym}
\newcommand{\timeout}{\cellcolor{red!20}\clock}
\newcommand{\explanation}[1]{\cellcolor{yellow!13}\textsl{#1}}
\newcommand{\valid}[1]{\cellcolor{green!13}#1}
\newcommand{\unknown}{\cellcolor{red!20}?}
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="./hello_proof/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../hello_proof.why" verified="false" expanded="true">
<theory name="HelloProof" verified="false" expanded="true">
<goal name="G1" sum="b060ede45247709977a2817a7ac6b4bd" proved="true" expanded="true" shape="t">
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<why3session
name="hello_proof/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.2pl1"/>
<prover
id="coq-realize"
name="Coq Realize"
version="8.2pl1"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="eprover"
name="Eprover"
version="1.4 Namring"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3"
name="Z3"
version="2.19"/>
<file
name="../hello_proof.why"
verified="false"
expanded="true">
<theory
name="HelloProof"
verified="false"
expanded="true">
<goal
name="G1"
sum="b060ede45247709977a2817a7ac6b4bd"
proved="true"
expanded="true"
shape="t">
<proof
prover="simplify"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G2" sum="29d2b92fcf63e1df963c30f4822b9801" proved="false" expanded="true" shape="fOtAfIt">
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<goal
name="G2"
sum="29d2b92fcf63e1df963c30f4822b9801"
proved="false"
expanded="true"
shape="fOtAfIt">
<proof
prover="simplify"
timelimit="10"
edited=""
obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
<transf name="split_goal" proved="false" expanded="true">
<goal name="G2.1" sum="12fa33a25c8f3a0a042196b8d8c3a85b" proved="false" expanded="true" shape="fIt">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.02"/>
<transf
name="split_goal"
proved="false"
expanded="true">
<goal
name="G2.1"
sum="12fa33a25c8f3a0a042196b8d8c3a85b"
proved="false"
expanded="true"
shape="fIt">
<proof
prover="coq"
timelimit="3"
edited="hello_proof_HelloProof_G2_1.v"
obsolete="false">
<result status="unknown" time="0.43"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="unknown" time="0.03"/>
</proof>
<proof
prover="simplify"
timelimit="10"
edited=""
obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal name="G2.2" sum="0a8787ba8a8ae75c6e58904fa2a5ece0" proved="true" expanded="true" shape="fOt">
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<goal
name="G2.2"
sum="0a8787ba8a8ae75c6e58904fa2a5ece0"
proved="true"
expanded="true"
shape="fOt">
<proof
prover="alt-ergo"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="simplify"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
<goal name="G3" sum="957de34bf31dbdb537afc46f3eaaa47b" proved="true" expanded="true" shape="ainfix >=ainfix *V0V0c0F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<goal
name="G3"
sum="957de34bf31dbdb537afc46f3eaaa47b"
proved="true"
expanded="true"
shape="ainfix >=ainfix *V0V0c0F">
<proof
prover="simplify"
timelimit="3"
edited=""
obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
......
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