STM: number of slaves passed by the command line

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16839 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 20 insertions, 9 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 9f4e81408e..ec6469affe 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -47,6 +47,7 @@ let batch_mode = ref false
 
 let ide_slave_mode = ref false
 let coq_slave_mode = ref (-1)
+let coq_slaves_number = ref 1
 
 let debug = ref false
 
diff --git a/lib/flags.mli b/lib/flags.mli
index a5abca7a9f..5774f3ad41 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -14,6 +14,7 @@ val batch_mode : bool ref
 
 val ide_slave_mode : bool ref
 val coq_slave_mode : int ref
+val coq_slaves_number : int ref
 
 val debug : bool ref
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index ed5e92867d..1187f907e2 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -228,6 +228,11 @@ let get_bool opt = function
   | "no" -> false
   | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1
 
+let get_int opt n =
+  try int_of_string n
+  with Failure _ ->
+    prerr_endline ("Error: integer expected after option "^opt); exit 1
+
 let parse_args arglist =
   let args = ref arglist in
   let extras = ref [] in
@@ -260,6 +265,7 @@ let parse_args arglist =
     (* Options with one arg *)
     |"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ())
     |"-coq-slaves" -> Flags.coq_slave_mode := (get_slave_number (next ()))
+    |"-coq-slaves-j" -> Flags.coq_slaves_number := (get_int opt (next ()))
     |"-compat" -> Flags.compat_version := get_compat_version (next ())
     |"-compile" -> add_compile false (next ())
     |"-compile-verbose" -> add_compile true (next ())
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 51fa14ea46..8dc1734c72 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -634,25 +634,27 @@ end = struct (* {{{ *)
 
   module SlavesPool : sig
   
-    val init : ((unit -> in_channel * out_channel * int) -> unit) -> unit
+    val init : int -> ((unit -> in_channel * out_channel * int) -> unit) -> unit
     val is_empty : unit -> bool
     val n_slaves : unit -> int
   
   end = struct (* {{{ *)
   
-    let slave_manager = ref (None : Thread.t option)
+    let slave_managers = ref None
     
-    let is_empty () = Option.is_empty !slave_manager
-    let n_slaves () = if Option.is_empty !slave_manager then 0 else 1
+    let n_slaves () = match !slave_managers with
+      | None -> 0
+      | Some managers -> Array.length managers
+    let is_empty () = !slave_managers = None
 
-    let respawn () =
+    let respawn n () =
       let c2s_r, c2s_w = Unix.pipe () in
       let s2c_r, s2c_w = Unix.pipe () in
       Unix.set_close_on_exec c2s_w;
       Unix.set_close_on_exec s2c_r;
       let prog =  Sys.argv.(0) in
       let rec set_slave_opt = function
-        | [] -> ["-coq-slaves";"1"]
+        | [] -> ["-coq-slaves"; string_of_int n]
         | ("-ideslave"|"-emacs"|"-emacs-U")::tl -> set_slave_opt tl
         | ("-coq-slaves"
           |"-compile"
@@ -668,8 +670,9 @@ end = struct (* {{{ *)
         Unix.in_channel_of_descr s2c_r, Unix.out_channel_of_descr c2s_w, pid in
       s
 
-    let init manage_slave =
-      slave_manager := Some (Thread.create manage_slave respawn);
+    let init n manage_slave =
+      slave_managers := Some
+        (Array.init n (fun x -> Thread.create manage_slave (respawn (x+1))));
 
   end (* }}} *)
   
@@ -854,7 +857,7 @@ end = struct (* {{{ *)
       close_out oc;
       manage_slave respawn
 
-  let init () = SlavesPool.init manage_slave
+  let init () = SlavesPool.init !Flags.coq_slaves_number manage_slave
 
   let slave_ic = ref stdin
   let slave_oc = ref stdout