Commit 16f0445d authored by MARCHE Claude's avatar MARCHE Claude

why3session html: output as a table by default

parent e23285f7
% \newcommand{\todo}[1]{{\Huge\bfseries TODO: #1}}
\newcommand{\todo}[1]{{\Huge\bfseries TODO: #1}}
\newcommand{\why}{\textsf{Why3}\xspace}
\newcommand{\whyml}{\textsf{Why3ML}\xspace}
......
......@@ -100,7 +100,8 @@ make byte opt
make install_lib
\end{verbatim}
\section{Installation of external provers}\label{provers}
\section{Installation of external provers}
\label{provers}
\why can use a wide range of external theorem provers. These need to
be installed separately, and then \why needs to be configured to use
......@@ -268,6 +269,8 @@ the actions of the various menus and buttons of the interface.
\item[-I] $d$: adds $d$ in the load path, to search for theories.
\end{description}
\todo{option -extra-config and others}
\subsection{Left toolbar actions}
\begin{description}
......@@ -372,6 +375,8 @@ is the directory of the project.
The XML file follows the DTD given in \texttt{share/why3session.dtd} and reproduced below.
\verbatiminput{../share/why3session.dtd}
\todo{The DTD is certainly outdated}
\section{The \texttt{why3ml} tool}
The \texttt{why3ml} tool is a layer on top of the \why library for
......@@ -509,16 +514,10 @@ to use the IDE to update it.
some proofs did not replay correctly.
\item Option \texttt{-smoke-detector \{none|top|deep\}} tries to detect
if the context is self-contradicting.
\item Option \texttt{-latex \textsl{<dir>}} produces 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>}} produces an 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}
\paragraph{Smoke Detector}
The smoke detector tries to detect if the context is self-contradicting
and, thus, that anything can be proved in this context. The smoke
detector can't be run on outdated session and does not modify the session.
......@@ -552,31 +551,6 @@ detector has been triggered, or \texttt{No smoke detected} (exit code 0)
otherwise.
\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{why3session} tool}
\label{sec:why3session}
......@@ -688,9 +662,55 @@ 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}
\todo{THIS SECTION IS OUTDATED}
\begin{figure}[t]
\begin{verbatim}
......
......@@ -58,8 +58,11 @@
\vfill
\todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
\begin{LARGE}
Version \whyversion{}, October 2011
Version \whyversion{}, \todo{October 2011}
\end{LARGE}
\vfill
......@@ -83,7 +86,7 @@ $^2$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893
\bigskip
\textcopyright 2010-2011 Univ Paris-Sud, CNRS, INRIA
\textcopyright 2010-2012 Univ Paris-Sud, CNRS, INRIA
This work has been partly supported by the `U3CAT' national ANR project
(ANR-08-SEGI-021-08, \url{http://frama-c.cea.fr/u3cat}) and by the
......
......@@ -42,7 +42,7 @@ let print_usage () =
(Pp.print_iter1 Array.iter Pp.newline
(fun fmt e -> fprintf fmt "%s @[<hov>%s@]"
(Util.padd_string ' ' e.cmd_name maxl) e.cmd_desc)) cmds;
Arg.usage (Arg.align Why3session_lib.env_spec) "common options:";
Arg.usage (Arg.align Why3session_lib.common_options) "common options:";
eprintf "@\nspecific command options: %s <command> -help@." exec_name;
exit 1
......
......@@ -81,7 +81,7 @@ let spec =
"-c", Arg.Unit (set_replace Not_valid), " same as --conservative";
"--never", Arg.Unit (set_replace Never), " never replace a proof";
"-n", Arg.Unit (set_replace Never), " same as --never"]@
(force_obsolete_spec @ filter_spec @ env_spec)
(force_obsolete_spec @ filter_spec @ common_options)
type action =
| Copy
......
......@@ -21,17 +21,24 @@ open Format
open Why3
open Why3session_lib
module S = Session
let output_dir = ref ""
let opt_context = ref false
type style = Simple | Jstree
type style = SimpleTree | Jstree | Table
let opt_style = ref Simple
let opt_style = ref Table
let default_style = "table"
let set_opt_style = function
| "simple" -> opt_style := Simple
| "simple" -> opt_style := SimpleTree
| "jstree" -> opt_style := Jstree
| _ -> assert false
| "table" -> opt_style := Table
| _ ->
eprintf "Unknown html style, ignored@."
let () = set_opt_style default_style
let opt_pp = ref []
......@@ -50,9 +57,11 @@ let spec =
" 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") ::
("--style", Arg.Symbol (["simple";"jstree"], set_opt_style),
" Set the style to use. 'simple' use only 'ul' and 'il' tag. 'jstree' use \
the 'jstree' plugin of the javascript library 'jquery'.") ::
("--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'." *)
) ::
("--add_pp", Arg.Tuple
[Arg.String set_opt_pp_in;
Arg.String set_opt_pp_cmd;
......@@ -65,7 +74,7 @@ replace by the input file and '%o' which will be replaced by the output file.")
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'") ::
simple_spec
common_options
(*
let version_msg = sprintf
......@@ -141,6 +150,144 @@ let run_file (context : context) print_session fname =
if output_dir <> "-" then close_out cout
module Table =
struct
let rec transf_depth tr =
List.fold_left
(fun depth g -> max depth (goal_depth g)) 0 tr.S.transf_goals
and goal_depth g =
S.PHstr.fold
(fun _st tr depth -> max depth (1 + transf_depth tr))
g.S.goal_transformations 1
let theory_depth t =
List.fold_left
(fun depth g -> max depth (goal_depth g)) 0 t.S.theory_goals
let rec provers_stats provers theory =
S.theory_iter_proof_attempt (fun a ->
Hashtbl.replace provers a.S.proof_prover a.S.proof_prover) theory
let print_prover = Whyconf.print_prover
let color_of_status ?(dark=false) fmt b =
fprintf fmt "%s" (if b then
if dark then "008000" else "C0FFC0"
else "FF0000")
let print_results fmt provers proofs =
List.iter (fun p ->
fprintf fmt "<td bgcolor=\"#";
begin
try
let pr = S.PHprover.find proofs p in
let s = pr.S.proof_state in
match s with
| S.Done res ->
begin
match res.Call_provers.pr_answer with
| Call_provers.Valid ->
fprintf fmt "C0FFC0\">%.2f" res.Call_provers.pr_time
| Call_provers.Invalid ->
fprintf fmt "FF0000\">Invalid"
| Call_provers.Timeout ->
fprintf fmt "FF8000\">Timeout"
| Call_provers.Unknown _ ->
fprintf fmt "FF8000\">Unknown"
| _ ->
fprintf fmt "Failure "
end
| _ -> fprintf fmt "Undone"
with Not_found -> fprintf fmt "E0E0E0\">"
end;
fprintf fmt "</td>") provers
let rec print_transf fmt depth max_depth provers tr =
fprintf fmt "<tr>";
for i=1 to 0 (* depth-1 *) do fprintf fmt "<td></td>" done;
fprintf fmt "<td bgcolor=\"#%a\">" (color_of_status ~dark:false) tr.S.transf_verified;
for i=1 to depth-1 do fprintf fmt "&nbsp;&nbsp;&nbsp;&nbsp;" done;
fprintf fmt "%s</td>" tr.transf_name;
for i=1 (* depth *) to (*max_depth - 1 + *) List.length provers do
fprintf fmt "<td bgcolor=\"#E0E0E0\"></td>"
done;
fprintf fmt "</tr>@\n";
List.iter
(print_goal fmt (depth+1) max_depth provers)
tr.transf_goals
and print_goal fmt depth max_depth provers g =
fprintf fmt "<tr>";
for i=1 to 0 (* depth-1 *) do fprintf fmt "<td></td>" done;
fprintf fmt "<td bgcolor=\"#%a\">" (color_of_status ~dark:false) g.S.goal_verified;
for i=1 to depth-1 do fprintf fmt "&nbsp;&nbsp;&nbsp;&nbsp;" done;
fprintf fmt "%s</td>" (S.goal_expl g);
(* for i=depth to max_depth-1 do fprintf fmt "<td></td>" done; *)
print_results fmt provers g.goal_external_proofs;
fprintf fmt "</tr>@\n";
PHstr.iter
(fun _ tr -> print_transf fmt depth max_depth provers tr)
g.goal_transformations
let print_theory fmt th =
let depth = theory_depth th in
if depth > 0 then
let provers = Hashtbl.create 9 in
provers_stats provers th;
let provers =
Hashtbl.fold (fun _ pr acc -> pr :: acc) provers []
in
let provers = List.sort Whyconf.Prover.compare provers in
let name = th.S.theory_name.Ident.id_string in
fprintf fmt "<h2><font color=\"#%a\">Theory \"%s\": %s</font></h2>@\n"
(color_of_status ~dark:true) th.S.theory_verified
name (if th.S.theory_verified then "fully verified" else "not fully verified")
;
(*
fprintf fmt "<table border=\"1\"><tr><td colspan=\"%d\">Obligations</td>" depth;
*)
fprintf fmt "<table border=\"1\"><tr><td>Obligations</td>";
List.iter
(fun pr -> fprintf fmt "<td text-rotation=\"90\">%a</td>" print_prover pr)
provers;
fprintf fmt "</td></tr>@\n";
List.iter (print_goal fmt 1 depth provers) th.theory_goals;
fprintf fmt "</table>@\n"
let print_file fmt f =
(* fprintf fmt "<h1>File %s</h1>@\n" f.file_name; *)
fprintf fmt "%a"
(Pp.print_list Pp.newline print_theory) f.file_theories
let print_session name fmt s =
fprintf fmt "<h1>Why3 Proof Results for Project \"%s\"</h1>@\n" name;
fprintf fmt "%a"
(Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing Pp.nothing
print_file) s.session_files
let context : context = "<!DOCTYPE html
PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"
\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">
<html xmlns=\"http://www.w3.org/1999/xhtml\">
<head>
<title>Why3 session of %s</title>
</head>
<body>
%a
</body>
</html>
"
let run_one = run_file context print_session
end
module Simple =
struct
......@@ -412,7 +559,8 @@ end
let run_one fname =
match !opt_style with
| Simple -> Simple.run_one fname
| Table -> Table.run_one fname
| SimpleTree -> Simple.run_one fname
| Jstree ->
eprintf "style jstree not yet available@.";
exit 1
......
......@@ -42,7 +42,7 @@ let spec =
("--print0", Arg.Set opt_print0,
" use the null character instead of newline to separate the output of \
--provers and --edited-files" ) ::
simple_spec
common_options
let run_one fname =
let project_dir = Session.get_project_dir fname in
......
......@@ -39,7 +39,7 @@ let spec =
("-longtable",
Arg.Set opt_longtable,
" produce tables using longtable package instead of tabular") ::
env_spec
common_options
(* Statistics in LaTeX*)
......
......@@ -41,13 +41,6 @@ let print_version () =
Format.printf "Why3 session, version %s (build date: %s)@."
Config.version Config.builddate
let simple_spec = [
("-v", Arg.Set opt_version, " print version information") ;
Debug.Opt.desc_debug_list;
Debug.Opt.desc_debug_all;
Debug.Opt.desc_debug;
]
let read_simple_spec () =
if !opt_version then begin
print_version (); exit 0
......@@ -73,9 +66,13 @@ let common_options = [
"<dir> Add <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" ;
Debug.Opt.desc_debug_list;
Debug.Opt.desc_debug_all;
Debug.Opt.desc_debug;
]
let env_spec = common_options @ simple_spec
let env_spec = common_options
let read_env_spec () =
......
......@@ -41,14 +41,13 @@ val print_version : unit -> unit
(** {2 Spec for version, debug} *)
val simple_spec : spec_list
(* val simple_spec : spec_list *)
val read_simple_spec : unit -> bool
val read_simple_spec : unit -> bool
(** return if we must exit *)
(** {2 Spec for configuratio, loadpath} *)
val env_spec : spec_list
(** include simple_spec *)
(** {2 Spec for configuration, loadpath} *)
val common_options : spec_list
val read_env_spec : unit -> Env.env * Whyconf.config * bool
(** read_simple_spec also *)
......
......@@ -55,7 +55,7 @@ associated to proved goals (same as --filter-verified-goal --conservative)")::
(* ("--never", Arg.Unit (set_remove Never),
" never remove a proof")::
("-n", Arg.Unit (set_remove Never), " same as --never")::*)
(filter_spec @ env_spec)
(filter_spec @ common_options)
let rec interactive to_remove =
eprintf "Do you want to remove the external proof %a (y/n)@."
......
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