sneeuwballen · c-cube · Jan 29, 2024 · Jan 22, 2024 · Jan 22, 2024 · Jan 23, 2024
diff --git a/benchpress-server.opam b/benchpress-server.opam
@@ -20,7 +20,7 @@ depends: [
   "gnuplot" { >= "0.6" & < "0.8" }
   "sqlite3"
   "sqlite3_utils" { >= "0.4" & < "0.5" }
-  "tiny_httpd" { >= "0.12" & < "1.0" }
+  "tiny_httpd" { >= "0.16" & < "1.0" }
   "printbox" { >= "0.6" }
   "printbox-text" { >= "0.6" }
   "ocaml" {>= "4.12" }

diff --git a/benchpress.opam b/benchpress.opam
@@ -24,7 +24,7 @@ depends: [
   "processor"
   "pp_loc" { >= "2.0" & < "3.0" }
   "gnuplot" { >= "0.6" & < "0.8" }
-  "sqlite3"
+  "sqlite3" { >= "5.0.3" } # https://github.com/sneeuwballen/benchpress/pull/73#issuecomment-1764108025
   "sqlite3_utils" { >= "0.4" & < "0.6" }
   "printbox" { >= "0.6" }
   "printbox-text" { >= "0.6" }

diff --git a/src/bin/benchpress_bin.ml b/src/bin/benchpress_bin.ml
@@ -19,9 +19,10 @@ module Run = struct
   (* sub-command for running tests *)
   let cmd =
     let open Cmdliner in
-    let aux j cpus pp_results dyn paths dir_files proof_dir defs task timeout
-        memory meta provers csv summary no_color output save wal_mode
+    let aux j cpus pp_results dyn paths dir_files proof_dir (log_lvl, defs) task
+        timeout memory meta provers csv summary no_color output save wal_mode
         desktop_notification no_failure update =
+      Misc.setup_logs log_lvl;
       catch_err @@ fun () ->
       if no_color then CCFormat.set_color_default false;
       let dyn =
@@ -173,10 +174,11 @@ module Slurm = struct
   (* sub-command for running tests with slurm *)
   let cmd =
     let open Cmdliner in
-    let aux j pp_results dyn paths dir_files proof_dir defs task timeout memory
-        meta provers csv summary no_color output save wal_mode
+    let aux j pp_results dyn paths dir_files proof_dir (log_lvl, defs) task
+        timeout memory meta provers csv summary no_color output save wal_mode
         desktop_notification no_failure update partition nodes addr port ntasks
         =
+      Misc.setup_logs log_lvl;
       catch_err @@ fun () ->
       if no_color then CCFormat.set_color_default false;
       let dyn =
@@ -543,7 +545,8 @@ end
 (** {2 See prover(s)} *)
 
 module Prover_show = struct
-  let run defs names =
+  let run (log_lvl, defs) names =
+    Misc.setup_logs log_lvl;
     catch_err @@ fun () ->
     let l = CCList.map (Definitions.find_prover' defs) names in
     Format.printf "@[<v>%a@]@." (Misc.pp_list Prover.pp) l;
@@ -561,7 +564,8 @@ end
 (** {2 List provers} *)
 
 module Prover_list = struct
-  let run defs =
+  let run (log_lvl, defs) =
+    Misc.setup_logs log_lvl;
     catch_err @@ fun () ->
     let l = Definitions.all_provers defs in
     Format.printf "@[<v>%a@]@."
@@ -580,7 +584,8 @@ end
 (** {2 Show Task} *)
 
 module Task_show = struct
-  let run defs names =
+  let run (log_lvl, defs) names =
+    Misc.setup_logs log_lvl;
     catch_err @@ fun () ->
     let l = CCList.map (Definitions.find_task' defs) names in
     Format.printf "@[<v>%a@]@." (Misc.pp_list Task.pp) l;
@@ -598,7 +603,8 @@ end
 (** {2 List Tasks} *)
 
 module Task_list = struct
-  let run defs =
+  let run (log_lvl, defs) =
+    Misc.setup_logs log_lvl;
     catch_err @@ fun () ->
     let l = Definitions.all_tasks defs in
     Format.printf "@[<v>%a@]@."

diff --git a/src/core/Bin_utils.ml b/src/core/Bin_utils.ml
@@ -2,10 +2,9 @@ module T = Test
 module Db = Misc.Db
 module MStr = Misc.Str_map
 
-let definitions_term : Definitions.t Cmdliner.Term.t =
+let definitions_term : (Logs.level option * Definitions.t) Cmdliner.Term.t =
   let open Cmdliner in
   let aux conf_files with_default logs_cmd =
-    Misc.setup_logs logs_cmd;
     let conf_files = CCList.flatten conf_files in
     let conf_files =
       let default_conf = Misc.default_config () in
@@ -22,7 +21,7 @@ let definitions_term : Definitions.t Cmdliner.Term.t =
     try
       let stanzas = Stanza.parse_files conf_files in
       let defs = Definitions.add_stanza_l stanzas Definitions.empty in
-      `Ok defs
+      `Ok (logs_cmd, defs)
     with Error.E err -> `Error (false, Error.show err)
   in
   let args =

diff --git a/src/core/Prover.ml b/src/core/Prover.ml
@@ -347,7 +347,7 @@ let of_db db name : t =
         ~ty:Db.Ty.(p1 text, p2 any_str any_str, mkp2)
         ~f:Db.Cursor.to_list name
     with e ->
-      Log.err (fun k ->
+      Log.debug (fun k ->
           k "prover.of_db: could not find tags: %s" (Printexc.to_string e));
       []
   in

diff --git a/src/core/Test_detailed_res.ml b/src/core/Test_detailed_res.ml
@@ -141,9 +141,8 @@ let get_res db prover file : _ * proof_check_res option =
               float;
               float;
             ],
-            fun x1 x2 x3 x4 x5 x6 x7 x8 x9 ->
-              Logs.info (fun k -> k "got results");
-              x1, x2, x3, x4, x5, x6, x7, x8, x9 ))
+            fun x1 x2 x3 x4 x5 x6 x7 x8 x9 -> x1, x2, x3, x4, x5, x6, x7, x8, x9
+          ))
     |> Misc.unwrap_db (fun () -> spf "listing results")
     |> Error.unwrap_opt' (fun () ->
            spf "expected a non-empty result for prover='%s', file='%s'" prover
@@ -157,7 +156,6 @@ let get_res db prover file : _ * proof_check_res option =
              rtime,
              utime,
              stime ) ->
-    Logs.info (fun k -> k "got results 2");
     let stdout = CCOpt.get_or ~default:"" stdout in
     let stderr = CCOpt.get_or ~default:"" stderr in
     Logs.debug (fun k -> k "res.of_string tags=[%s]" (String.concat "," tags));
@@ -171,9 +169,7 @@ let get_res db prover file : _ * proof_check_res option =
       { Run_proc_result.errcode; stdout; stderr; rtime; utime; stime }
   in
   let proof_check_res = get_proof_check db prover file in
-  Logs.info (fun k -> k "try to get prover");
   let prover = Prover.of_db db prover in
-  Logs.info (fun k -> k "got prover");
   Run_result.map ~f:(fun _ -> prover) res, proof_check_res
 
 module PB = PrintBox

diff --git a/src/core/Test_stat.ml b/src/core/Test_stat.ml
@@ -11,12 +11,7 @@ module Stats = struct
   let curr = snd
   let init = { n = 0; total = 0.; mean = 0., 0.; s = 0., 0. }
 
-  let step ({ n; total; mean; s } as acc) x =
-    let x =
-      match x with
-      | Sqlite3.Data.FLOAT f -> f
-      | _ -> assert false
-    in
+  let step ({ n; total; mean; s } as acc) (x : float) =
     let n = n + 1 in
     let total = total +. x in
     if n = 1 then
@@ -40,13 +35,6 @@ module Stats = struct
       0.
     else
       Float.(sqrt (s /. of_int (n - 1)))
-
-  let final acc =
-    let res = Fmt.asprintf "%f|%f|%f" (total acc) (mean acc) (sd acc) in
-    Sqlite3.Data.TEXT res
-
-  let attach_aggregate db =
-    Sqlite3.Aggregate.create_fun1 db ~init ~step ~final "stats"
 end
 
 type detail_stats = { n: int; total: float; mean: float; sd: float }
@@ -159,29 +147,35 @@ let to_printbox_l ?(details = false) ?to_link l : PB.t =
 let of_db_for ~(prover : Prover.name) (db : Db.t) : t =
   Error.guard (Error.wrapf "reading stat(%s) from DB" prover) @@ fun () ->
   let custom = Prover.tags_of_db db in
-  Stats.attach_aggregate db;
-  let convert n stats =
-    let extract_stats stats =
-      String.split_on_char '|' stats |> List.map Float.of_string |> function
-      | [ total; mean; sd ] ->
-        { n = CCOpt.get_or ~default:0 n; total; mean; sd }
-      | _ -> assert false
-    in
-    extract_stats stats
-  in
   let get_res r =
     Error.guard (Error.wrapf "get-res %S" r) @@ fun () ->
-    Logs.debug (fun k -> k "get-res %S" r);
-    Db.exec db
-      {| select count(*), stats(rtime) from prover_res where prover=? and res=?; |}
-      prover r
-      ~ty:Db.Ty.(p2 text text, p2 (nullable int) text, convert)
-      ~f:Db.Cursor.get_one_exn
-    |> Misc.unwrap_db (fun () -> spf "problems with result %s" r)
+    let count : int option =
+      Db.exec db {| select count(*) from prover_res where prover=? and res=?; |}
+        prover r
+        ~ty:Db.Ty.(p2 text text, p1 (nullable int), Fun.id)
+        ~f:Db.Cursor.get_one_exn
+      |> Misc.unwrap_db (fun () -> spf "problems with result %s" r)
+    in
+
+    let stats =
+      let stat = ref Stats.init in
+      Db.exec db {| select rtime from prover_res where prover=? and res=?; |}
+        prover r
+        ~ty:Db.Ty.(p2 text text, p1 float, Fun.id)
+        ~f:(fun cursor ->
+          Db.Cursor.iter cursor ~f:(fun rtime -> stat := Stats.step !stat rtime))
+      |> Misc.unwrap_db (fun () -> spf "problems with result %s" r);
+      !stat
+    in
+
+    let total = Stats.total stats in
+    let mean = Stats.mean stats in
+    let sd = Stats.sd stats in
+    { n = CCOpt.get_or ~default:0 count; total; mean; sd }
   in
+
   let get_proof_res r =
     Error.guard (Error.wrapf "get-proof-res %S %S" prover r) @@ fun () ->
-    Logs.debug (fun k -> k "get-proof-res %S %S" prover r);
     try
       Db.exec db
         {| select count( * ) from proof_check_res where prover=? and res=?; |}