Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Activate the WAL mode after creating the database file #54

Merged
merged 3 commits into from
Nov 1, 2022
Merged

Activate the WAL mode after creating the database file #54

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
978104d
Activate the WAL mode after creating the database file
Halbaroth Oct 31, 2022
437c77f
Add a cli option to turn on the WAL mode
Halbaroth Nov 1, 2022
78e65b5
Use a flag for the option
Halbaroth Nov 1, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions src/bin/Run_main.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
?j ?timestamp ?pp_results ?dyn ?limits ?proof_dir ?output ~notify ~uuid ~save ~wal_mode
(defs: Definitions.t) (r:Action.run_provers)
: (_ * Test_compact_result.t) =
begin
Expand All @@ -22,7 +22,7 @@ let execute_run_prover_action
Error.guard (Error.wrapf "running %d tests" len) @@ fun () ->
Exec_action.Exec_run_provers.run ~uuid ?timestamp
~interrupted:(fun () -> CCLock.get interrupted)
~on_solve:progress#on_res ~save
~on_solve:progress#on_res ~save ~wal_mode
~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
Expand All @@ -36,7 +36,7 @@ type top_task =
| TT_other of Action.t

let main ?j ?pp_results ?dyn ?timeout ?memory ?csv ?(provers=[])
?meta:_ ?summary ?task ?dir_file ?proof_dir ?output ?(save=true)
?meta:_ ?summary ?task ?dir_file ?proof_dir ?output ?(save=true) ?(wal_mode=false)
(defs:Definitions.t) paths () : unit =
Log.info
(fun k->k"run-main.main for paths %a" (Misc.pp_list Misc.Pp.pp_str) paths);
Expand Down Expand Up @@ -93,7 +93,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
~uuid ?pp_results ?proof_dir ?dyn:progress ~limits ?j ?output ~notify ~timestamp ~save ~wal_mode
defs run_provers_action
in
if CCOpt.is_some csv then (
Expand Down
8 changes: 5 additions & 3 deletions src/bin/benchpress_bin.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,12 +18,12 @@ 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 =
meta provers csv summary no_color output save wal_mode =
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 defs paths ()
~meta ?task ?summary ?dir_file ?proof_dir ?output ~save ~wal_mode defs paths ()
in
let defs = Bin_utils.definitions_term
and dyn =
Expand All @@ -34,6 +34,8 @@ module Run = struct
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")
and wal_mode =
Arg.(value & flag & info ["wal"] ~doc:"turn on the journal WAL mode")
and dir_file =
Arg.(value & opt (some string) None & info ["F"] ~doc:"file containing a list of files")
and proof_dir =
Expand Down Expand Up @@ -65,7 +67,7 @@ module Run = struct
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))
$ meta $ provers $ csv $ summary $ no_color $ output $ save $ wal_mode))
end

module List_files = struct
Expand Down
10 changes: 8 additions & 2 deletions src/core/Exec_action.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@ module Exec_run_provers : sig
?output:string ->
uuid:Uuidm.t ->
save:bool ->
wal_mode:bool ->
expanded ->
Test_top_result.t lazy_t * Test_compact_result.t
(** Run the given prover(s) on the given problem set, obtaining results
Expand Down Expand Up @@ -155,7 +156,7 @@ end = struct
?(on_start=_nop) ?(on_solve = _nop) ?(on_start_proof_check=_nop)
?(on_proof_check = _nop) ?(on_done = _nop)
?(interrupted=fun _->false) ?output
~uuid ~save
~uuid ~save ~wal_mode
(self:expanded) : _*_ =
let start = Misc.now_s() in
(* prepare DB *)
Expand All @@ -170,7 +171,12 @@ end = struct
| None -> db_file_for_uuid ~timestamp uuid
in
Log.debug (fun k -> k"output database file %s" db_file);
Sqlite3.db_open ~mutex:`FULL db_file
let db = Sqlite3.db_open ~mutex:`FULL db_file in
if wal_mode then
match Db.exec0 db "pragma journal_mode=WAL;" with
| Ok _ -> db
| Error rc -> Error.raise (Misc.err_of_db rc)
else db
) else
Sqlite3.db_open ":memory:"
in
Expand Down
1 change: 1 addition & 0 deletions src/core/Exec_action.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@ module Exec_run_provers : sig
?output:string ->
uuid:Uuidm.t ->
save:bool ->
wal_mode:bool ->
expanded ->
Test_top_result.t lazy_t * Test_compact_result.t
(** Run the given prover(s) on the given problem set, obtaining results
Expand Down