Added prover quorum to project files and command line.

Author: alleystoughton

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,9 +310,9 @@ let main () =
 
           List.flatten [
             maxjobs; timeout; cpufactor; ppwidth;
-            provers; pragmas; checkall ; profile;
-            iterate; why3srv; why3     ; reloc  ;
-            noevict; boot   ; idirs    ;
+            provers; quorum ; pragmas  ; checkall;
+            profile; iterate; why3srv  ; why3    ;
+            reloc  ; noevict; boot     ; idirs   ;
           ]
         in
 
@@ -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;
@@ -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

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
 

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;
 }

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; }

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;