diff --git a/src/ec.ml b/src/ec.ml index ada7602b5..2cd488295 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -249,6 +249,11 @@ let main () = |> List.map (fun prover -> ["-p"; prover]) |> List.flatten in + let quorum = + input.runo_provers.prvo_quorum + |> omap (fun i -> ["-quorum"; string_of_int i]) + |> odfl [] in + let pragmas = input.runo_provers.prvo_pragmas |> List.map (fun pragmas -> ["-pragmas"; pragmas]) @@ -305,7 +310,7 @@ let main () = List.flatten [ maxjobs; timeout; cpufactor; ppwidth; - provers; pragmas; checkall ; profile; + provers; quorum; pragmas; checkall ; profile; iterate; why3srv; why3 ; reloc ; noevict; boot ; idirs ; ] @@ -434,7 +439,7 @@ let main () = let push_message (trace : trace1 list) msg = match trace with | [] -> - [push1_message trace0 msg] + [push1_message trace0 msg] | trace1 :: trace -> push1_message trace1 msg :: trace end @@ -584,6 +589,7 @@ let main () = prvo_timeout = None; prvo_cpufactor = None; prvo_provers = None; + prvo_quorum = None; prvo_pragmas = []; prvo_ppwidth = None; prvo_checkall = false; @@ -644,7 +650,7 @@ let main () = msg in String.concat "\n" (List.rev_map for1 trace1.messages) in (trace1.position, EcEco.{ goals; messages; }) - in List.rev_map mktrace1 trace in + in List.rev_map mktrace1 trace in EcEco.{ eco_root = EcEco.{ @@ -734,6 +740,7 @@ let main () = EcCommands.cm_cpufactor = odfl 1 (state.prvopts.prvo_cpufactor); EcCommands.cm_nprovers = odfl 4 (state.prvopts.prvo_maxjobs); EcCommands.cm_provers = state.prvopts.prvo_provers; + EcCommands.cm_quorum = state.prvopts.prvo_quorum; EcCommands.cm_profile = state.prvopts.prvo_profile; EcCommands.cm_iterate = state.prvopts.prvo_iterate; } in diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 474eab888..4910def1f 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -827,6 +827,7 @@ type checkmode = { cm_cpufactor : int; cm_nprovers : int; cm_provers : string list option; + cm_quorum : int option; cm_profile : bool; cm_iterate : bool; } @@ -839,6 +840,7 @@ let initial ~checkmode ~boot ~checkproof = EcScope.Prover.po_cpufactor = Some checkmode.cm_cpufactor; EcScope.Prover.po_nprovers = Some checkmode.cm_nprovers; EcScope.Prover.po_provers = (checkmode.cm_provers, []); + EcScope.Prover.po_quorum = checkmode.cm_quorum; EcScope.Prover.pl_iterate = Some (checkmode.cm_iterate); } in diff --git a/src/ecCommands.mli b/src/ecCommands.mli index e411b99d6..56440bfa9 100644 --- a/src/ecCommands.mli +++ b/src/ecCommands.mli @@ -20,6 +20,7 @@ type checkmode = { cm_cpufactor: int; cm_nprovers : int; cm_provers : string list option; + cm_quorum : int option; cm_profile : bool; cm_iterate : bool; } diff --git a/src/ecOptions.ml b/src/ecOptions.ml index 52a4d6e66..0a4787516 100644 --- a/src/ecOptions.ml +++ b/src/ecOptions.ml @@ -60,6 +60,7 @@ and prv_options = { prvo_timeout : int option; prvo_cpufactor : int option; prvo_provers : string list option; + prvo_quorum : int option; prvo_pragmas : string list; prvo_ppwidth : int option; prvo_checkall : bool; @@ -86,6 +87,7 @@ type ini_options = { ini_why3 : string option; ini_ovrevict : string list; ini_provers : string list; + ini_quorum : int option; ini_timeout : int option; ini_idirs : (string option * string) list; ini_rdirs : (string option * string) list; @@ -107,6 +109,8 @@ module Ini : sig val get_provers : ini_context -> string list + val get_quorum : ini_context -> int option + val get_timeout : ini_context -> int option val get_idirs : ini_context -> (string option * string) list @@ -122,6 +126,8 @@ module Ini : sig val get_all_provers : ini_context list -> string list + val get_all_quorum : ini_context list -> int option + val get_all_timeout : ini_context list -> int option val get_all_idirs : ini_context list -> (string option * string) list @@ -153,6 +159,9 @@ end = struct let get_provers (ini : ini_context) = ini.inic_ini.ini_provers + let get_quorum (ini : ini_context) = + ini.inic_ini.ini_quorum + let get_timeout (ini : ini_context) = ini.inic_ini.ini_timeout @@ -179,6 +188,9 @@ end = struct let get_all_provers (ini : ini_context list) = List.flatten (List.map get_provers ini) + let get_all_quorum (ini : ini_context list) = + List.find_map_opt get_quorum ini + let get_all_timeout (ini : ini_context list) = List.find_map_opt get_timeout ini @@ -391,6 +403,7 @@ let specs = { ("provers", "Options related to provers", [ `Spec ("p" , `String, "Add a prover to the set of provers"); `Spec ("max-provers", `Int , "Maximum number of prover running in the same time"); + `Spec ("quorum", `Int , "Set prover quorum"); `Spec ("timeout" , `Int , "Set the SMT timeout"); `Spec ("cpu-factor" , `Int , "Set the timeout CPU factor"); `Spec ("check-all" , `Flag , "Force checking all files"); @@ -509,6 +522,11 @@ let prv_options_of_values ini values = end; prvo_cpufactor = get_int "cpu-factor" values; prvo_provers = provers; + prvo_quorum = begin + match get_int "quorum" values with + | None -> Ini.get_all_quorum ini + | Some _ as i -> i + end; prvo_pragmas = get_string_list "pragmas" values; prvo_ppwidth = begin match get_int "pp-width" values with @@ -729,6 +747,7 @@ let read_ini_file (filename : string) = ini_why3 = tryget "why3conf"; ini_ovrevict = trylist "no-evict"; ini_provers = trylist "provers" ; + ini_quorum = tryint "quorum" ; ini_timeout = tryint "timeout" ; ini_idirs = List.map parse_idir (trylist "idirs"); ini_rdirs = List.map parse_idir (trylist "rdirs"); } in @@ -737,6 +756,7 @@ let read_ini_file (filename : string) = ini_why3 = omap expand ini.ini_why3; ini_ovrevict = ini.ini_ovrevict; ini_provers = ini.ini_provers; + ini_quorum = ini.ini_quorum; ini_timeout = ini.ini_timeout; ini_idirs = ini.ini_idirs; ini_rdirs = ini.ini_rdirs; } diff --git a/src/ecOptions.mli b/src/ecOptions.mli index 7ac81ec0a..0feb9f616 100644 --- a/src/ecOptions.mli +++ b/src/ecOptions.mli @@ -56,6 +56,7 @@ and prv_options = { prvo_timeout : int option; prvo_cpufactor : int option; prvo_provers : string list option; + prvo_quorum : int option; prvo_pragmas : string list; prvo_ppwidth : int option; prvo_checkall : bool; @@ -82,6 +83,7 @@ type ini_options = { ini_why3 : string option; ini_ovrevict : string list; ini_provers : string list; + ini_quorum : int option; ini_timeout : int option; ini_idirs : (string option * string) list; ini_rdirs : (string option * string) list;