Update runner with single-query and mulity-query mode

.gitignore

@@ -31,3 +31,5 @@ nix/profiles/
 # dkml desktop CI
 /msys64
 /.ci
+
+res-*

bench/runner/dune

@@ -1,3 +1,17 @@
 (executable
  (name runner)
- (libraries bos cohttp cohttp-lwt-unix cmdliner lwt yojson str))
+ (libraries
+  bos
+  cohttp
+  cohttp-lwt-unix
+  core_unix
+  cmdliner
+  dune-glob
+  owl
+  lwt
+  yojson
+  str
+  smtml
+  smtml.prelude)
+ (flags
+  (:standard -open Smtml_prelude)))

bench/runner/git.ml

@@ -1,14 +1,14 @@
 (** Best effort to try and get commit hash of HEAD *)
 let get_head ?(length = 6) () =
   let open Bos in
-  let short = Format.asprintf "--short=%d" length in
+  let short = Fmt.str "--short=%d" length in
   let cmd = Cmd.(v "git" % "rev-parse" % short % "HEAD") in
   let output = OS.Cmd.run_out ~err:OS.Cmd.err_run_out cmd in
   match OS.Cmd.out_string ~trim:true output with
   | Ok (stdout, (_, `Exited 0)) -> stdout
   | Error (`Msg err) ->
-    Format.eprintf "ERROR: %s@." err;
+    Fmt.epr "ERROR: %s@." err;
     "unknown"
   | Ok (stdout, (_, (`Exited _ | `Signaled _))) ->
-    Format.eprintf "%s@\nWARN: Unable to fetch git HEAD@." stdout;
+    Fmt.epr "%s@\nWARN: Unable to fetch git HEAD@." stdout;
     "unknown"

bench/runner/multi_query.ml

@@ -0,0 +1,93 @@
+let pp_exit_status fmt = function
+  | Ok () -> Fmt.pf fmt "Exited 0"
+  | Error (`Exit_non_zero n) -> Fmt.pf fmt "Exited %d" n
+  | Error (`Signal s) -> Fmt.pf fmt "Signal %s" (Core.Signal.to_string s)
+
+let parse_stdout =
+  let re = Dune_re.(compile @@ Perl.re {|Run\s(.*?)\sin\s([0-9.]+)|}) in
+  fun stdout ->
+    let matches = Dune_re.all re stdout in
+    List.map
+      (fun group ->
+        let benchmark = Dune_re.Group.get group 1 in
+        let rtime = Dune_re.Group.get group 2 in
+        (benchmark, Float.of_string rtime) )
+      matches
+
+let parse_results (prover, (_status, stdout, _stderr, _rusage)) =
+  let results = parse_stdout stdout in
+  let results =
+    List.map
+      (fun (benchmark, rtime) ->
+        (Tool.prover_to_string prover, benchmark, rtime) )
+      results
+  in
+  (prover, results)
+
+let summary results =
+  List.iter
+    (fun (prover, results) ->
+      let total, rtime =
+        List.fold_left
+          (fun (total, time) (_, _, rtime) -> (succ total, time +. rtime))
+          (0, 0.) results
+      in
+      Fmt.pr "Ran %d benchmarks on %a in %0.03f" total Tool.pp_prover prover
+        rtime )
+    results
+
+let make_data_frames results =
+  List.map
+    (fun (prover, prover_results) ->
+      let provers, benchmark, rtime =
+        List.fold_left
+          (fun (prover_acc, bench_acc, rtime_acc) (prover, benchmark, rtime) ->
+            (prover :: prover_acc, benchmark :: bench_acc, rtime :: rtime_acc)
+            )
+          ([], [], []) prover_results
+      in
+      let df =
+        Owl_dataframe.make
+          [| "prover"; "benchmark"; "rtime" |]
+          ~data:
+            [| Owl_dataframe.pack_string_series @@ Array.of_list provers
+             ; Owl_dataframe.pack_string_series @@ Array.of_list benchmark
+             ; Owl_dataframe.pack_float_series @@ Array.of_list rtime
+            |]
+      in
+      (prover, df) )
+    results
+
+let write_data_frame started_at results_dir (prover, df) =
+  let csv_file = Fmt.str "%a-%s.csv" Tool.pp_prover prover started_at in
+  let csv_path = Fpath.(results_dir / csv_file) in
+  Owl_dataframe.to_csv ~sep:',' df (Fpath.to_string csv_path)
+
+let main _hook provers dirs =
+  let open Result in
+  let now = Core_unix.(localtime @@ gettimeofday ()) in
+  let started_at = Core_unix.strftime now "%Y%m%dT%H%M%S" in
+  assert (List.for_all Tool.is_available provers);
+  List.iter
+    (fun (p : Tool.prover) -> match p with Z3 -> () | Smtml p -> p.st <- true)
+    provers;
+  let dirs = List.map Fpath.to_string dirs in
+  let results =
+    List.map
+      (fun p ->
+        let ((status, stdout, _stderr, _) as result) =
+          Tool.fork_and_run p dirs
+        in
+        Fmt.pr "@[<v 2>Run %a@;Exited: %a@;Stdout:@; %a@]@." Tool.pp_prover p
+          pp_exit_status status Fmt.string (String.escaped stdout);
+        (p, result) )
+      provers
+  in
+  let results = List.map parse_results results in
+  summary results;
+  let data_frames = make_data_frames results in
+  let results_dir = Fmt.kstr Fpath.v "res-multi-query-%s" started_at in
+  let* _ = Bos.OS.Dir.create ~path:true results_dir in
+  List.iter (write_data_frame started_at results_dir) data_frames;
+  (* Option.iter (Notify.notify_done msg) hook; *)
+  Ok ()

bench/runner/notify.ml

@@ -0,0 +1,7 @@
+let notify_done results url =
+  let url = Webhook.url_of_string url in
+  let head = Git.get_head () in
+  let title = Fmt.str "Test results (commit hash=%s) :octopus:" head in
+  let body = Fmt.str "```%s```" results in
+  let body = Webhook.default_slack_mrkdwn title body in
+  Lwt_main.run @@ Webhook.post_and_forget url body

bench/runner/runner.ml

@@ -1,21 +1,32 @@
+let prover_conv = Cmdliner.Arg.conv (Tool.prover_of_string, Tool.pp_prover)
+
+let fpath_dir =
+  let dir_parser, _ = Cmdliner.Arg.dir in
+  ( (fun str ->
+      match dir_parser str with
+      | `Ok dir -> `Ok (Fpath.v dir)
+      | `Error _ as err -> err )
+  , Fpath.pp )
+
 let cli =
   let open Cmdliner in
-  let run =
-    let task = Arg.(required & opt (some string) None & info [ "task" ]) in
-    let hook = Arg.(value & opt (some string) None & info [ "web-hook" ]) in
-    let info = Cmd.info "run" in
-    Cmd.v info Term.(const Benchpress.run $ hook $ task)
+  let hook = Arg.(value & opt (some string) None & info [ "web-hook" ]) in
+  let dirs = Arg.(value & pos_all fpath_dir [] & info [] ~docv:"PATH") in
+  let provers = Arg.(value & opt_all prover_conv [] & info [ "p"; "prover" ]) in
+  let timeout = Arg.(value & opt (some int) None & info [ "timeout" ]) in
+  let single_query =
+    let info = Cmd.info "single-query" in
+    Cmd.v info Term.(const Single_query.main $ hook $ provers $ timeout $ dirs)
   in
-  let latest_results =
-    let nc = Arg.(value & flag & info [ "nc" ]) in
-    let info = Cmd.info "latest-results" in
-    Cmd.v info Term.(const Benchpress.latest_results $ nc)
+  let multi_query =
+    let info = Cmd.info "multi-query" in
+    Cmd.v info Term.(const Multi_query.main $ hook $ provers $ dirs)
   in
   let info = Cmd.info "runner" in
-  Cmd.group info [ run; latest_results ]
+  Cmd.group info [ single_query; multi_query ]
 
 let () =
   match Cmdliner.Cmd.eval_value' cli with
   | `Exit code -> exit code
-  | `Ok (Error (`Msg err)) -> failwith err
+  | `Ok (Error (`Msg err)) -> Fmt.failwith "%s" err
   | `Ok (Ok ()) -> exit 0