Commit bfcb73aa authored by MARCHE Claude's avatar MARCHE Claude

documentation for why3session

parent 513794b4
......@@ -87,10 +87,10 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
==================== Roadmap for release 0.72 ========================
== New Features to annouce ==
== New Features to announce ==
* Coq Realizations
* tool why3session with commands latex, html, stats, etc
* tool why3session with commands latex, html, etc
* tool why3doc
* Support for several versions of the same prover
* Improved IDE:
......
......@@ -555,12 +555,44 @@ otherwise.
\section{The \texttt{why3session} tool}
\label{sec:why3session}
The program \texttt{why3session} allows to manipulate why3 session on
the command line. It thus allows to batch modifications to several
sessions at once. This tool provides several subcommands:
\texttt{info}, \texttt{rm}, \texttt{copy}, \texttt{mod}.
The program \texttt{why3session} allows to extract informations from
proof sessions on the command line, or even modify them to some
extent. The invocation of this program is done under the form
\begin{verbatim}
why3session <command> [options] <session directories>
\end{verbatim}
The available commands are the following:
\begin{description}
\item[\texttt{info}] prints informations and statistics about sessions.
\item[\texttt{latex}] outputs session contents in LaTeX format.
\item[\texttt{html}] outputs session contents in HTML format.
\item[\texttt{mod}] modifies some of the proofs, selected by a filter.
\item[\texttt{copy}] duplicates some of the proofs, selected by a filter.
\item[\texttt{copy-archive}] same as copy but also archives the
original proofs.
\item[\texttt{rm}] remove some of the proofs, selected by a filter.
\end{description}
The first three commands do not modify the sessions, whereas the four
last modify them. Only the proof attempts recorded are modified. No
prover is called on the modified or created proof attempts, and
consequently the proof status is always marked as obsolete.
All the commands above share the following common set of options:
common options:
\begin{description}
\item[\texttt{-C <file>}] reads configuration from \texttt{file}
\item[\texttt{--config}] same as \texttt{-C}
\item[\texttt{--extra-config <file>}] reads additional configuration from \texttt{<file>}
\item[\texttt{-L <dir>}] adds \texttt{<dir>} to the library search path
\item[\texttt{--library}] same as \texttt{-L}
\item[\texttt{-v}] prints version information
\item[\texttt{--list-debug-flags}] lists known debug flags
\item[\texttt{--debug-all}] sets all debug flags (except flags which change the behavior)
\item[\texttt{--debug <flag>}] sets a debug flag
\end{description}
Currently this tool reports or modifies only proof attempts.
\subsection{Command \texttt{info}}
\texttt{why3session info} reports informations:
\begin{itemize}
......@@ -597,6 +629,88 @@ why3session info --edited-files --print0 vstte12_bfs.mlw | \
\end{itemize}
\paragraph{Session Statistics}
\todo{DETAILLER why3session info --stats}
\subsection{Command \texttt{latex}}
Command \texttt{latex} produces a summary of the replay under the
form of a tabular environment in LaTeX, one tabular for each theory,
one per file.
Option \texttt{-style 2} produces an alternate
version of LaTeX output, with a different layout of the tables.
\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 \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 explanation
\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}.
\subsection{Command \texttt{html}}
This command produces a summary of the proof session in HTML syntax.
There are three styles of output: table, simpletree, jstree
'simple' use only 'ul' and 'il' tag. 'jstree' use the 'jstree' plugin
of the javascript library 'jquery'.
\todo{Detailler}
Specific options for this command are as follows.
\begin{description}
\item[\texttt{-o}]
the directory to output the produces files ('-' for stdout)
\item[\texttt{--context}] adds context around the generated code in
order to allow direct visualisation (header, css, ...). It also adds
in the directory all the needed external files. It can't be set with
stdout output.
\item[\texttt{--style <s>}] sets the style to
use, among \texttt{simpletree}, \texttt{jstree} and \texttt{table}, defaults to \texttt{table}.
\item[\texttt{--add\_pp <suffix> <cmd> <out\_suffix>}] adds for the
given prefix the given pretty-printer, the new file as the given
out\_suffix. cmd must contain
'\%i' which will be replaced by the input file
and '\%o' which will be replaced by the
output file.
\item[\texttt{--coqdoc}] use the coqdoc command to display Coq proof
scripts. This is equivalent to \texttt{--add\_pp .v "coqdoc
--no-index --html -o \%o \%i" .html}
\end{description}
\subsection{Commands modifying the proof attempts}
The subcommands \texttt{mod}, \texttt{copy}, and \texttt{rm} share the
same set of options for selecting the proof attempts to work on:
\begin{itemize}
......@@ -662,50 +776,6 @@ corresponds to \verb|--filter-verified-goal --conservative| and
removes the proof attempts that are not verified but which correspond
to verified goals.
\subsubsection{Session Statistics}
\todo{DETAILLER why3session stats}
\subsubsection{Session Dump in LaTeX or HTML Format}
\begin{itemize}
\item Command \texttt{latex} produces a summary of the
replay under the form of a tabular environment in LaTeX, one tabular
for each theory, one per file.
Option \texttt{-style 2} produces an alternate
version of LaTeX output, with a different layout of the tables.
\item command \texttt{html} produces a summary of the replay in HTML syntax.
\end{itemize}
\todo{DETAILLER}
\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 \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 explanation
\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}.
\section{The \texttt{why3.conf} configuration file}
\label{sec:whyconffile}
......
......@@ -23,13 +23,13 @@ open Why3session_lib
let cmds =
[|
Why3session_info.cmd;
Why3session_latex.cmd;
Why3session_html.cmd;
Why3session_copy.cmd_mod;
Why3session_copy.cmd_copy;
Why3session_copy.cmd_archive;
Why3session_info.cmd;
Why3session_rm.cmd;
Why3session_latex.cmd;
Why3session_html.cmd;
|]
let exec_name = Sys.argv.(0)
......@@ -37,7 +37,7 @@ let exec_name = Sys.argv.(0)
let print_usage () =
let maxl = Array.fold_left
(fun acc e -> max acc (String.length e.cmd_name)) 0 cmds in
eprintf "%s <command> [options]@.@.available commands:@.@[<hov>%a@]@\n@."
eprintf "%s <command> [options] <session directories>@\n@\navailable commands:@.@[<hov>%a@]@\n@."
exec_name
(Pp.print_iter1 Array.iter Pp.newline
(fun fmt e -> fprintf fmt "%s @[<hov>%s@]"
......
......@@ -52,28 +52,21 @@ let set_opt_pp_in,set_opt_pp_cmd,set_opt_pp_out =
let spec =
("-o",
Arg.Set_string output_dir,
" The directory to output the files ('-' for stdout)") ::
"<path> output directory ('-' for stdout)") ::
("--context", Arg.Set opt_context,
" Add context around the generated code in order to allow direct \
visualisation (header, css, ...). It also add in the directory \
all the needed external file. It can't be set with stdout output") ::
" adds context around the generated HTML code") ::
("--style", Arg.Symbol (["simpletree";"jstree";"table"], set_opt_style),
" Set the style to use, defaults to '" ^ default_style ^ "'."
(* "'simple' use only 'ul' and 'il' tag. 'jstree' use \
the 'jstree' plugin of the javascript library 'jquery'." *)
" style to use, defaults to '" ^ default_style ^ "'."
) ::
("--add_pp", Arg.Tuple
[Arg.String set_opt_pp_in;
Arg.String set_opt_pp_cmd;
Arg.String set_opt_pp_out],
"<suffix> <cmd> <out_suffix> \
Add for the given prefix the given pretty-printer, \
the new file as the given out_suffix. cmd must contain '%i' which will be \
replace by the input file and '%o' which will be replaced by the output file.") ::
"<suffix> <cmd> <out_suffix> declares a pretty-printer for edited proofs") ::
("--coqdoc",
Arg.Unit (fun ()->
opt_pp := (".v",("coqdoc --no-index --html -o %o %i",".html"))::!opt_pp),
" same as '--add_pp .v \"coqdoc --no-index --html -o %o %i\" .html'") ::
" use coqdoc to print Coq proofs") ::
common_options
open Session
......
......@@ -38,18 +38,17 @@ let opt_print0 = ref false
let spec =
("--provers", Arg.Set opt_print_provers,
" the prover used in the session are listed" ) ::
" provers used in the session" ) ::
("--edited-files", Arg.Set opt_print_edited,
" the edited files used in the session are listed" ) ::
" edited proof scripts in the session" ) ::
("--stats", Arg.Set opt_stats_print,
" prints provers statistics" ) ::
" prints various proofs statistics" ) ::
("--tree", Arg.Set opt_tree_print,
" the session is pretty printed in an ascii tree format" ) ::
" session contents as a tree in textual format" ) ::
("--dir", Arg.Set opt_project_dir,
" print the directory of the session" ) ::
" prints the directory of the session" ) ::
("--print0", Arg.Set opt_print0,
" use the null character instead of newline to separate the output of \
--provers and --edited-files" ) ::
" use the null character instead of newline" ) ::
common_options
......@@ -249,7 +248,7 @@ let run () =
let cmd =
{ cmd_spec = spec;
cmd_desc = "print informations about session.";
cmd_desc = "print informations and statistics about a session.";
cmd_name = "info";
cmd_run = run;
}
......
......@@ -35,10 +35,10 @@ let spec =
"<n> sets output style (1 or 2, default 1)") ::
("-o",
Arg.Set_string opt_output_dir,
" <path> where to produce LaTeX files (default: session dir)") ::
"<path> where to produce LaTeX files (default: session dir)") ::
("-longtable",
Arg.Set opt_longtable,
" produce tables using longtable package instead of tabular") ::
" use 'longtable' environment instead of 'tabular'") ::
common_options
......
......@@ -56,16 +56,16 @@ let opt_extra = ref []
let common_options = [
"-C", Arg.String (fun s -> opt_config := Some s),
"<file> Read configuration from <file>";
"<file> reads configuration from <file>";
"--config", Arg.String (fun s -> opt_config := Some s),
" same as -C";
"<file> same as -C";
"--extra-config", Arg.String (fun s -> opt_extra := !opt_extra @ [s]),
"<file> Read additional configuration from <file>";
"<file> reads additional configuration from <file>";
"-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
"<dir> Add <dir> to the library search path";
"<dir> adds <dir> to the library search path";
"--library", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
" same as -L";
"-v", Arg.Set opt_version, " print version information" ;
"<dir> same as -L";
"-v", Arg.Set opt_version, " prints version information" ;
Debug.Opt.desc_debug_list;
Debug.Opt.desc_debug_all;
Debug.Opt.desc_debug;
......
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