whybench : csv output

examples/programs/prgbench.rc

@@ -12,4 +12,7 @@ transform = "split_goal"
 
 [bench fast_and_funny]
 tools = fast
-probs = funny
\ No newline at end of file
+probs = funny
+timeline = "prgbench.time"
+average = "prgbench.avg"
+csv = "prgbench.csv"

src/bench/bench.ml

@@ -161,13 +161,14 @@ let all_list_tools ?callback tools probs =
 
 type output =
   (** on stdout *)
-  |Average
-  |Timeline
+  |Average of string
+  |Timeline of string
   (** In a file *)
-  |Csv
+  |Csv of string
 
 type ('a,'b) bench =
     {
+      bname  : string;
       btools : 'a tool list;
       bprobs : 'b prob list;
       boutputs : output list;
@@ -261,3 +262,87 @@ let empty_tool_res =
 
   let max_time l =
     List.fold_left (fun acc {result={pr_time = t}} -> max acc t) 0. l
+
+  open Format
+(**
+answer output time
+
+*)
+
+
+  let print_prover_answer fmt = function
+    | Valid -> fprintf fmt "Valid"
+    | Invalid -> fprintf fmt "Invalid"
+    | Timeout -> fprintf fmt "Timeout"
+    | Unknown s -> fprintf fmt "Unknown: %S" s
+    | Failure s -> fprintf fmt "Failure: %S" s
+    | HighFailure -> fprintf fmt "HighFailure"
+
+  let print_newline fmt () = fprintf fmt "\n"
+
+  let print_csv cmp print_tool print_probs fmt l =
+    let cmp x y =
+      let c = cmp x.prob y.prob in
+      if c <> 0 then c else
+        let id x = (Task.task_goal x.task).Decl.pr_name.Ident.id_string in
+        let c = String.compare (id x) (id y) in
+        if c <> 0 then c else compare x.idtask y.idtask in
+    let l = List.map (fun (p,l) -> p,List.fast_sort cmp l) l in
+    fprintf fmt "prover ,";
+    let print_header fmt e = fprintf fmt "%a, " print_probs e.prob in
+    begin match l with
+      | [] -> ()
+      | (_,r)::_ -> Pp.print_list Pp.comma print_header fmt r
+    end;
+    print_newline fmt ();
+    let print_cell fmt r =
+      fprintf fmt "%a, %.3f" (*"%a, %S, %.3f"*)
+        print_prover_answer r.result.pr_answer (*r.result.pr_output*)
+        r.result.pr_time in
+    let print_line fmt (p,l) =
+      fprintf fmt "%a ," print_tool p;
+      Pp.print_list Pp.comma print_cell fmt l in
+    Pp.print_list print_newline print_line fmt l
+
+  let print_timeline print_tool fmt l =
+    let l = List.map (fun (t,l) -> t,filter_timeline l) l in
+    let max = List.fold_left (fun acc (_,l) -> max acc (max_time l)) 0. l in
+    let max = max +. 0.1 in
+    let step = max /. 10. in
+    let tl = List.map (fun (t,l) -> t,compute_timeline 0. max step l) l in
+    let print_timeline (tool_val,timeline) =
+      fprintf fmt "@[%a - %a@]@."
+        (Pp.print_list Pp.comma (fun fmt -> fprintf fmt "%4i"))
+        timeline print_tool tool_val in
+    fprintf fmt "@[%a@]@."
+      (Pp.print_iter1 (fun f -> Util.iterf f 0. max)
+         Pp.comma (fun fmt -> fprintf fmt "%3.2f"))
+      step;
+    List.iter print_timeline tl
+
+
+  let print_average print_tool fmt l =
+    let tool_res = List.map (fun (t,l) -> t,compute_average l) l in
+    let print_tool_res (tool_val,tool_res) =
+      fprintf fmt "%a - %a@." print_tool_res tool_res print_tool tool_val in
+    fprintf fmt "(v,t,u,f,i) - valid, unknown, timeout, invalid, failure@.";
+    List.iter print_tool_res tool_res
+
+
+  let print_output cmp print_tool print_probs (b,l) =
+    let open_std f s =
+      if s = "-"
+      then begin f std_formatter;pp_print_flush std_formatter () end
+      else
+        let cout = (open_out s) in
+        let fmt = (formatter_of_out_channel cout) in
+        f fmt;
+        pp_print_flush fmt ();
+        close_out cout in
+    List.iter (function
+      | Average s -> open_std (fun fmt -> print_average print_tool fmt l) s
+      | Timeline s -> open_std (fun fmt -> print_timeline print_tool fmt l) s
+      | Csv s ->
+        open_std (fun fmt -> Pp.wnl fmt;
+          print_csv cmp print_tool print_probs fmt l) s
+    ) b.boutputs

src/bench/bench.mli

@@ -70,15 +70,17 @@ val all_list_tools :
   ?callback:('a,'b) callback ->
   'a tool list -> 'b prob list -> ('a * ('a,'b) result list) list
 
+
 type output =
   (** on stdout *)
-  |Average
-  |Timeline
+  |Average of string
+  |Timeline of string
   (** In a file *)
-  |Csv
+  |Csv of string
 
 type ('a,'b) bench =
     {
+      bname  : string;
       btools : 'a tool list;
       bprobs : 'b prob list;
       boutputs : output list;
@@ -117,3 +119,18 @@ val compute_timeline :
 val filter_timeline : ('a,'b) result list -> ('a,'b) result list
 
 val max_time : ('a,'b) result list -> float
+
+open Format
+
+val print_csv :
+  ('b -> 'b -> int)         ->
+  (formatter -> 'a -> unit) ->
+  (formatter -> 'b -> unit) ->
+  formatter ->
+  ('a * ('a,'b) result list) list -> unit
+
+val print_output :
+  ('b -> 'b -> int)         ->
+  (formatter -> 'a -> unit) ->
+  (formatter -> 'b -> unit) ->
+  ('a,'b) bench * ('a * ('a,'b) result list) list -> unit

src/bench/benchrc.ml

@@ -36,6 +36,7 @@ open Whyconf
 open Rc
 
 let absolute_filename dirname f =
+  if f = "-" then f else
   if Filename.is_relative f then
     Filename.concat dirname f
   else
@@ -129,7 +130,7 @@ let read_probs absf map (name,section) =
     Scheduler.do_why_sync fwhy () in
   Mstr.add name { ptask   = gen; ptrans   = gen_trans} map
 
-let read_bench mtools mprobs map (name,section) =
+let read_bench absf mtools mprobs map (name,section) =
   let tools = get_stringl section "tools" in
   let lookup s =
     try Mstr.find s mtools
@@ -142,14 +143,20 @@ let read_bench mtools mprobs map (name,section) =
     with Not_found -> eprintf "Undefined probs %s@." s;
       exit 1 in
   let probs = List.map lookup probs in
-  let outputs = get_stringl ~default:[] section "outputs" in
-  let check = function
-    | "average" -> Average
-    | "timeline" -> Timeline
-    | "csv" -> Csv
-    | s -> eprintf "Unknown output %s@." s; exit 1 in
-  let outputs = List.map check outputs in
-  Mstr.add name { btools = tools; bprobs = probs; boutputs = outputs} map
+  let averages = get_stringl ~default:[] section "average" in
+  let outputs = List.fold_left
+    (cons (fun s -> Average (absf s)))
+    [] averages in
+  let timelines = get_stringl ~default:[] section "timeline" in
+  let outputs = List.fold_left
+    (cons (fun s -> Timeline (absf s)))
+    outputs timelines in
+  let csvs = get_stringl ~default:[] section "csv" in
+  let outputs = List.fold_left
+    (cons (fun s -> Csv (absf s)))
+    outputs csvs in
+  Mstr.add name
+    { bname = name; btools = tools; bprobs = probs; boutputs = outputs} map
 
 
 let read_file wc f =
@@ -160,7 +167,7 @@ let read_file wc f =
   let probs = get_family rc "probs" in
   let probs = List.fold_left (read_probs absf) Mstr.empty probs in
   let benchs = get_family rc "bench" in
-  let benchs = List.fold_left (read_bench tools probs)
+  let benchs = List.fold_left (read_bench absf tools probs)
     Mstr.empty benchs in
   {tools = tools;
    probs = probs;

src/bench/whybench.ml

@@ -337,7 +337,20 @@ let () =
       }::acc in
   probs := Queue.fold fold_prob [] opt_queue;
 
-  benchs := List.map (Benchrc.read_file config) !opt_benchrc
+  let cmdl = "commandline" in
+  let bench = List.map (Benchrc.read_file config) !opt_benchrc in
+  let bench = if !tools <> [] && !probs <> [] then
+      let b_cmdl = {
+        B.bname = cmdl;
+        btools = !tools; bprobs = !probs;
+        boutputs = [B.Timeline "-";B.Average "-"]} in
+      { Benchrc.tools = Mstr.empty;
+        probs = Mstr.empty;
+        benchs = Mstr.singleton cmdl b_cmdl}
+      ::bench
+    else bench in
+  benchs := bench
+
 
   with e when not (Debug.test_flag Debug.stack_trace) ->
     eprintf "%a@." Exn_printer.exn_printer e;
@@ -345,40 +358,8 @@ let () =
 
 let () = Scheduler.async := (fun f v -> ignore (Thread.create f v))
 
-let print_result l =
-  let tool_res = List.map (fun (t,l) -> t,B.compute_average l) l in
-  let print_tool_res ((_,tool_name),tool_res) =
-    printf "%a - %s@." B.print_tool_res tool_res tool_name in
-  printf "(v,t,u,f,i) - valid, unknown, timeout, invalid, failure@.";
-  List.iter print_tool_res tool_res
-
-let print_timeline l =
-  let l = List.map (fun (t,l) -> t,B.filter_timeline l) l in
-  let max = List.fold_left (fun acc (_,l) -> max acc (B.max_time l)) 0. l in
-  let step = max/.10. in
-  let tl = List.map (fun (t,l) -> t,B.compute_timeline 0. max step l) l in
-  let print_timeline ((_,tool_name),timeline) =
-    printf "@[%a - %s@]@."
-      (Pp.print_list Pp.comma (fun fmt -> fprintf fmt "%.3i")) 
-      timeline tool_name in
-  printf "@[%a@]@."
-    (Pp.print_iter1 (fun f -> iterf f 0. max)
-       Pp.comma (fun fmt -> fprintf fmt "%.3f"))
-    step;
-  List.iter print_timeline tl
-
-
 let () =
   let m = Mutex.create () in
-  let callback (_,tool) (_,_,prob) task i res =
-    Mutex.lock m;
-    printf "%s %a %i with %s : %a@."
-      prob Pretty.print_pr (task_goal task) i tool
-      Scheduler.print_pas res;
-    Mutex.unlock m
-  in
-  let l = B.all_list_tools ~callback !tools !probs in
-  print_result l;
   let callback (_,tool) (_,file,prob) task i res =
     Mutex.lock m;
     printf "%s.%s %a %i with %s : %a@."
@@ -390,8 +371,10 @@ let () =
     List.map (fun b -> List.map snd (Mstr.bindings b.Benchrc.benchs))
       !benchs in
   let bl = B.run_benchs_tools ~callback (list_flatten_rev benchs) in
-  List.iter (fun (_,l) -> print_result l) bl;
-    List.iter (fun (_,l) -> print_timeline l) bl
+  let print_tool fmt (t,s) = fprintf fmt "%s.%s" t s in
+  let print_prob fmt (b,f,t) = fprintf fmt "%s.%s.%s" b f t in
+  let cmp = compare in
+  List.iter (B.print_output cmp print_tool print_prob) bl
 
 (*
 Local Variables:

src/ide/scheduler.ml

@@ -179,7 +179,7 @@ let event_handler () =
         in
         incr scheduled_proofs;
         Debug.dprintf debug
-          "scheduled_proofs = %i; maximum_running_proofs = %i@."
+          "scheduled_proofs = %i; maximum_running_proofs = %i;@."
           !scheduled_proofs !maximum_running_proofs;
         Mutex.unlock queue_lock;
         (* build the prover task from goal in [a] *)

src/util/pp.ml

@@ -154,13 +154,16 @@ let string_of p x =
   fprintf fmt "%a@?" p x;
   Buffer.contents b
 
+let wnl fmt =
+  let out,flush,_newline,spaces =
+    pp_get_all_formatter_output_functions fmt () in
+  pp_set_all_formatter_output_functions fmt
+    ~out ~flush ~newline:(fun () -> spaces 1) ~spaces
+
 
 let string_of_wnl p x =
   let b = Buffer.create 100 in
   let fmt = formatter_of_buffer b in
-  let out,flush,_newline,spaces =
-    pp_get_all_formatter_output_functions fmt () in
-  pp_set_all_formatter_output_functions fmt
-    ~out ~flush ~newline:(fun () -> spaces 1) ~spaces;
+  wnl fmt;
   fprintf fmt "%a@?" p x;
   Buffer.contents b

src/util/pp.mli

@@ -122,3 +122,5 @@ val print_list_opt :
 val string_of : (Format.formatter -> 'a -> unit) -> 'a -> string
 val string_of_wnl : (Format.formatter -> 'a -> unit) -> 'a -> string
   (** same as {!string_of} but without newline *)
+
+val wnl : Format.formatter -> unit