Commit 893110f2 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

latex output moved to why3session tool

parent b6175e0a
......@@ -668,8 +668,8 @@ install_local: bin/why3replayer
# Session
###############
SESSION_FILES = why3session_lib why3session_copy why3session_info \
why3session_rm why3session
SESSION_FILES = why3session_lib why3session_copy why3session_info \
why3session_output why3session_rm why3session
SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))
......
......@@ -69,7 +69,7 @@ version_bad = "2.4"
version_ok = "2.2"
version_old = "2.1"
# we pass time 0 to why3-cpulimit to avoid race
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -timeout %t %f"
command = "@LOCALBIN@why3-cpulimit %T %m -s %e -timeout %t %f"
driver = "drivers/cvc3.drv"
[ATP yices]
......@@ -94,7 +94,7 @@ version_switch = "--version"
version_regexp = "E \\([-0-9.]+\\) [^\n]+"
version_ok = "1.4"
# we pass time 0 to why3-cpulimit to avoid race
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
command = "@LOCALBIN@why3-cpulimit %T %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
driver = "drivers/tptp.drv"
[ATP gappa]
......@@ -136,7 +136,7 @@ version_switch = "-TPTP || true"
version_regexp = "SPASS V \\([^ \n\t]+\\)"
version_ok = "3.7"
# we pass time 0 to why3-cpulimit to avoid race
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
command = "@LOCALBIN@why3-cpulimit %T %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
driver = "drivers/tptp.drv"
[ATP vampire]
......@@ -145,7 +145,7 @@ exec = "vampire"
version_switch = "--version"
version_regexp = "Vampire \\([0-9.]+\\)"
# we pass time 0 to why3-cpulimit to avoid race
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -t %t"
command = "@LOCALBIN@why3-cpulimit %T %m -s %e -t %t"
driver = "drivers/vampire.drv"
version_ok = "0.6"
......
......@@ -126,6 +126,7 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
| "%" -> "%"
| "f" -> fin
| "t" -> on_timelimit := true; string_of_int timelimit
| "T" -> string_of_int (16 * succ timelimit)
| "m" -> string_of_int memlimit
(* FIXME: libdir and datadir can be changed in the configuration file
Should we pass them as additional arguments? Or would it be better
......
......@@ -21,15 +21,11 @@
open Format
open Why3
module S = Session
module C = Whyconf
let includes = ref []
let file = ref None
let opt_version = ref false
let opt_stats = ref true
let opt_latex = ref ""
let opt_latex2 = ref ""
let opt_longtable = ref false
let opt_force = ref false
let opt_convert_unknown_provers = ref false
......@@ -82,15 +78,6 @@ let spec = Arg.align [
("-v",
Arg.Set opt_version,
" print version information") ;
("-latex",
Arg.Set_string opt_latex,
" [Dir_output] produce latex statistics") ;
("-latex2",
Arg.Set_string opt_latex2,
" [Dir_output] produce latex statistics") ;
("-longtable",
Arg.Set opt_longtable,
" produce latex statistics using longtable package") ;
"--convert-unknown-provers", Arg.Set opt_convert_unknown_provers,
" try to find compatible provers for all unknown provers";
Debug.Opt.desc_debug_list;
......@@ -272,251 +259,9 @@ let print_statistics files =
in
List.iter print_file (List.rev files)
(* Statistics in LaTeX*)
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 0
let theory_depth t =
List.fold_left (fun depth g -> max depth (goal_depth g)) 0 t.S.theory_goals
let rec provers_latex_stats provers theory =
S.theory_iter_proof_attempt (fun a ->
Hashtbl.replace provers a.S.proof_prover a.S.proof_prover) theory
let protect s =
let b = Buffer.create 7 in
for i = 0 to String.length s - 1 do
match s.[i] with
'_' -> Buffer.add_string b "\\_"
| c -> Buffer.add_char b c
done;
Buffer.contents b
let column n depth provers =
if n == 1 then
if depth > 1 then
(List.length provers) + depth
else
(List.length provers) + depth + 1
else
(List.length provers) + 1
let print_result_prov proofs prov fmt=
List.iter (fun p ->
try
let pr = S.PHprover.find proofs p in
let s = pr.S.proof_state in
match s with
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.Unknown _s -> fprintf fmt "& \\unknown "
| _ -> fprintf fmt "& \\failure "
end
| _ -> fprintf fmt "& Undone"
with Not_found -> fprintf fmt "& \\noresult") prov;
fprintf fmt "\\\\ @."
let rec goal_latex_stat fmt prov depth depth_max subgoal g =
let column = column 1 depth prov
in
if depth > 0 then
if subgoal > 0 then
fprintf fmt "\\cline{%d-%d} @." (depth + 1) column
else ()
else
fprintf fmt "\\hline @.";
if depth_max > 1 then
begin
if subgoal > 0 then
begin
if(depth < depth_max) then
for i = 1 to depth do
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
done
else
for i = 1 to depth - 1 do
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
done
end
else
if(depth < depth_max) then
if depth > 0 then
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
end
else
begin
if subgoal > 0 then
for i = 1 to depth do
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " " done
else
if depth > 0 then
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
end;
if (depth <= 1) then
fprintf fmt "\\explanation{%s} " (protect (S.goal_expl g))
else
fprintf fmt "\\explanation{%s}" " ";
let proofs = g.S.goal_external_proofs in
if (S.PHprover.length proofs) > 0 then
begin
if depth_max <= 1 then
begin
if depth > 0 then
for i = depth to (depth_max - depth) do
fprintf fmt "& \\explanation{%s}" " " done
else
for i = depth to (depth_max - depth - 1) do
fprintf fmt "& \\explanation{%s}" " " done
end
else
if depth > 0 then
for i = depth to (depth_max - depth - 1) do
fprintf fmt "& \\explanation{%s}" " " done
else
for i = depth to (depth_max - depth - 2) do
fprintf fmt "& \\explanation{%s}" " " done;
print_result_prov proofs prov fmt;
end;
let tr = g.S.goal_transformations in
if S.PHstr.length tr > 0 then
if S.PHprover.length proofs > 0 then
fprintf fmt "\\cline{%d-%d} @." (depth + 2) column;
S.PHstr.iter (fun _st tr ->
let goals = tr.S.transf_goals in
let _ = List.fold_left (fun subgoal g ->
goal_latex_stat fmt prov (depth + 1) depth_max (subgoal) g;
subgoal + 1) 0 goals in
() ) tr
let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
let column = column 2 depth prov
in
if depth > 0 then
fprintf fmt "\\cline{%d-%d} @." 2 column
else
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))
else
fprintf fmt "\\explanation{%d} " (subgoal + 1);
let proofs = g.S.goal_external_proofs in
if (S.PHprover.length proofs) > 0 then
print_result_prov proofs prov fmt;
let tr = g.S.goal_transformations in
if S.PHstr.length tr > 0 then
begin
if (S.PHprover.length proofs == 0) then
fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @."
(List.length prov);
S.PHstr.iter (fun _st tr ->
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;
subgoal + 1) 0 goals in
() ) tr
end
else
if (S.PHprover.length proofs) == 0 then
fprintf fmt "\\\\ @."
let print_head n depth provers fmt =
if n == 1 then
if (depth > 1) then
fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } "
depth
else
fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } "
(depth + 1)
else
fprintf fmt "\\hline Proof obligations ";
List.iter (fun a -> fprintf fmt "& \\provername{%a} " C.print_prover a)
provers;
fprintf fmt "\\\\ @."
let latex_tabular n fmt depth provers t =
fprintf fmt "\\begin{tabular}";
fprintf fmt "{| l |";
for i = 0 to (List.length provers) + depth do fprintf fmt "c |" done;
fprintf fmt "}@.";
print_head n depth provers fmt;
if n == 1 then
List.iter (goal_latex_stat fmt provers 0 depth 0) t.S.theory_goals
else
List.iter (goal_latex2_stat fmt provers 0 depth 0) t.S.theory_goals;
fprintf fmt "\\hline \\end{tabular}@."
let latex_longtable n fmt depth name provers t=
fprintf fmt "\\begin{longtable}";
fprintf fmt "{| l |";
for i = 0 to (List.length provers) + depth do fprintf fmt "c |" done;
fprintf fmt "}@.";
(** First head *)
print_head n depth provers fmt;
fprintf fmt "\\hline \\endfirsthead @.";
(** Other heads : "Continued... " added *)
fprintf fmt "\\multicolumn{%d}{r}{\\textit{Continued from previous page}} \
\\\\ @." (List.length provers + 1) ;
fprintf fmt "\\hline @.";
print_head n depth provers fmt;
fprintf fmt "\\hline \\endhead @.";
(** Other foots : "Continued..." added *)
fprintf fmt "\\hline \\multicolumn{%d}{r}{\\textit{Continued on next page}} \
\\\\ @." (List.length provers);
(** Last foot : nothing *)
fprintf fmt "\\endfoot \\endlastfoot @.";
if n == 1 then
List.iter (goal_latex_stat fmt provers 0 depth 0) t.S.theory_goals
else
List.iter (goal_latex2_stat fmt provers 0 depth 0) t.S.theory_goals;
fprintf fmt "\\hline \\caption{%s statistics} @." (protect name);
fprintf fmt "\\label{%s} \\end{longtable}@." (protect name)
let theory_latex_stat n table dir t =
let provers = Hashtbl.create 9 in
provers_latex_stats provers t;
let provers = Hashtbl.fold (fun _ pr acc -> pr :: acc)
provers [] in
let provers = List.sort C.Prover.compare provers in
let depth = theory_depth t in
let name = t.S.theory_name.Ident.id_string in
let ch = open_out (Filename.concat dir(name^".tex")) in
let fmt = formatter_of_out_channel ch in
if table = "tabular" then
begin
latex_tabular n fmt depth provers t
end
else
latex_longtable n fmt depth name provers t;
close_out ch
let file_latex_stat n table dir f =
List.iter (theory_latex_stat n table dir) f.S.file_theories
let print_latex_statistics n table dir session =
let files = session.S.session_files in
S.PHstr.iter (fun _ f -> file_latex_stat n table dir f) files
let print_report (g,p,r) =
printf " goal '%s', prover '%a': " g.Ident.id_string C.print_prover p;
printf " goal '%s', prover '%a': " g.Ident.id_string Whyconf.print_prover p;
match r with
| M.Result(new_res,old_res) ->
(* begin match !opt_smoke with *)
......@@ -644,32 +389,10 @@ let () =
end;
(* M.smoke_detector := !opt_smoke; *)
eprintf " done.";
if !opt_longtable && !opt_latex == "" && !opt_latex2 == "" then
begin
eprintf
"[Error] I can't use option longtable without latex ou latex2@.";
exit 1
end;
if !opt_latex <> "" then
if !opt_longtable then
print_latex_statistics 1 "longtable" !opt_latex
env_session.S.session
else
print_latex_statistics 1 "tabular" !opt_latex
env_session.S.session
else
if !opt_latex2 <> "" then
if !opt_longtable then
print_latex_statistics 2 "longtable" !opt_latex2
env_session.S.session
else
print_latex_statistics 2 "tabular" !opt_latex2
env_session.S.session
else
begin
add_to_check found_obs env_session sched;
main_loop (); eprintf "main replayer exited unexpectedly@."; exit 1
end
add_to_check found_obs env_session sched;
main_loop ();
eprintf "main replayer exited unexpectedly@.";
exit 1
with
| S.OutdatedSession ->
eprintf "The session database '%s' is outdated, cannot replay@."
......
......@@ -28,6 +28,7 @@ let cmds =
Why3session_copy.cmd_archive;
Why3session_info.cmd;
Why3session_rm.cmd;
Why3session_output.cmd;
|]
let usage = "why3session cmd [opts]"
......
......@@ -21,6 +21,7 @@ open Why3
open Why3session_lib
open Whyconf
open Format
module S = Session
let opt_print_provers = ref false
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Why3
open Why3session_lib
open Whyconf
open Format
module S = Session
let opt_latex = ref ""
let opt_latex2 = ref ""
let opt_longtable = ref false
let spec =
("-latex",
Arg.Set_string opt_latex,
" [Dir_output] produce latex statistics") ::
("-latex2",
Arg.Set_string opt_latex2,
" [Dir_output] produce latex statistics") ::
("-longtable",
Arg.Set opt_longtable,
" produce latex statistics using longtable package") ::
simple_spec
(* Statistics in LaTeX*)
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 0
let theory_depth t =
List.fold_left (fun depth g -> max depth (goal_depth g)) 0 t.S.theory_goals
let rec provers_latex_stats provers theory =
S.theory_iter_proof_attempt (fun a ->
Hashtbl.replace provers a.S.proof_prover a.S.proof_prover) theory
let protect s =
let b = Buffer.create 7 in
for i = 0 to String.length s - 1 do
match s.[i] with
'_' -> Buffer.add_string b "\\_"
| c -> Buffer.add_char b c
done;
Buffer.contents b
let column n depth provers =
if n == 1 then
if depth > 1 then
(List.length provers) + depth
else
(List.length provers) + depth + 1
else
(List.length provers) + 1
let print_result_prov proofs prov fmt=
List.iter (fun p ->
try
let pr = S.PHprover.find proofs p in
let s = pr.S.proof_state in
match s with
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.Unknown _s -> fprintf fmt "& \\unknown "
| _ -> fprintf fmt "& \\failure "
end
| _ -> fprintf fmt "& Undone"
with Not_found -> fprintf fmt "& \\noresult") prov;
fprintf fmt "\\\\ @."
let rec goal_latex_stat fmt prov depth depth_max subgoal g =
let column = column 1 depth prov
in
if depth > 0 then
if subgoal > 0 then
fprintf fmt "\\cline{%d-%d} @." (depth + 1) column
else ()
else
fprintf fmt "\\hline @.";
if depth_max > 1 then
begin
if subgoal > 0 then
begin
if(depth < depth_max) then
for i = 1 to depth do
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
done
else
for i = 1 to depth - 1 do
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
done
end
else
if(depth < depth_max) then
if depth > 0 then
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
end
else
begin
if subgoal > 0 then
for i = 1 to depth do
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " " done
else
if depth > 0 then
fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
end;
if (depth <= 1) then
fprintf fmt "\\explanation{%s} " (protect (S.goal_expl g))
else
fprintf fmt "\\explanation{%s}" " ";
let proofs = g.S.goal_external_proofs in
if (S.PHprover.length proofs) > 0 then
begin
if depth_max <= 1 then
begin
if depth > 0 then
for i = depth to (depth_max - depth) do
fprintf fmt "& \\explanation{%s}" " " done
else
for i = depth to (depth_max - depth - 1) do
fprintf fmt "& \\explanation{%s}" " " done
end
else
if depth > 0 then
for i = depth to (depth_max - depth - 1) do
fprintf fmt "& \\explanation{%s}" " " done
else
for i = depth to (depth_max - depth - 2) do
fprintf fmt "& \\explanation{%s}" " " done;
print_result_prov proofs prov fmt;
end;
let tr = g.S.goal_transformations in
if S.PHstr.length tr > 0 then
if S.PHprover.length proofs > 0 then
fprintf fmt "\\cline{%d-%d} @." (depth + 2) column;
S.PHstr.iter (fun _st tr ->
let goals = tr.S.transf_goals in
let _ = List.fold_left (fun subgoal g ->
goal_latex_stat fmt prov (depth + 1) depth_max (subgoal) g;
subgoal + 1) 0 goals in
() ) tr
let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
let column = column 2 depth prov
in
if depth > 0 then
fprintf fmt "\\cline{%d-%d} @." 2 column
else
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))
else
fprintf fmt "\\explanation{%d} " (subgoal + 1);
let proofs = g.S.goal_external_proofs in
if (S.PHprover.length proofs) > 0 then
print_result_prov proofs prov fmt;
let tr = g.S.goal_transformations in
if S.PHstr.length tr > 0 then
begin
if (S.PHprover.length proofs == 0) then
fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @."
(List.length prov);
S.PHstr.iter (fun _st tr ->
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;
subgoal + 1) 0 goals in
() ) tr
end
else
if (S.PHprover.length proofs) == 0 then
fprintf fmt "\\\\ @."
let print_head n depth provers fmt =
if n == 1 then
if (depth > 1) then
fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } "