[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.

8 files changed, 126 insertions, 52 deletions

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