Merge pull request #57 from hra687261/master-edit

added `desktop_notification`, `no_failure` and `update` as command line options

src/bin/Run_main.ml

@@ -5,7 +5,7 @@ module Log = (val Logs.src_log (Logs.Src.create "benchpress.run-main"))
 
 (* run provers on the given dirs, return a list [prover, dir, results] *)
 let execute_run_prover_action
-    ?j ?timestamp ?pp_results ?dyn ?limits ?proof_dir ?output ~notify ~uuid ~save ~wal_mode
+    ?j ?timestamp ?pp_results ?dyn ?limits ?proof_dir ?output ~notify ~uuid ~save ~wal_mode ~update
     (defs: Definitions.t) (r:Action.run_provers)
   : (_ * Test_compact_result.t) =
   begin
@@ -26,7 +26,7 @@ let execute_run_prover_action
         ~on_start_proof_check:(fun() -> progress#on_start_proof_check)
         ~on_proof_check:progress#on_proof_check_res
         ~on_done:(fun _ -> progress#on_done) r
-        ?output
+        ?output ~update
     in
     result
   end
@@ -37,6 +37,7 @@ type top_task =
 
 let main ?j ?pp_results ?dyn ?timeout ?memory ?csv ?(provers=[])
     ?meta:_ ?summary ?task ?dir_file ?proof_dir ?output ?(save=true) ?(wal_mode=false)
+    ~desktop_notification ~no_failure ~update
     (defs:Definitions.t) paths () : unit =
   Log.info
     (fun k->k"run-main.main for paths %a" (Misc.pp_list Misc.Pp.pp_str) paths);
@@ -94,7 +95,7 @@ let main ?j ?pp_results ?dyn ?timeout ?memory ?csv ?(provers=[])
       let (top_res, (results:Test_compact_result.t)) =
         execute_run_prover_action
           ~uuid ?pp_results ?proof_dir ?dyn:progress ~limits ?j ?output ~notify ~timestamp ~save ~wal_mode
-          defs run_provers_action
+          ~update defs run_provers_action
       in
       if CCOpt.is_some csv then (
         let res = Lazy.force top_res in
@@ -105,13 +106,14 @@ let main ?j ?pp_results ?dyn ?timeout ?memory ?csv ?(provers=[])
         Bin_utils.dump_summary ~summary res
       );
       (* now fail if results were bad *)
-      let r = Bin_utils.check_compact_res notify results in
+      let r = Bin_utils.check_compact_res ~no_failure notify results in
       Notify.sync notify;
       Bin_utils.printbox_compact_results results;
       (* try to send a desktop notification *)
-      (try CCUnix.call "notify-send 'benchmark done (%s)'"
-             (CCOpt.map_or ~default:"?" Misc.human_duration
-                results.cr_meta.total_wall_time) |> ignore
-       with _ -> ());
+      if desktop_notification then
+        (try CCUnix.call "notify-send 'benchmark done (%s)'"
+               (CCOpt.map_or ~default:"?" Misc.human_duration
+                  results.cr_meta.total_wall_time) |> ignore
+         with _ -> ());
       r
   end

src/bin/benchpress_bin.ml

@@ -18,19 +18,21 @@ module Run = struct
   let cmd =
     let open Cmdliner in
     let aux j pp_results dyn paths dir_file proof_dir defs task timeout memory
-        meta provers csv summary no_color output save wal_mode =
+        meta provers csv summary no_color output save wal_mode
+        desktop_notification no_failure update =
       catch_err @@ fun () ->
       if no_color then CCFormat.set_color_default false;
       let dyn = if dyn then Some true else None in
       Run_main.main ~pp_results ?dyn ~j ?timeout ?memory ?csv ~provers
-        ~meta ?task ?summary ?dir_file ?proof_dir ?output ~save ~wal_mode defs paths ()
+        ~meta ?task ?summary ?dir_file ?proof_dir ?output ~save ~wal_mode
+        ~desktop_notification ~no_failure ~update defs paths ()
     in
     let defs = Bin_utils.definitions_term
     and dyn =
       Arg.(value & flag & info ["progress"] ~doc:"print progress bar")
     and pp_results =
       Arg.(value & opt bool true & info ["pp-results"] ~doc:"print results as they are found")
-    and output = 
+    and output =
       Arg.(value & opt (some string) None & info ["o"; "output"] ~doc:"output database file")
     and save =
       Arg.(value & opt bool true & info ["save"] ~doc:"save results on disk")
@@ -63,11 +65,18 @@ module Run = struct
       Arg.(value & flag & info ["no-color"; "nc"] ~doc:"disable colored output")
     and summary =
       Arg.(value & opt (some string) None & info ["summary"] ~doc:"write summary in FILE")
+    and desktop_notification =
+      Arg.(value & opt bool true & info ["desktop-notification"; "dn"] ~doc:"send a desktop notification when the benchmarking is done (true by default)")
+    and no_failure =
+      Arg.(value & flag & info ["no-failure"; "nf"] ~doc:"don't fail if some provers give incorrect answers (contradictory to what was expected)")
+    and update =
+      Arg.(value & flag & info ["update"; "u"] ~doc:"if the output file already exists, overwrite it with the new one.")
     in
     Cmd.v (Cmd.info ~doc "run")
       (Term.(const aux $ j $ pp_results $ dyn $ paths
              $ dir_file $ proof_dir $ defs $ task $ timeout $ memory
-             $ meta $ provers $ csv $ summary $ no_color $ output $ save $ wal_mode))
+             $ meta $ provers $ csv $ summary $ no_color $ output $ save $ wal_mode
+             $ desktop_notification $ no_failure $ update))
 end
 
 module List_files = struct

src/core/Bin_utils.ml

@@ -67,7 +67,7 @@ let dump_summary ~summary results : unit =
            Format.fprintf out "%a@." Test_top_result.pp_compact results);
   end
 
-let check_res_an notify a : unit =
+let check_res_an ?(no_failure = false) notify a : unit =
   if List.for_all (fun (_,r) -> Test_analyze.is_ok r) a
   then (
     Notify.send notify "OK";
@@ -76,15 +76,15 @@ let check_res_an notify a : unit =
       List.fold_left (fun n (_,r) -> n + Test_analyze.num_bad r) 0 a
     in
     Notify.sendf notify "FAIL (%d failures)" n_fail;
-    Error.failf "FAIL (%d failures)" n_fail
+    if not no_failure then Error.failf "FAIL (%d failures)" n_fail
   )
 
-let check_compact_res notify (results:Test_compact_result.t) : unit =
-  check_res_an notify (results.Test_compact_result.cr_analyze)
+let check_compact_res ?(no_failure = false) notify (results:Test_compact_result.t) : unit =
+  check_res_an ~no_failure notify (results.Test_compact_result.cr_analyze)
 
-let check_res notify (results:Test_top_result.t) : unit =
+let check_res ?(no_failure = false) notify (results:Test_top_result.t) : unit =
   let a = Test_top_result.analyze results in
-  check_res_an notify a
+  check_res_an ~no_failure notify a
 
 let printbox_stat st : unit =
   let box_st = Test_stat.to_printbox_l st in

src/core/Exec_action.ml

@@ -47,6 +47,7 @@ module Exec_run_provers : sig
     ?on_done:(Test_compact_result.t -> unit) ->
     ?interrupted:(unit -> bool) ->
     ?output:string ->
+    ?update:bool ->
     uuid:Uuidm.t ->
     save:bool ->
     wal_mode:bool ->
@@ -155,7 +156,7 @@ end = struct
   let run ?(timestamp=Misc.now_s())
       ?(on_start=_nop) ?(on_solve = _nop) ?(on_start_proof_check=_nop)
       ?(on_proof_check = _nop) ?(on_done = _nop)
-      ?(interrupted=fun _->false) ?output
+      ?(interrupted=fun _->false) ?output ?(update = false)
       ~uuid ~save ~wal_mode
       (self:expanded) : _*_ =
     let start = Misc.now_s() in
@@ -165,9 +166,12 @@ end = struct
         let db_file =
           match output with
           | Some output ->
-              if Sys.file_exists output then
-                Error.failf "The file %s exists" output
-              else output
+            if Sys.file_exists output then
+              if update then (
+                Sys.remove output;
+                output
+              ) else Error.failf "The file %s exists" output
+            else output
           | None -> db_file_for_uuid ~timestamp uuid
         in
         Log.debug (fun k -> k"output database file %s" db_file);
@@ -487,7 +491,7 @@ module Git_checkout = struct
   let run (self:t) : unit =
     Error.guard (Error.wrapf "running action git-checkout '%s'" self.ref) @@ fun () ->
     let {Action.dir; ref; fetch_first; loc=_} = self in
-    with_chdir dir 
+    with_chdir dir
       (fun () ->
         begin match fetch_first with
         | Some Git_fetch -> run_cmd "git fetch"

src/core/Exec_action.mli

@@ -34,6 +34,7 @@ module Exec_run_provers : sig
     ?on_done:(Test_compact_result.t -> unit) ->
     ?interrupted:(unit -> bool) ->
     ?output:string ->
+    ?update:bool ->
     uuid:Uuidm.t ->
     save:bool ->
     wal_mode:bool ->