Commit e0279f0b authored by François Bobot's avatar François Bobot

[why3session] merge the option hist of why3session info and why3session csv --valid-by-time

              rename options of why3session csv
parent f83677ba
......@@ -21,10 +21,11 @@ version 0.82, December 9, 2013
o new version of prover: SPASS 3.8ds
o new version of prover: veriT (201310)
o API: more examples of use in examples/use_api/
o why3session new option --hist for histograms
o why3session csv can create graph with option --gnuplot [png|svg|pdf|qt]
o shape algorithm modified (see VSTTE'13 paper) but is
backward compatible thanks to shape_version numbers in
why3session.xml files
* options name and default of why3session csv changed
* [emacs] why.el renamed to why3.el
* [GTK sourceview] why.lang renamed to why3.lang
* Loc.try[1-7] functions now take location as an optional parameter
......
......@@ -16,10 +16,13 @@ open Format
module Hprover = Whyconf.Hprover
module S = Session
let opt_output_dir = ref ""
let orig_dir = Sys.getcwd ()
let opt_output_dir = ref "./"
let opt_provers = ref []
let opt_aggregate = ref false
let opt_print_csv = ref false
let simple_read_opt_prover s =
try
......@@ -31,49 +34,49 @@ let simple_read_opt_prover s =
let opt_value_not_valid = ref "-1."
let opt_gnuplot = false
type style =
| Normal
| By_Time
let opt_style = ref Normal
let set_style s =
match s with
| "normal" -> opt_style := Normal
| "by_time" -> opt_style := By_Time
| _ -> assert false
(* TODO *)
let print_gnuplot =
"set datafile separator \",\"
set key autotitle columnhead
set term png
set logscale xy 10
set object rectangle from screen 0,0 to screen 1,1 behind
set output \"%s\"
set xlabel \"%a\"
max(x,y) = x > y ? x : y
plot \"aggregate.csv\" using (max($4,0.001)):(max($3,0.001))
"
type gnuplot =
| PDF
| PNG
| SVG
| QT
| GP
let opt_gnuplot = ref []
let select_gnuplot = function
| "pdf" -> opt_gnuplot := PDF::!opt_gnuplot
| "png" -> opt_gnuplot := PNG::!opt_gnuplot
| "svg" -> opt_gnuplot := SVG::!opt_gnuplot
| "qt" -> opt_gnuplot := QT::!opt_gnuplot
| "gp" -> opt_gnuplot := GP::!opt_gnuplot
| _ -> assert false (** absurd: Arg already filtered bad cases *)
let opt_data = ref false
let opt_by_time = ref false
let spec =
("-o",
Arg.Set_string opt_output_dir,
"<dir> where to produce LaTeX files (default: session dir)") ::
"<dir> where to produce files (default: session dir)") ::
("--filter-prover",
Arg.String (fun s ->
opt_provers := (simple_read_opt_prover s)::!opt_provers),
" select the provers")::
("--data", Arg.Set opt_data,
"For all the goals give the time taken by each provers that proved it.")::
("--aggregate", Arg.Set opt_aggregate,
" aggregate all the input into one")::
" aggregate all the input into one file named \
aggregate_data.* and aggregate.*")::
("--value-not-valid", Arg.Set_string opt_value_not_valid,
" value used when the external proof is not valid")::
("--style", Arg.Symbol (["normal";"by_time"],set_style)," set the style")
:: (common_options)
" value used when the external proof is not valid (only for --data)")::
("--valid_by_time", Arg.Set opt_by_time,
"Give the evolution of the number of goal proved \
for each provers (default)")::
("--gnuplot", Arg.Symbol (["pdf";"png";"svg";"qt";"gp"],select_gnuplot),
"Run gnuplot on the produced file (currently only with --valid_by_time)\
(gp write the gnuplot script used for generating the other case)")::
("--output-csv", Arg.Set opt_print_csv,
"print the csv, set byt default when --gnuplot is not set")::
common_options
(** Normal *)
......@@ -117,7 +120,7 @@ let run_one_normal filter_provers fmt fname =
let run_normal dir filter_provers =
if !opt_aggregate then
let out = open_out (Filename.concat dir "aggregate.csv") in
let out = open_out (Filename.concat dir "aggregate_data.csv") in
let fmt = formatter_of_out_channel out in
Pp.wnl fmt;
iter_files (run_one_normal filter_provers fmt);
......@@ -126,7 +129,7 @@ let run_normal dir filter_provers =
iter_files (fun fname ->
let out = open_out
(Filename.concat dir
((try Filename.chop_extension fname with _ -> fname)^".csv")) in
((try Filename.chop_extension fname with _ -> fname)^"_data.csv")) in
let fmt = formatter_of_out_channel out in
Pp.wnl fmt;
run_one_normal filter_provers fmt fname;
......@@ -197,27 +200,123 @@ let print_provers_time (provers_time : float list Whyconf.Hprover.t) fmt =
print_line l end in
print_line l
let run_by_time dir filter_provers =
if !opt_aggregate then
let out = open_out (Filename.concat dir "aggregate.csv") in
let create_gnuplot_by_time nb_provers fmt =
Format.pp_print_string fmt
"\
set datafile separator \",\"\n\
set key autotitle columnhead\n\
set logscale x 10\n\
set object rectangle from screen 0,0 to screen 1,1 behind\n\
set xlabel \"time\"\n\
\n\
plot ";
for i=1 to nb_provers do
Format.fprintf fmt
"data_filename using ($1):($%i) with steps"
(i+1);
if i <> nb_provers then Format.pp_print_string fmt ",\\\n";
done
let print_file out f : unit =
let fmt = formatter_of_out_channel out in
Pp.wnl fmt;
let provers_time = Whyconf.Hprover.create 5 in
iter_files (run_one_by_time provers_time filter_provers);
print_provers_time provers_time fmt;
f fmt;
close_out out
let print_args fmt args =
(Pp.print_iter1 Array.iter
(fun fmt () -> Format.pp_print_string fmt " ") (** no @\n *)
(fun fmt -> Format.fprintf fmt "%S"))
fmt args
let call_gnuplot arg1 arg2 csv_file gp_file =
let args =
[| "gnuplot"; "-e"; arg1; "-e"; arg2;
"-e"; Printf.sprintf "data_filename = \"%s\"" (Opt.get csv_file);
Opt.get gp_file |] in
Debug.dprintf verbose "exec:%a@." print_args args;
let pid = Unix.create_process "gnuplot" args
Unix.stdin Unix.stdout Unix.stderr in
match Unix.waitpid [] pid with
| _, Unix.WEXITED 0 -> ()
| _ -> Format.eprintf "Command failed:%a@." print_args args
let run_by_time_gen dir canonical_name iter =
let to_remove = Stack.create () in
let canonical_name = Filename.concat dir canonical_name in
(** compute stats *)
let provers_time = Whyconf.Hprover.create 5 in
iter provers_time;
(** print .csv if necessary *)
let csv_file =
if !opt_gnuplot = [] || !opt_print_csv then
let fname = canonical_name ^ ".csv" in
print_file (open_out fname)
(fun fmt -> print_provers_time provers_time fmt);
Some fname
else if !opt_gnuplot <> [] then
let fname,ch = Filename.open_temp_file "why3session" ".csv" in
Stack.push fname to_remove;
print_file ch
(fun fmt -> print_provers_time provers_time fmt);
Some fname
else None
in
(** create .gp if necessary *)
let nb_provers = Whyconf.Hprover.length provers_time in
let gp_file =
if List.mem GP !opt_gnuplot
then let fname = canonical_name ^ ".gp" in
print_file (open_out fname)
(fun fmt -> create_gnuplot_by_time nb_provers fmt);
Some fname
else if !opt_gnuplot <> [] then
let fname,ch = Filename.open_temp_file "why3session" ".gp" in
Stack.push fname to_remove;
print_file ch
(fun fmt -> create_gnuplot_by_time nb_provers fmt);
Some fname
else None
in
(** output .png, .pdf, .csv and run .qt if necessary *)
if List.mem PNG !opt_gnuplot then
call_gnuplot
"set terminal pngcairo size 600, 400"
(Printf.sprintf "set output \"%s.png\"" canonical_name)
csv_file gp_file;
if List.mem PDF !opt_gnuplot then
call_gnuplot
"set terminal pdfcairo"
(Printf.sprintf "set output \"%s.pdf\"" canonical_name)
csv_file gp_file;
if List.mem SVG !opt_gnuplot then
call_gnuplot
"set terminal svg"
(Printf.sprintf "set output \"%s.svg\"" canonical_name)
csv_file gp_file;
if List.mem QT !opt_gnuplot then
call_gnuplot
"set terminal qt persist"
""
csv_file gp_file;
(** Clean up temporary files *)
Stack.iter Sys.remove to_remove
let run_by_time dir filter_provers =
if !opt_aggregate then
run_by_time_gen dir "aggregate.csv"
(fun provers_time ->
iter_files (run_one_by_time provers_time filter_provers))
else
iter_files (fun fname ->
let out = open_out
(Filename.concat dir
((try Filename.chop_extension fname with _ -> fname)^".csv")) in
let fmt = formatter_of_out_channel out in
Pp.wnl fmt;
let provers_time = Whyconf.Hprover.create 5 in
run_one_by_time provers_time filter_provers fname;
print_provers_time provers_time fmt;
close_out out)
run_by_time_gen dir (try Filename.chop_extension fname with _ -> fname)
(fun provers_time ->
run_one_by_time provers_time filter_provers fname)
)
(* Common *)
......@@ -226,14 +325,14 @@ let run () =
if should_exit1 then exit 1;
let filter_provers =
List.map (Whyconf.filter_prover_with_shortcut whyconf) !opt_provers in
let dir = !opt_output_dir in
match !opt_style with
| Normal -> run_normal dir filter_provers
| By_Time -> run_by_time dir filter_provers
let dir = Sysutil.absolutize_filename orig_dir (!opt_output_dir) in
if !opt_data then run_normal dir filter_provers;
if !opt_by_time || not (!opt_data) then run_by_time dir filter_provers
let cmd =
{ cmd_spec = spec;
cmd_desc = "output session as a table for simple processing.";
cmd_desc =
"output session as a table or graph for simple processing or viewing.";
cmd_name = "csv";
cmd_run = run;
}
......@@ -25,7 +25,6 @@ let opt_print_provers = ref false
let opt_print_edited = ref false
let opt_tree_print = ref false
let opt_stats_print = ref false
let opt_hist_print = ref false
let opt_project_dir = ref false
let opt_print0 = ref false
......@@ -36,8 +35,6 @@ let spec =
" edited proof scripts in the session" ) ::
("--stats", Arg.Set opt_stats_print,
" prints various proofs statistics" ) ::
("--hist", Arg.Set opt_hist_print,
" outputs a histogram of external proof results" ) ::
("--tree", Arg.Set opt_tree_print,
" session contents as a tree in textual format" ) ::
("--dir", Arg.Set opt_project_dir,
......@@ -55,7 +52,6 @@ type proof_stats =
mutable nb_proved_sub_goals : int;
mutable no_proof : Sstr.t;
mutable only_one_proof : Sstr.t;
prover_hist : int Mfloat.t Hprover.t;
prover_min_time : float Hprover.t;
prover_sum_time : float Hprover.t;
prover_max_time : float Hprover.t;
......@@ -71,7 +67,6 @@ let new_proof_stats () =
nb_proved_sub_goals = 0;
no_proof = Sstr.empty;
only_one_proof = Sstr.empty;
prover_hist = Hprover.create 3;
prover_min_time = Hprover.create 3;
prover_sum_time = Hprover.create 3;
prover_max_time = Hprover.create 3;
......@@ -117,27 +112,13 @@ let update_count tbl (prover, _time) =
| None -> 1)
~name:prover
let update_hist tbl (prover, time) =
let h =
try Hprover.find tbl prover
with Not_found -> Mfloat.empty
in
let h =
try
let c = Mfloat.find time h in
Mfloat.add time (succ c) h
with Not_found ->
Mfloat.add time 1 h
in
Hprover.replace tbl prover h
let update_perf_stats stats ((_,t) as prover_and_time) =
if t > stats.max_time then stats.max_time <- t;
update_min_time stats.prover_min_time prover_and_time;
update_max_time stats.prover_max_time prover_and_time;
update_sum_time stats.prover_sum_time prover_and_time;
update_count stats.prover_num_proofs prover_and_time;
update_hist stats.prover_hist prover_and_time
update_count stats.prover_num_proofs prover_and_time
let string_of_prover p = Pp.string_of_wnl print_prover p
......@@ -367,7 +348,7 @@ let run_one stats r0 r1 fname =
session;
if !opt_tree_print then
printf "%a@." print_session session;
if !opt_stats_print || !opt_hist_print then
if !opt_stats_print then
begin
(* fill_prover_data stats session; *)
PHstr.iter (stats_of_file stats) session.session_files;
......@@ -375,61 +356,6 @@ let run_one stats r0 r1 fname =
r1 := stats2_of_session ~nb_proofs:1 session !r1
end
(**** print histograms ******)
let print_hist stats =
let main_file,main_ch =
Filename.open_temp_file "why3session" ".gnuplot"
in
let main_fmt = formatter_of_out_channel main_ch in
fprintf main_fmt "set logscale y@\n";
fprintf main_fmt "set key rmargin@\n";
let max_sum_times =
Hprover.fold
(fun _ s acc -> max s acc)
stats.prover_sum_time 0.0
in
let (_:int) =
Hprover.fold
(fun p h acc ->
let pf,ch = Filename.open_temp_file "why3session" ".data" in
if acc = 1 then
fprintf main_fmt "plot [1:%d] [0.01:%.2f] "
(stats.nb_proved_sub_goals + stats.nb_proved_root_goals)
max_sum_times
else
fprintf main_fmt "replot";
fprintf main_fmt
" \"%s\" using 2:1 title \"%s\" with linespoints ps 0.2@\n"
pf (string_of_prover p);
let fmt = formatter_of_out_channel ch in
let (_ : float * int) =
Mfloat.fold
(fun t c (acct,accc) ->
let accc = c + accc in
let acct = t +. acct in
fprintf fmt "%.2f %d@\n" acct accc;
(acct,accc))
h (0.0,0)
in
fprintf fmt "@.";
close_out ch;
acc+1)
stats.prover_hist 1
in
fprintf main_fmt "pause -1 \"Press any key\"@\n";
fprintf main_fmt "set terminal pdfcairo@\n";
fprintf main_fmt "set output \"why3session.pdf\"@\n";
fprintf main_fmt "replot@.";
close_out main_ch;
let cmd = "gnuplot " ^ main_file in
eprintf "Running command %s@." cmd;
let ret = Sys.command cmd in
if ret <> 0 then
eprintf "Command %s failed@." cmd
else
eprintf "See also results in file why3session.pdf@."
(****** run on all files ******)
let run () =
......@@ -442,8 +368,7 @@ let run () =
begin
(* finalize_stats stats; *)
print_stats !r0 !r1 stats
end;
if !opt_hist_print then print_hist stats
end
let cmd =
......
......@@ -13,6 +13,9 @@ open Why3
module S = Session
module C = Whyconf
let verbose = Debug.register_info_flag "verbose"
~desc:"Increase verbosity."
type spec_list = (Arg.key * Arg.spec * Arg.doc) list
type cmd =
......@@ -58,6 +61,7 @@ let common_options = [
"--library", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
"<dir> same as -L";
"-v", Arg.Set opt_version, " prints version information" ;
Debug.Args.desc_shortcut "verbose" "--verbose" "increase verbosity";
Debug.Args.desc_debug_list;
Debug.Args.desc_debug_all;
Debug.Args.desc_debug;
......
......@@ -12,6 +12,8 @@
open Why3
open Whyconf
val verbose: Debug.flag
type spec_list = (Arg.key * Arg.spec * Arg.doc) list
type cmd =
......
......@@ -28,9 +28,6 @@ module C = Call_provers
**)
let debug = register_info_flag "verbose"
~desc:"Describe@ all@ the@ result@ compared@ to@ the@ previous."
(** To prover *)
type edit_mode =
......@@ -149,7 +146,7 @@ end
module M = Session_scheduler.Make(O)
let print_res fname pa ps old_ps =
dprintf debug
dprintf verbose
"@[<hov 2>From file %s:@\nResult@ for@ the@ proof@ attempt@ %a:\
@ %a@\nPreviously@ it@ was@ %a@]@."
fname print_external_proof pa print_attempt_status ps
......@@ -201,7 +198,7 @@ let run_one sched env config filters interactive_provers fname =
read_update_session ~allow_obsolete:(!opt_outofsync <> Outofsync_none)
env config fname in
if out_of_sync then
dprintf debug "@[From@ file@ %s:out of sync@]@." fname;
dprintf verbose "@[From@ file@ %s:out of sync@]@." fname;
let todo = Todo.create () (fun () _ -> ())
(fun () ->
if !opt_save <> Save_none &&
......@@ -223,13 +220,13 @@ let run_one sched env config filters interactive_provers fname =
| _, M.StatusChange (Interrupted) -> Todo.stop todo
| _, M.StatusChange (JustEdited|Unedited) -> assert false
| _, M.MissingFile efname ->
dprintf debug
dprintf verbose
"@[From@ file@ %s:@\nThe@ edited@ file@ %s@ for@ the@ proof@ of@ %a@ \
is@ missing@]@."
fname efname print_proof_goal pa;
Todo.stop todo
| _, M.MissingProver ->
dprintf debug
dprintf verbose
"@[From@ file@ %s:@\nThe@ prover@ %a@ for@ the@ proof@ of@ %a@ is@ \
not@ installed@]@."
fname Whyconf.print_prover p
......@@ -248,7 +245,7 @@ let run_one sched env config filters interactive_provers fname =
queue_proof pa old_res new_res
| Some old_res, M.StatusChange (Done new_res)
when same_result old_res new_res ->
dprintf debug
dprintf verbose
"@[From@ file@ %s:@\nThe@ prover@ %a for@ the@ proof@ of@ \
%a@ give@ the@ same@ result@ %a@ as@ before@ %a.@]@."
fname print_prover pa.proof_prover print_proof_goal pa
......@@ -259,7 +256,7 @@ let run_one sched env config filters interactive_provers fname =
set_proof_state ~obsolete:false ~archived:false (Done new_res) pa;
Todo.stop todo
| None, M.StatusChange (Done new_res) ->
dprintf debug
dprintf verbose
"@[From@ file@ %s:@\nThe@ prover@ %a@ for@ the@ proof,@ previously@ \
undone,@ of@ %a@ give@ the@ new@ result@ %a.@]@."
fname print_prover pa.proof_prover
......@@ -268,7 +265,7 @@ let run_one sched env config filters interactive_provers fname =
set_proof_state ~obsolete:false ~archived:false (Done new_res) pa;
Todo.stop todo
| Some old_res, M.StatusChange (Done new_res) when pa.proof_obsolete ->
dprintf debug
dprintf verbose
"@[From@ file@ %s:@\nThe@ prover@ %a@ for@ the@ proof@ of@ %a@ give@ \
the@ result@ %a@ instead@ of@ the@ obsolete@ %a.@]@."
fname print_prover pa.proof_prover print_proof_goal pa
......@@ -277,7 +274,7 @@ let run_one sched env config filters interactive_provers fname =
set_proof_state ~obsolete:false ~archived:false (Done new_res) pa;
Todo.stop todo
| Some old_res, M.StatusChange (Done new_res) ->
dprintf debug
dprintf verbose
"@[From@ file@ %s:@\nThe@ prover@ %a@ for@ the@ proof@ of@ %a@ give@ \
the@ result@ %a@ instead@ of@ %a.@]@."
fname print_prover pa.proof_prover print_proof_goal pa
......@@ -286,7 +283,7 @@ let run_one sched env config filters interactive_provers fname =
set_proof_state ~obsolete:false ~archived:false (Done new_res) pa;
Todo.stop todo
| _, M.StatusChange (InternalFailure exn) ->
dprintf debug
dprintf verbose
"@[From@ file@ %s:@\nThe@ prover@ %a@ for@ the@ proof@ of@ %a@ \
failed@ with@ the@ error@ %a@]@."
fname print_prover pa.proof_prover print_proof_goal pa
......
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