Commit 6188733d authored by Claude Marche's avatar Claude Marche

improved why3session latex

parent 1af367a5
......@@ -143,13 +143,15 @@ Provers support:
o support for iProver and Zenon
Misc:
o [replayer] new option -q
o improved output of "why3session latex"
(incompatible changes in LaTeX macos)
o [replayer] new option -q for running quietly
o a warning is emitted for unused bound logic variables in "forall",
"exists" and "let"
o a warning is emitted for any occurrence of a formula of the form
"exists x, P -> Q". Formulas of this form are usually a user
mistake. If this is intended, one can write "exists x, not P \/ Q"
instead
instead
Bug fixes:
o fixed bug on merging config files which prevented the use
......
\begin{tabular}{| l |c |c |c |c |c |}
\hline \multicolumn{2}{|c|}{Proof obligations } & \provername{Alt-Ergo (0.93)} & \provername{Coq (8.3pl3)} & \provername{Simplify (1.5.4)} \\
\hline \multicolumn{2}{|c|}{Proof obligations } & \provername{Alt-Ergo (0.94)} & \provername{Coq (8.3pl4)} & \provername{Simplify (1.5.4)} \\
\hline
\explanation{G1} & \explanation{ }& \noresult& \noresult& \valid{0.01} \\
\explanation{G1} & \explanation{ }& \noresult& \noresult& \valid{0.00} \\
\hline
\explanation{G2} & \explanation{ }& \unknown & \noresult& \unknown \\
\explanation{G2} & \explanation{ }& \unknown{0.00} & \noresult& \unknown{0.00} \\
\cline{2-4}
\explanation{ }& \explanation{ }\explanation{G2.0} & \unknown & \unknown & \unknown \\
\explanation{ }& \explanation{ }\explanation{G2.1} & \unknown{0.00} & \unknown{0.49} & \unknown{0.00} \\
\cline{2-5}
\explanation{ }& \explanation{ }\explanation{G2.1} & \valid{0.02} & \noresult& \valid{0.01} \\
\explanation{ }& \explanation{ }\explanation{G2.2} & \valid{0.00} & \noresult& \valid{0.00} \\
\hline
\explanation{G3} & \explanation{ }& \valid{0.02} & \noresult& \unknown \\
\explanation{G3} & \explanation{ }& \valid{0.00} & \noresult& \unknown{0.00} \\
\hline \end{tabular}
......@@ -783,6 +783,8 @@ output.
\label{fig:custom-latex}
\end{figure}
\todo{rejouer HelloProofs, pour eviter tout ces 0.00, et qu'en plus
cela soit coherent avec la sortie HTML ci-dessous}
\begin{figure}[t]
\begin{center}
\begin{toimage}
......
\usepackage{xcolor}
\usepackage{colortbl}
\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}?}
\newcommand{\unknown}[1]{\cellcolor{red!20}#1}
\newcommand{\invalid}[1]{\cellcolor{red!50}#1}
\newcommand{\timeout}[1]{\cellcolor{red!20}(#1)}
\newcommand{\outofmemory}[1]{\cellcolor{red!20}(#1)}
\newcommand{\noresult}{\multicolumn{1}{>{\columncolor[gray]{0.8}}c|}{~}}
\newcommand{\failure}{\cellcolor{red!20}failure}
\newcommand{\highfailure}{\cellcolor{red!50}FAILURE}
......@@ -698,7 +698,7 @@ let general_settings (c : t) (notebook:GPack.notebook) =
in
let showtimelimit =
GButton.check_button
~label:"show time limit for each proof"
~label:"show time and memory limits for each proof"
~packing:display_options_box#add ()
~active:c.show_time_limit
in
......
......@@ -134,14 +134,20 @@ let print_result_prov proofs prov fmt=
| Session.Done res ->
begin
match res.Call_provers.pr_answer with
Call_provers.Valid ->
fprintf fmt "& \\valid{%.2f} " res.Call_provers.pr_time
| Call_provers.Invalid -> fprintf fmt "& \\invalid "
| Call_provers.Timeout -> fprintf fmt "& \\timeout "
| Call_provers.OutOfMemory -> fprintf fmt "& \\outofmemory "
| Call_provers.Unknown _ -> fprintf fmt "& \\unknown "
| Call_provers.Failure _ -> fprintf fmt "& \\failure "
| Call_provers.HighFailure -> fprintf fmt "& \\highfailure "
| Call_provers.Valid ->
fprintf fmt "& \\valid{%.2f} " res.Call_provers.pr_time
| Call_provers.Invalid ->
fprintf fmt "& \\invalid{%.2f} " res.Call_provers.pr_time
| Call_provers.Timeout ->
fprintf fmt "& \\timeout{%ds} " pr.S.proof_timelimit
| Call_provers.OutOfMemory ->
fprintf fmt "& \\outofmemory{%dM} " pr.S.proof_memlimit
| Call_provers.Unknown _ ->
fprintf fmt "& \\unknown{%.2f} " res.Call_provers.pr_time
| Call_provers.Failure _ ->
fprintf fmt "& \\failure "
| Call_provers.HighFailure ->
fprintf fmt "& \\highfailure "
end
| Session.InternalFailure _ -> fprintf fmt "& Internal Failure"
......@@ -226,7 +232,7 @@ let rec goal_latex_stat fmt prov depth depth_max subgoal g =
() ) tr
let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
let style_2_row fmt depth prov subgoal expl=
let column = column 2 depth prov in
if depth > 0 then
fprintf fmt "\\cline{%d-%d} @." 2 column
......@@ -234,9 +240,12 @@ let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
fprintf fmt "\\hline @.";
for _i = 1 to depth do fprintf fmt "\\quad" done;
if (depth <= 1) then
fprintf fmt "\\explanation{%s} " (protect (S.goal_expl g))
fprintf fmt "\\explanation{%s} " expl
else
fprintf fmt "\\explanation{%d} " (subgoal + 1);
fprintf fmt "\\explanation{%d} " (subgoal + 1)
let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
style_2_row fmt depth prov subgoal (protect (S.goal_expl g));
let proofs = g.S.goal_external_proofs in
if (S.PHprover.length proofs) > 0 then
print_result_prov proofs prov fmt;
......@@ -247,6 +256,9 @@ let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @."
(List.length prov);
S.PHstr.iter (fun _st tr ->
style_2_row fmt depth prov subgoal (protect tr.S.transf_name);
fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @."
(List.length prov);
let goals = tr.S.transf_goals in
let _ = List.fold_left (fun subgoal g ->
goal_latex2_stat fmt prov (depth + 1) depth_max (subgoal) g;
......
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