[flags] [stm] Reorganize flags.

We move the main async flags to the STM in preparation for
more state encapsulation.

There is still more work to do, in particular we should make some of
the defaults a parameter instead of a flag.

16 files changed, 159 insertions, 133 deletions

diff --git a/Makefile.build b/Makefile.build
index 39b793d2b..d548a8bd8 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -493,7 +493,7 @@ $(COQDOC): $(call bestobj, $(COQDOCCMO))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,,str unix)
 
-$(COQWORKMGR): $(call bestobj, lib/clib.cma stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo)
+$(COQWORKMGR): $(call bestobj, lib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,, $(SYSMOD))
 
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index cfc0e09a0..bd43d1ffc 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -13,7 +13,6 @@ open Util
 open Pp
 open Printer
 
-module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 module CompactedDecl = Context.Compacted.Declaration
 
@@ -517,7 +516,7 @@ let rec parse = function
 let () = Coqtop.toploop_init := (fun args ->
         let args = parse args in
         Flags.quiet := true;
-        CoqworkmgrApi.(init Flags.High);
+        CoqworkmgrApi.(init High);
         args)
 
 let () = Coqtop.toploop_run := loop
diff --git a/lib/control.ml b/lib/control.ml
index d936d7557..c6489938e 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -12,15 +12,12 @@ let interrupt = ref false
 
 let steps = ref 0
 
-let are_we_threading = lazy (
-  match !Flags.async_proofs_mode with
-  | Flags.APon -> true
-  | _ -> false)
+let enable_thread_delay = ref false
 
 let check_for_interrupt () =
   if !interrupt then begin interrupt := false; raise Sys.Break end;
   incr steps;
-  if !steps = 1000 && Lazy.force are_we_threading then begin
+  if !enable_thread_delay && !steps = 1000 then begin
     Thread.delay 0.001;
     steps := 0;
   end
diff --git a/lib/control.mli b/lib/control.mli
index f6c63ffb3..261b07693 100644
--- a/lib/control.mli
+++ b/lib/control.mli
@@ -8,6 +8,9 @@
 
 (** Global control of Coq. *)
 
+(** Will periodically call [Thread.delay] if set to true *)
+val enable_thread_delay : bool ref
+
 val interrupt : bool ref
 (** Coq interruption: set the following boolean reference to interrupt Coq
     (it eventually raises [Break], simulating a Ctrl-C) *)
diff --git a/lib/flags.ml b/lib/flags.ml
index ddc8f8482..b43d5f74d 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -35,36 +35,10 @@ let record_aux_file = ref false
 
 let test_mode = ref false
 
-type async_proofs = APoff | APonLazy | APon
-let async_proofs_mode = ref APoff
-type cache = Force
-let async_proofs_cache = ref None
-let async_proofs_n_workers = ref 1
-let async_proofs_n_tacworkers = ref 2
-let async_proofs_private_flags = ref None
-let async_proofs_full = ref false
-let async_proofs_never_reopen_branch = ref false
-let async_proofs_flags_for_workers = ref []
 let async_proofs_worker_id = ref "master"
-type priority = Low | High
-let async_proofs_worker_priority = ref Low
-let string_of_priority = function Low -> "low" | High -> "high"
-let priority_of_string = function
-  | "low" -> Low
-  | "high" -> High
-  | _ -> raise (Invalid_argument "priority_of_string")
-type tac_error_filter = [ `None | `Only of string list | `All ]
-let async_proofs_tac_error_resilience = ref (`Only [ "curly" ])
-let async_proofs_cmd_error_resilience = ref true
-
-let async_proofs_is_worker () =
-  !async_proofs_worker_id <> "master"
-let async_proofs_is_master () =
-  !async_proofs_mode = APon && !async_proofs_worker_id = "master"
-let async_proofs_delegation_threshold = ref 0.03
+let async_proofs_is_worker () = !async_proofs_worker_id <> "master"
 
 let debug = ref false
-let stm_debug = ref false
 
 let in_debugger = ref false
 let in_toplevel = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index c4afb8318..b82fe6128 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -21,35 +21,14 @@ val record_aux_file : bool ref
 val test_mode : bool ref
 
 (** Async-related flags *)
-type async_proofs = APoff | APonLazy | APon
-val async_proofs_mode : async_proofs ref
-type cache = Force
-val async_proofs_cache : cache option ref
-val async_proofs_n_workers : int ref
-val async_proofs_n_tacworkers : 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_full : 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
-type priority = Low | High
-val async_proofs_worker_priority : priority ref
-val string_of_priority : priority -> string
-val priority_of_string : string -> priority
-type tac_error_filter = [ `None | `Only of string list | `All ]
-val async_proofs_tac_error_resilience : tac_error_filter ref
-val async_proofs_cmd_error_resilience : bool ref
-val async_proofs_delegation_threshold : float ref
+val async_proofs_is_worker : unit -> bool
 
+(** Debug flags *)
 val debug : bool ref
 val in_debugger : bool ref
 val in_toplevel : bool ref
 
-(** Enable STM debugging *)
-val stm_debug : bool ref
-
 val profile : bool
 
 (* -ide_slave: printing will be more verbose, will affect stm caching *)
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 28c16a656..26aef5355 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -11,10 +11,10 @@ open Pp
 open Util
 
 let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp
-
 let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else ()
 
 type cancel_switch = bool ref
+let async_proofs_flags_for_workers = ref []
 
 module type Task = sig
 
@@ -117,12 +117,12 @@ module Make(T : Task) () = struct
     let name = Printf.sprintf "%s:%d" !T.name id in
     let proc, ic, oc =
       let rec set_slave_opt = function
-        | [] -> !Flags.async_proofs_flags_for_workers @
+        | [] -> !async_proofs_flags_for_workers @
                 ["-toploop"; !T.name^"top";
                  "-worker-id"; name;
                  "-async-proofs-worker-priority";
-                   Flags.string_of_priority !Flags.async_proofs_worker_priority]
-        | ("-ideslave"|"-emacs"|"-batch")::tl -> set_slave_opt tl
+                   CoqworkmgrApi.(string_of_priority !WorkerLoop.async_proofs_worker_priority)]
+        | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
         | ("-async-proofs" |"-toploop" |"-vio2vo"
           |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv"
           |"-compile" |"-compile-verbose"
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index ccd643deb..07689389f 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -6,6 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Default flags for workers *)
+val async_proofs_flags_for_workers : string list ref
+
 (** This file provides an API for defining and managing a queue of
     tasks to be done by external workers.
 
diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml
index 6d6a198c5..14fd97a6d 100644
--- a/stm/coqworkmgrApi.ml
+++ b/stm/coqworkmgrApi.ml
@@ -8,8 +8,15 @@
 
 let debug = false
 
+type priority = Low | High
+let string_of_priority = function Low -> "low" | High -> "high"
+let priority_of_string = function
+  | "low" -> Low
+  | "high" -> High
+  | _ -> raise (Invalid_argument "priority_of_string")
+
 type request =
-  | Hello of Flags.priority
+  | Hello of priority
   | Get of int
   | TryGet of int
   | GiveBack of int
@@ -36,8 +43,8 @@ let positive_int_of_string n =
 let parse_request s =
   if debug then Printf.eprintf "parsing '%s'\n" s;
   match Str.split (Str.regexp " ") (strip_r s) with
-  | [ "HELLO"; "LOW" ] -> Hello Flags.Low
-  | [ "HELLO"; "HIGH" ] -> Hello Flags.High
+  | [ "HELLO"; "LOW" ] -> Hello Low
+  | [ "HELLO"; "HIGH" ] -> Hello High
   | [ "GET"; n ] -> Get (positive_int_of_string n)
   | [ "TRYGET"; n ] -> TryGet (positive_int_of_string n)
   | [ "GIVEBACK"; n ] -> GiveBack (positive_int_of_string n)
@@ -57,8 +64,8 @@ let parse_response s =
   | _ -> raise ParseError
        
 let print_request = function
-  | Hello Flags.Low -> "HELLO LOW\n"
-  | Hello Flags.High -> "HELLO HIGH\n"
+  | Hello Low -> "HELLO LOW\n"
+  | Hello High -> "HELLO HIGH\n"
   | Get n -> Printf.sprintf "GET %d\n" n
   | TryGet n -> Printf.sprintf "TRYGET %d\n" n
   | GiveBack n -> Printf.sprintf "GIVEBACK %d\n" n
@@ -106,8 +113,7 @@ let with_manager f g =
 
 let get n =
   with_manager
-  (fun () ->
-    min n (min !Flags.async_proofs_n_workers !Flags.async_proofs_n_tacworkers))
+  (fun () -> n)
   (fun cin cout ->
     output_string cout (print_request (Get n));
     flush cout;
@@ -118,10 +124,7 @@ let get n =
 
 let tryget n =
   with_manager
-  (fun () ->
-    Some
-     (min n
-       (min !Flags.async_proofs_n_workers !Flags.async_proofs_n_tacworkers)))
+  (fun () -> Some n)
   (fun cin cout ->
     output_string cout (print_request (TryGet n));
     flush cout;
diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli
index 70d4173ae..953903810 100644
--- a/stm/coqworkmgrApi.mli
+++ b/stm/coqworkmgrApi.mli
@@ -8,9 +8,13 @@
 
 (* High level api for clients of the service (like coqtop) *)
 
+type priority = Low | High
+val string_of_priority : priority -> string
+val priority_of_string : string -> priority
+
 (* Connects to a work manager if any. If no worker manager, then
    -async-proofs-j and -async-proofs-tac-j are used *)
-val init : Flags.priority -> unit
+val init : priority -> unit
 
 (* blocking *)
 val get : int -> int
@@ -21,7 +25,7 @@ val giveback : int -> unit
 
 (* Low level *)
 type request =
-  | Hello of Flags.priority
+  | Hello of priority
   | Get of int
   | TryGet of int
   | GiveBack of int
diff --git a/stm/stm.ml b/stm/stm.ml
index 877263096..b79a4a939 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -8,13 +8,13 @@
 
 (* enable in case of stm problems  *)
 (* let stm_debug () = !Flags.debug *)
-let stm_debug () = !Flags.stm_debug
+let stm_debug = ref false
 
 let stm_pr_err s  = Format.eprintf "%s] %s\n%!"     (Spawned.process_id ()) s
 let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp
 
-let stm_prerr_endline s = if stm_debug () then begin stm_pr_err (s ()) end else ()
-let stm_pperr_endline s = if stm_debug () then begin stm_pp_err (s ()) end else ()
+let stm_prerr_endline s = if !stm_debug then begin stm_pr_err (s ()) end else ()
+let stm_pperr_endline s = if !stm_debug then begin stm_pp_err (s ()) end else ()
 
 let stm_prerr_debug   s = if !Flags.debug then begin stm_pr_err (s ()) end else ()
 
@@ -23,6 +23,35 @@ open CErrors
 open Feedback
 open Vernacexpr
 
+module AsyncOpts = struct
+
+  let async_proofs_n_workers = ref 1
+  let async_proofs_n_tacworkers = ref 2
+
+  type cache = Force
+  let async_proofs_cache : cache option ref = ref None
+
+  type async_proofs = APoff | APonLazy | APon
+  let async_proofs_mode = ref APoff
+
+  let async_proofs_private_flags = ref None
+  let async_proofs_full = ref false
+  let async_proofs_never_reopen_branch = ref false
+
+  type tac_error_filter = [ `None | `Only of string list | `All ]
+  let async_proofs_tac_error_resilience = ref (`Only [ "curly" ])
+  let async_proofs_cmd_error_resilience = ref true
+
+  let async_proofs_delegation_threshold = ref 0.03
+
+end
+
+open AsyncOpts
+
+let async_proofs_is_master () =
+  !async_proofs_mode = APon &&
+  !Flags.async_proofs_worker_id = "master"
+
 (* Protect against state changes *)
 let stm_purify f x =
   let st = Vernacstate.freeze_interp_state `No in
@@ -352,7 +381,7 @@ end = struct (* {{{ *)
 
        In case you are hitting the race enable stm_debug.
     *)
-    if stm_debug () then Flags.we_are_parsing := false;
+    if !stm_debug then Flags.we_are_parsing := false;
 
     let fname =
       "stm_" ^ Str.global_replace (Str.regexp " ") "_" (Spawned.process_id ()) in
@@ -529,7 +558,7 @@ end = struct (* {{{ *)
     | None -> raise Vcs_aux.Expired
   let set_state id s =
     (get_info id).state <- s;
-    if Flags.async_proofs_is_master () then Hooks.(call state_ready id)
+    if async_proofs_is_master () then Hooks.(call state_ready id)
   let get_state id = (get_info id).state
   let reached id =
     let info = get_info id in
@@ -1105,7 +1134,7 @@ end = struct (* {{{ *)
              " the \"-async-proofs-cache force\" option to Coq."))
 
   let undo_vernac_classifier v =
-    if VCS.is_interactive () = `No && !Flags.async_proofs_cache <> Some Flags.Force
+    if VCS.is_interactive () = `No && !async_proofs_cache <> Some Force
     then undo_costly_in_batch_mode v;
     try
       match v with
@@ -1241,7 +1270,7 @@ let prev_node { id } =
 let cur_node id = mk_doc_node id (VCS.visit id)
 
 let is_block_name_enabled name =
-  match !Flags.async_proofs_tac_error_resilience with
+  match !async_proofs_tac_error_resilience with
   | `None -> false
   | `All -> true
   | `Only l -> List.mem name l
@@ -1249,7 +1278,7 @@ let is_block_name_enabled name =
 let detect_proof_block id name =
   let name = match name with None -> "indent" | Some x -> x in
   if is_block_name_enabled name &&
-     (Flags.async_proofs_is_master () || Flags.async_proofs_is_worker ())
+     (async_proofs_is_master () || Flags.async_proofs_is_worker ())
   then (
   match cur_node id with
   | None -> ()
@@ -1351,7 +1380,7 @@ end = struct (* {{{ *)
   let task_match age t =
     match age, t with
     | Fresh, BuildProof { t_states } ->
-        not !Flags.async_proofs_full ||
+        not !async_proofs_full ||
         List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) t_states
     | Old my_states, States l ->
         List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l
@@ -1388,7 +1417,7 @@ end = struct (* {{{ *)
         feedback (InProgress ~-1);
         t_assign (`Val pl);
         record_pb_time ?loc:t_loc t_name time;
-        if !Flags.async_proofs_full || t_drop
+        if !async_proofs_full || t_drop
         then `Stay(t_states,[States t_states])
         else `End
     | Fresh, BuildProof { t_assign; t_loc; t_name; t_states },
@@ -1562,8 +1591,8 @@ end = struct (* {{{ *)
 
   let queue = ref None
   let init () =
-    if Flags.async_proofs_is_master () then
-      queue := Some (TaskQueue.create !Flags.async_proofs_n_workers)
+    if async_proofs_is_master () then
+      queue := Some (TaskQueue.create !async_proofs_n_workers)
     else
       queue := Some (TaskQueue.create 0)
 
@@ -2028,7 +2057,7 @@ end = struct (* {{{ *)
       QueryTask.({ t_where = prev; t_for = id; t_what = q }) ~cancel_switch
 
   let init () = queue := Some (TaskQueue.create
-    (if !Flags.async_proofs_full then 1 else 0))
+    (if !async_proofs_full then 1 else 0))
 
 end (* }}} *)
 
@@ -2051,9 +2080,9 @@ let async_policy () =
     (VCS.is_vio_doc () || !async_proofs_mode <> APoff)
 
 let delegate name =
-     get_hint_bp_time name >= !Flags.async_proofs_delegation_threshold
+     get_hint_bp_time name >= !async_proofs_delegation_threshold
   || VCS.is_vio_doc ()
-  || !Flags.async_proofs_full
+  || !async_proofs_full
 
 let warn_deprecated_nested_proofs =
   CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated"
@@ -2150,7 +2179,7 @@ let collect_proof keep cur hd brkind id =
        let rc = collect (Some cur) [] id in
        if is_empty rc then make_sync `AlreadyEvaluated rc
        else if (keep == VtKeep || keep == VtKeepAsAxiom) &&
-          (not(State.is_cached_and_valid id) || !Flags.async_proofs_full)
+          (not(State.is_cached_and_valid id) || !async_proofs_full)
        then check_policy rc
        else make_sync `AlreadyEvaluated rc
 
@@ -2232,9 +2261,9 @@ let known_state ?(redefine_qed=false) ~cache id =
 
   (* Absorb tactic errors from f () *)
   let resilient_tactic id blockname f =
-    if !Flags.async_proofs_tac_error_resilience = `None ||
-       (Flags.async_proofs_is_master () &&
-        !Flags.async_proofs_mode = Flags.APoff)
+    if !async_proofs_tac_error_resilience = `None ||
+       (async_proofs_is_master () &&
+        !async_proofs_mode = APoff)
     then f ()
     else
       try f ()
@@ -2243,9 +2272,9 @@ let known_state ?(redefine_qed=false) ~cache id =
         error_absorbing_tactic id blockname ie in
   (* Absorb errors from f x *)
   let resilient_command f x =
-    if not !Flags.async_proofs_cmd_error_resilience ||
-       (Flags.async_proofs_is_master () &&
-        !Flags.async_proofs_mode = Flags.APoff)
+    if not !async_proofs_cmd_error_resilience ||
+       (async_proofs_is_master () &&
+        !async_proofs_mode = APoff)
     then f x
     else
       try f x
@@ -2287,10 +2316,10 @@ let known_state ?(redefine_qed=false) ~cache id =
             resilient_tactic id cblock (fun () ->
               reach ~cache:`Shallow view.next;
               Partac.vernac_interp ~solve ~abstract ~cancel_switch
-                !Flags.async_proofs_n_tacworkers view.next id x)
+                !async_proofs_n_tacworkers view.next id x)
           ), cache, true
       | `Cmd { cast = x; cqueue = `QueryQueue cancel_switch }
-        when Flags.async_proofs_is_master () -> (fun () ->
+        when async_proofs_is_master () -> (fun () ->
             reach view.next;
             Query.vernac_interp ~cancel_switch view.next id x
           ), cache, false
@@ -2304,10 +2333,10 @@ let known_state ?(redefine_qed=false) ~cache id =
 	    if eff then update_global_env ()
           ), (if eff then `Yes else cache), true
       | `Cmd { cast = x; ceff = eff } -> (fun () ->
-          (match !Flags.async_proofs_mode with
-           | Flags.APon | Flags.APonLazy ->
+          (match !async_proofs_mode with
+           | APon | APonLazy ->
              resilient_command reach view.next
-           | Flags.APoff -> reach view.next);
+           | APoff -> reach view.next);
           let st = Vernacstate.freeze_interp_state `No in
           ignore(stm_vernac_interp id st x);
           if eff then update_global_env ()
@@ -2434,7 +2463,7 @@ let known_state ?(redefine_qed=false) ~cache id =
           ), cache, true
     in
     let cache_step =
-      if !Flags.async_proofs_cache = Some Flags.Force then `Yes
+      if !async_proofs_cache = Some Force then `Yes
       else cache_step in
     State.define ?safe_id
       ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id;
@@ -2465,6 +2494,7 @@ let doc_type_module_name (std : stm_doc_type) =
 *)
 
 let init_core () =
+  if !async_proofs_mode = APon then Control.enable_thread_delay := true;
   State.register_root_state ()
 
 let new_doc { doc_type ; require_libs } =
@@ -2503,10 +2533,10 @@ let new_doc { doc_type ; require_libs } =
   State.define ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial;
   Backtrack.record ();
   Slaves.init ();
-  if Flags.async_proofs_is_master () then begin
+  if async_proofs_is_master () then begin
     stm_prerr_endline (fun () -> "Initializing workers");
     Query.init ();
-    let opts = match !Flags.async_proofs_private_flags with
+    let opts = match !async_proofs_private_flags with
       | None -> []
       | Some s -> Str.split_delim (Str.regexp ",") s in
     begin try
@@ -2705,7 +2735,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
       | VtQuery (true, route), w ->
           let id = VCS.new_node ~id:newtip () in
           let queue =
-            if !Flags.async_proofs_full then `QueryQueue (ref false)
+            if !async_proofs_full then `QueryQueue (ref false)
             else if VCS.is_vio_doc () &&
                     VCS.((get_branch head).kind = `Master) &&
                     may_pierce_opaque x
@@ -2870,7 +2900,7 @@ let parse_sentence ~doc sid pa =
       (str "Currently, the parsing api only supports parsing at the tip of the document." ++ fnl () ++
        str "You wanted to parse at: "  ++ str (Stateid.to_string sid) ++
        str " but the current tip is: " ++ str (Stateid.to_string cur_tip)) ;
-  if not (Stateid.equal sid real_tip) && !Flags.debug && stm_debug () then
+  if not (Stateid.equal sid real_tip) && !Flags.debug && !stm_debug then
     Feedback.msg_debug
       (str "Warning, the real tip doesn't match the current tip." ++
        str "You wanted to parse at: "  ++ str (Stateid.to_string sid) ++
@@ -3029,7 +3059,7 @@ let edit_at ~doc id =
     VCS.delete_boxes_of id;
     VCS.gc ();
     VCS.print ();
-    if not !Flags.async_proofs_full then
+    if not !async_proofs_full then
       Reach.known_state ~cache:(VCS.is_interactive ()) id;
     VCS.checkout_shallowest_proof_branch ();
     `NewTip in
@@ -3045,7 +3075,7 @@ let edit_at ~doc id =
       | _, Some _, None -> assert false
       | false, Some { qed = qed_id ; lemma = start }, Some(mode,bn) ->
           let tip = VCS.cur_tip () in
-          if has_failed qed_id && is_pure qed_id && not !Flags.async_proofs_never_reopen_branch
+          if has_failed qed_id && is_pure qed_id && not !async_proofs_never_reopen_branch
           then reopen_branch start id mode qed_id tip bn
           else backto id (Some bn)
       | true, Some { qed = qed_id }, Some(mode,bn) ->
diff --git a/stm/stm.mli b/stm/stm.mli
index 9fd35a0d3..ef95be0e4 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -225,3 +225,30 @@ val state_of_id : doc:doc ->
 (* Queries for backward compatibility *)
 val current_proof_depth : doc:doc -> int
 val get_all_proof_names : doc:doc -> Id.t list
+
+(** Enable STM debugging *)
+val stm_debug : bool ref
+
+(* Flags *)
+module AsyncOpts : sig
+
+  (* Defaults for worker creation *)
+  val async_proofs_n_workers : int ref
+  val async_proofs_n_tacworkers : int ref
+
+  type async_proofs = APoff | APonLazy | APon
+  val async_proofs_mode : async_proofs ref
+
+  type cache = Force
+  val async_proofs_cache : cache option ref
+
+  val async_proofs_private_flags : string option ref
+  val async_proofs_full : bool ref
+  val async_proofs_never_reopen_branch : bool ref
+
+  type tac_error_filter = [ `None | `Only of string list | `All ]
+  val async_proofs_tac_error_resilience : tac_error_filter ref
+  val async_proofs_cmd_error_resilience : bool ref
+  val async_proofs_delegation_threshold : float ref
+
+end
diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml
index 64121eb3d..704119186 100644
--- a/stm/workerLoop.ml
+++ b/stm/workerLoop.ml
@@ -6,6 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Default priority *)
+open CoqworkmgrApi
+let async_proofs_worker_priority = ref Low
+
 let rec parse = function
   | "--xml_format=Ppcmds" :: rest -> parse rest
   | x :: rest -> x :: parse rest
@@ -15,5 +19,5 @@ let loop init args =
   let args = parse args in
   Flags.quiet := true;
   init ();
-  CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
+  CoqworkmgrApi.init !async_proofs_worker_priority;
   args
diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli
index 53f745935..da2e6fe0c 100644
--- a/stm/workerLoop.mli
+++ b/stm/workerLoop.mli
@@ -6,4 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Default priority *)
+val async_proofs_worker_priority : CoqworkmgrApi.priority ref
+
 val loop : (unit -> unit) -> string list -> string list
diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml
index e1d1c60d7..f4777c4fb 100644
--- a/tools/coqworkmgr.ml
+++ b/tools/coqworkmgr.ml
@@ -14,7 +14,7 @@ type party = {
           sock     : Unix.file_descr;
           cout     : out_channel;
   mutable tokens   : int;
-          priority : Flags.priority;
+          priority : priority;
 }
 
 let answer party msg =
@@ -42,10 +42,10 @@ end = struct
   let is_empty q = !q = []
   let rec split acc = function
     | [] -> List.rev acc, []
-    | (_, { priority = Flags.Low }) :: _ as l -> List.rev acc, l
+    | (_, { priority = Low }) :: _ as l -> List.rev acc, l
     | x :: xs -> split (x :: acc) xs
   let push (_,{ priority } as item) q =
-    if priority = Flags.Low then q := !q @ [item]
+    if priority = Low then q := !q @ [item]
     else
       let high, low = split [] !q in
       q := high @ (item :: low)
@@ -148,7 +148,7 @@ let check_alive s =
   | Some s ->
       let cout = Unix.out_channel_of_descr s in
       set_binary_mode_out cout true;
-      output_string cout (print_request (Hello Flags.Low)); flush cout;
+      output_string cout (print_request (Hello Low)); flush cout;
       output_string cout (print_request Ping); flush cout;
       begin match Unix.select [s] [] [] 1.0 with
       | [s],_,_ ->
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 553da2dc0..6048dae3b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -71,7 +71,7 @@ let init_color () =
 
 let toploop_init = ref begin fun x ->
   let () = init_color () in
-  let () = CoqworkmgrApi.(init !Flags.async_proofs_worker_priority) in
+  let () = CoqworkmgrApi.init !WorkerLoop.async_proofs_worker_priority in
   x
   end
 
@@ -529,18 +529,18 @@ let print_config = ref false
 let print_tags = ref false
 
 let get_priority opt s =
-  try Flags.priority_of_string s
+  try CoqworkmgrApi.priority_of_string s
   with Invalid_argument _ ->
     prerr_endline ("Error: low/high expected after "^opt); exit 1
 
-let get_async_proofs_mode opt = function
-  | "no" | "off" -> Flags.APoff
-  | "yes" | "on" -> Flags.APon
-  | "lazy" -> Flags.APonLazy
+let get_async_proofs_mode opt = let open Stm.AsyncOpts in function
+  | "no" | "off" -> APoff
+  | "yes" | "on" -> APon
+  | "lazy" -> APonLazy
   | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1
 
 let get_cache opt = function
-  | "force" -> Some Flags.Force
+  | "force" -> Some Stm.AsyncOpts.Force
   | _ -> prerr_endline ("Error: force expected after "^opt); exit 1
 
 
@@ -649,23 +649,23 @@ let parse_args arglist =
     (* Options with one arg *)
     |"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ())
     |"-async-proofs" ->
-        Flags.async_proofs_mode := get_async_proofs_mode opt (next())
+        Stm.AsyncOpts.async_proofs_mode := get_async_proofs_mode opt (next())
     |"-async-proofs-j" ->
-        Flags.async_proofs_n_workers := (get_int opt (next ()))
+        Stm.AsyncOpts.async_proofs_n_workers := (get_int opt (next ()))
     |"-async-proofs-cache" ->
-        Flags.async_proofs_cache := get_cache opt (next ())
+        Stm.AsyncOpts.async_proofs_cache := get_cache opt (next ())
     |"-async-proofs-tac-j" ->
-        Flags.async_proofs_n_tacworkers := (get_int opt (next ()))
+        Stm.AsyncOpts.async_proofs_n_tacworkers := (get_int opt (next ()))
     |"-async-proofs-worker-priority" ->
-        Flags.async_proofs_worker_priority := get_priority opt (next ())
+        WorkerLoop.async_proofs_worker_priority := get_priority opt (next ())
     |"-async-proofs-private-flags" ->
-        Flags.async_proofs_private_flags := Some (next ());
+        Stm.AsyncOpts.async_proofs_private_flags := Some (next ());
     |"-async-proofs-tactic-error-resilience" ->
-        Flags.async_proofs_tac_error_resilience := get_error_resilience opt (next ())
+        Stm.AsyncOpts.async_proofs_tac_error_resilience := get_error_resilience opt (next ())
     |"-async-proofs-command-error-resilience" ->
-        Flags.async_proofs_cmd_error_resilience := get_bool opt (next ())
+        Stm.AsyncOpts.async_proofs_cmd_error_resilience := get_bool opt (next ())
     |"-async-proofs-delegation-threshold" ->
-        Flags.async_proofs_delegation_threshold:= get_float opt (next ())
+        Stm.AsyncOpts.async_proofs_delegation_threshold:= get_float opt (next ())
     |"-worker-id" -> set_worker_id opt (next ())
     |"-compat" ->
         let v = G_vernac.parse_compat_version ~allow_old:false (next ()) in
@@ -705,9 +705,9 @@ let parse_args arglist =
     |"-async-queries-always-delegate"
     |"-async-proofs-always-delegate"
     |"-async-proofs-full" ->
-        Flags.async_proofs_full := true;
+        Stm.AsyncOpts.async_proofs_full := true;
     |"-async-proofs-never-reopen-branch" ->
-        Flags.async_proofs_never_reopen_branch := true;
+        Stm.AsyncOpts.async_proofs_never_reopen_branch := true;
     |"-batch" -> set_batch_mode ()
     |"-test-mode" -> Flags.test_mode := true
     |"-beautify" -> Flags.beautify := true
@@ -716,7 +716,7 @@ let parse_args arglist =
     |"-color" -> set_color (next ())
     |"-config"|"--config" -> print_config := true
     |"-debug" -> Coqinit.set_debug ()
-    |"-stm-debug" -> Flags.stm_debug := true
+    |"-stm-debug" -> Stm.stm_debug := true
     |"-emacs" -> set_emacs ()
     |"-filteropts" -> filter_opts := true
     |"-h"|"-H"|"-?"|"-help"|"--help" -> usage !batch_mode