STM: code restructured to reuse task queue for tactics

8 files changed, 27 insertions, 18 deletions

diff --git a/lib/control.ml b/lib/control.ml
index 18176b843..cce9d3a9f 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -14,7 +14,7 @@ let steps = ref 0
 
 let are_we_threading = lazy (
   match !Flags.async_proofs_mode with
-  | Flags.APonParallel _ -> true
+  | Flags.APon -> true
   | _ -> false)
 
 let check_for_interrupt () =
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 27ed44724..e01844a48 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -65,7 +65,7 @@ type feedback_content =
   | GlobDef of Loc.t * string * string * string
   | ErrorMsg of Loc.t * string
   | InProgress of int
-  | SlaveStatus of int * string
+  | SlaveStatus of string * string
   | ProcessingInMaster
   | Goals of Loc.t * string
   | FileLoaded of string * string
@@ -90,7 +90,7 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
   | "errormsg", [loc;  s] -> ErrorMsg (to_loc loc, to_string s)
   | "inprogress", [n] -> InProgress (to_int n)
   | "slavestatus", [ns] ->
-       let n, s = to_pair to_int to_string ns in
+       let n, s = to_pair to_string to_string ns in
        SlaveStatus(n,s)
   | "goals", [loc;s] -> Goals (to_loc loc, to_string s)
   | "fileloaded", [dirpath; filename] ->
@@ -121,7 +121,7 @@ let of_feedback_content = function
   | InProgress n -> constructor "feedback_content" "inprogress" [of_int n]
   | SlaveStatus(n,s) ->
       constructor "feedback_content" "slavestatus"
-        [of_pair of_int of_string (n,s)]
+        [of_pair of_string of_string (n,s)]
   | Goals (loc,s) ->
       constructor "feedback_content" "goals" [of_loc loc;of_string s]
   | FileLoaded(dirpath, filename) ->
diff --git a/lib/feedback.mli b/lib/feedback.mli
index b3c0c8896..7e7b57625 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -40,7 +40,7 @@ type feedback_content =
   | GlobDef of Loc.t * string * string * string
   | ErrorMsg of Loc.t * string
   | InProgress of int
-  | SlaveStatus of int * string
+  | SlaveStatus of string * string
   | ProcessingInMaster
   | Goals of Loc.t * string
   | FileLoaded of string * string
diff --git a/lib/flags.ml b/lib/flags.ml
index 92824c9f5..4b323f611 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -48,18 +48,19 @@ let batch_mode = ref false
 type compilation_mode = BuildVo | BuildVi | Vi2Vo
 let compilation_mode = ref BuildVo
 
-type async_proofs = APoff | APonLazy | APonParallel of int
+type async_proofs = APoff | APonLazy | APon
 let async_proofs_mode = ref APoff
 let async_proofs_n_workers = ref 1
 let async_proofs_private_flags = ref None
 let async_proofs_always_delegate = ref false
 let async_proofs_never_reopen_branch = ref false
 let async_proofs_flags_for_workers = ref []
+let async_proofs_worker_id = ref "master"
 
 let async_proofs_is_worker () =
-  match !async_proofs_mode with
-  | APonParallel n -> n > 0
-  | _ -> false
+  !async_proofs_worker_id <> "master"
+let async_proofs_is_master () =
+  !async_proofs_mode = APon && !async_proofs_worker_id = "master"
 
 let debug = ref false
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 7f2b749b7..db1d8bcc4 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -15,14 +15,16 @@ val batch_mode : bool ref
 type compilation_mode = BuildVo | BuildVi | Vi2Vo
 val compilation_mode : compilation_mode ref
 
-type async_proofs = APoff | APonLazy | APonParallel of int
+type async_proofs = APoff | APonLazy | APon
 val async_proofs_mode : async_proofs ref
 val async_proofs_n_workers : int ref
 val async_proofs_private_flags : string option ref
 val async_proofs_is_worker : unit -> bool
+val async_proofs_is_master : unit -> bool
 val async_proofs_always_delegate : bool ref
 val async_proofs_never_reopen_branch : bool ref
 val async_proofs_flags_for_workers : string list ref
+val async_proofs_worker_id : string ref
 
 val debug : bool ref
 
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
index bec46901f..72887b21a 100644
--- a/lib/remoteCounter.ml
+++ b/lib/remoteCounter.ml
@@ -24,18 +24,14 @@ let new_counter ~name a ~incr ~build =
     (* - slaves must use a remote counter getter, not this one! *)
     (* - in the main process there is a race condition between slave
          managers (that are threads) and the main thread, hence the mutex *)
-    (match !Flags.async_proofs_mode with
-    | Flags.APonParallel n when n > 0 ->
-        Errors.anomaly(Pp.str"Slave processes must install remote counters");
-    | _ -> ());
+    if Flags.async_proofs_is_worker () then
+      Errors.anomaly(Pp.str"Slave processes must install remote counters");
     Mutex.lock m; let x = f () in Mutex.unlock m;
     build x in
   let getter = ref(mk_thsafe_getter (fun () -> !data := incr !!data; !!data)) in
   let installer f =
-    (match !Flags.async_proofs_mode with
-    | Flags.APoff | Flags.APonLazy | Flags.APonParallel 0 -> 
-      Errors.anomaly(Pp.str"Only slave processes can install a remote counter")
-    | _ -> ());
+    if not (Flags.async_proofs_is_worker ()) then
+      Errors.anomaly(Pp.str"Only slave processes can install a remote counter");
     getter := f in
   (fun () -> !getter ()), installer
 
diff --git a/lib/system.ml b/lib/system.ml
index 4188eb2b4..59260fbf6 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -295,3 +295,10 @@ let with_time time f x =
     let msg2 = if time then "" else " (failure)" in
     msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     raise e
+
+let process_id () =
+  if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id
+  else if Flags.async_proofs_is_master () then
+    Printf.sprintf "master:%d" (Thread.id (Thread.self ()))
+  else "master"
+    
diff --git a/lib/system.mli b/lib/system.mli
index 9cfb1456f..0569c7889 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -69,3 +69,6 @@ val time_difference : time -> time -> float (** in seconds *)
 val fmt_time_difference : time -> time -> Pp.std_ppcmds
 
 val with_time : bool -> ('a -> 'b) -> 'a -> 'b
+
+(** {6 Name of current process.} *)
+val process_id : unit -> string