[stm] Move options to a per-document record.

We gather (almost) all the STM options in a record, now set at
document creation time.

This is refactoring is convenient for some other ongoing
functionalization work.

3 files changed, 146 insertions, 83 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 5f4fe6565..07d8b39bd 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -26,31 +26,50 @@ 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
+  type tac_error_filter = [ `None | `Only of string list | `All ]
 
-  let async_proofs_private_flags = ref None
-  let async_proofs_full = ref false
-  let async_proofs_never_reopen_branch = ref false
+  type stm_opt = {
+    async_proofs_n_workers : int;
+    async_proofs_n_tacworkers : int;
 
-  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
+    async_proofs_cache : cache option;
+    async_proofs_mode : async_proofs;
+
+    async_proofs_private_flags : string option;
+    async_proofs_full : bool;
+    async_proofs_never_reopen_branch : bool;
+
+    async_proofs_tac_error_resilience : tac_error_filter;
+    async_proofs_cmd_error_resilience : bool;
+    async_proofs_delegation_threshold : float;
+  }
 
-  let async_proofs_delegation_threshold = ref 0.03
+  let default_opts = {
+    async_proofs_n_workers = 1;
+    async_proofs_n_tacworkers = 2;
 
+    async_proofs_cache = None;
+
+    async_proofs_mode = APoff;
+
+    async_proofs_private_flags = None;
+    async_proofs_full = false;
+    async_proofs_never_reopen_branch = false;
+
+    async_proofs_tac_error_resilience = `Only [ "curly" ];
+    async_proofs_cmd_error_resilience = true;
+    async_proofs_delegation_threshold = 0.03;
+  }
+
+  let cur_opt = ref default_opts
 end
 
 open AsyncOpts
 
-let async_proofs_is_master () =
-  !async_proofs_mode = APon &&
+let async_proofs_is_master opt =
+  opt.async_proofs_mode = APon &&
   !Flags.async_proofs_worker_id = "master"
 
 (* Protect against state changes *)
@@ -558,7 +577,7 @@ end = struct (* {{{ *)
     | None -> raise Vcs_aux.Expired
   let set_state id s =
     (get_info id).state <- s;
-    if async_proofs_is_master () then Hooks.(call state_ready id)
+    if async_proofs_is_master !cur_opt then Hooks.(call state_ready id)
   let get_state id = (get_info id).state
   let reached id =
     let info = get_info id in
@@ -1150,7 +1169,7 @@ end = struct (* {{{ *)
              " the \"-async-proofs-cache force\" option to Coq."))
 
   let undo_vernac_classifier v =
-    if VCS.is_interactive () = `No && !async_proofs_cache <> Some Force
+    if VCS.is_interactive () = `No && !cur_opt.async_proofs_cache <> Some Force
     then undo_costly_in_batch_mode v;
     try
       match Vernacprop.under_control v with
@@ -1286,7 +1305,7 @@ let prev_node { id } =
 let cur_node id = mk_doc_node id (VCS.visit id)
 
 let is_block_name_enabled name =
-  match !async_proofs_tac_error_resilience with
+  match !cur_opt.async_proofs_tac_error_resilience with
   | `None -> false
   | `All -> true
   | `Only l -> List.mem name l
@@ -1294,7 +1313,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 &&
-     (async_proofs_is_master () || Flags.async_proofs_is_worker ())
+     (async_proofs_is_master !cur_opt || Flags.async_proofs_is_worker ())
   then (
   match cur_node id with
   | None -> ()
@@ -1396,7 +1415,7 @@ end = struct (* {{{ *)
   let task_match age t =
     match age, t with
     | Fresh, BuildProof { t_states } ->
-        not !async_proofs_full ||
+        not !cur_opt.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
@@ -1433,7 +1452,7 @@ end = struct (* {{{ *)
         feedback (InProgress ~-1);
         t_assign (`Val pl);
         record_pb_time ?loc:t_loc t_name time;
-        if !async_proofs_full || t_drop
+        if !cur_opt.async_proofs_full || t_drop
         then `Stay(t_states,[States t_states])
         else `End
     | Fresh, BuildProof { t_assign; t_loc; t_name; t_states },
@@ -1607,8 +1626,8 @@ end = struct (* {{{ *)
 
   let queue = ref None
   let init () =
-    if async_proofs_is_master () then
-      queue := Some (TaskQueue.create !async_proofs_n_workers)
+    if async_proofs_is_master !cur_opt then
+      queue := Some (TaskQueue.create !cur_opt.async_proofs_n_workers)
     else
       queue := Some (TaskQueue.create 0)
 
@@ -2074,7 +2093,7 @@ end = struct (* {{{ *)
       QueryTask.({ t_where = prev; t_for = id; t_what = q }) ~cancel_switch
 
   let init () = queue := Some (TaskQueue.create
-    (if !async_proofs_full then 1 else 0))
+    (if !cur_opt.async_proofs_full then 1 else 0))
 
 end (* }}} *)
 
@@ -2090,14 +2109,14 @@ let async_policy () =
   let open Flags in
   if is_universe_polymorphism () then false
   else if VCS.is_interactive () = `Yes then
-    (async_proofs_is_master () || !async_proofs_mode = APonLazy)
+    (async_proofs_is_master !cur_opt || !cur_opt.async_proofs_mode = APonLazy)
   else
-    (VCS.is_vio_doc () || !async_proofs_mode <> APoff)
+    (VCS.is_vio_doc () || !cur_opt.async_proofs_mode <> APoff)
 
 let delegate name =
-     get_hint_bp_time name >= !async_proofs_delegation_threshold
+     get_hint_bp_time name >= !cur_opt.async_proofs_delegation_threshold
   || VCS.is_vio_doc ()
-  || !async_proofs_full
+  || !cur_opt.async_proofs_full
 
 let warn_deprecated_nested_proofs =
   CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated"
@@ -2212,7 +2231,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) || !async_proofs_full)
+          (not(State.is_cached_and_valid id) || !cur_opt.async_proofs_full)
        then check_policy rc
        else make_sync `AlreadyEvaluated rc
 
@@ -2294,9 +2313,9 @@ let known_state ?(redefine_qed=false) ~cache id =
 
   (* Absorb tactic errors from f () *)
   let resilient_tactic id blockname f =
-    if !async_proofs_tac_error_resilience = `None ||
-       (async_proofs_is_master () &&
-        !async_proofs_mode = APoff)
+    if !cur_opt.async_proofs_tac_error_resilience = `None ||
+       (async_proofs_is_master !cur_opt &&
+        !cur_opt.async_proofs_mode = APoff)
     then f ()
     else
       try f ()
@@ -2305,9 +2324,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 !async_proofs_cmd_error_resilience ||
-       (async_proofs_is_master () &&
-        !async_proofs_mode = APoff)
+    if not !cur_opt.async_proofs_cmd_error_resilience ||
+       (async_proofs_is_master !cur_opt &&
+        !cur_opt.async_proofs_mode = APoff)
     then f x
     else
       try f x
@@ -2353,10 +2372,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
-                !async_proofs_n_tacworkers view.next id x)
+                !cur_opt.async_proofs_n_tacworkers view.next id x)
           ), cache, true
       | `Cmd { cast = x; cqueue = `QueryQueue cancel_switch }
-        when async_proofs_is_master () -> (fun () ->
+        when async_proofs_is_master !cur_opt -> (fun () ->
             reach view.next;
             Query.vernac_interp ~cancel_switch view.next id x
           ), cache, false
@@ -2370,7 +2389,7 @@ 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 !async_proofs_mode with
+          (match !cur_opt.async_proofs_mode with
            | APon | APonLazy ->
              resilient_command reach view.next
            | APoff -> reach view.next);
@@ -2500,7 +2519,7 @@ let known_state ?(redefine_qed=false) ~cache id =
           ), cache, true
     in
     let cache_step =
-      if !async_proofs_cache = Some Force then `Yes
+      if !cur_opt.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;
@@ -2516,6 +2535,7 @@ end (* }}} *)
 type stm_init_options = {
   doc_type     : stm_doc_type;
   require_libs : (string * string option * bool option) list;
+  stm_options  : AsyncOpts.stm_opt;
 (*
   fb_handler   : Feedback.feedback -> unit;
   iload_path   : (string list * string * bool) list;
@@ -2531,10 +2551,11 @@ let doc_type_module_name (std : stm_doc_type) =
 *)
 
 let init_core () =
-  if !async_proofs_mode = APon then Control.enable_thread_delay := true;
+  if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true;
   State.register_root_state ()
 
-let new_doc { doc_type ; require_libs } =
+let new_doc { doc_type ; stm_options; require_libs } =
+
   let load_objs libs =
     let rq_file (dir, from, exp) =
       let mp = Libnames.(Qualid (Loc.tag @@ qualid_of_string dir)) in
@@ -2543,6 +2564,9 @@ let new_doc { doc_type ; require_libs } =
     List.(iter rq_file (rev libs))
   in
 
+  (* Set the options from the new documents *)
+  AsyncOpts.cur_opt := stm_options;
+
   (* We must reset the whole state before creating a document! *)
   State.restore_root_state ();
 
@@ -2570,10 +2594,10 @@ let new_doc { doc_type ; require_libs } =
   State.define ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial;
   Backtrack.record ();
   Slaves.init ();
-  if async_proofs_is_master () then begin
+  if async_proofs_is_master !cur_opt then begin
     stm_prerr_endline (fun () -> "Initializing workers");
     Query.init ();
-    let opts = match !async_proofs_private_flags with
+    let opts = match !cur_opt.async_proofs_private_flags with
       | None -> []
       | Some s -> Str.split_delim (Str.regexp ",") s in
     begin try
@@ -2772,7 +2796,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 !async_proofs_full then `QueryQueue (ref false)
+            if !cur_opt.async_proofs_full then `QueryQueue (ref false)
             else if VCS.is_vio_doc () &&
                     VCS.((get_branch head).kind = `Master) &&
                     may_pierce_opaque (Vernacprop.under_control x.expr)
@@ -3104,7 +3128,7 @@ let edit_at ~doc id =
     VCS.delete_boxes_of id;
     VCS.gc ();
     VCS.print ();
-    if not !async_proofs_full then
+    if not !cur_opt.async_proofs_full then
       Reach.known_state ~cache:(VCS.is_interactive ()) id;
     VCS.checkout_shallowest_proof_branch ();
     `NewTip in
@@ -3120,7 +3144,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 !async_proofs_never_reopen_branch
+          if has_failed qed_id && is_pure qed_id && not !cur_opt.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 587b75642..8b5581979 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -10,6 +10,33 @@ open Names
 
 (** state-transaction-machine interface *)
 
+(* Flags *)
+module AsyncOpts : sig
+
+  type cache = Force
+  type async_proofs = APoff | APonLazy | APon
+  type tac_error_filter = [ `None | `Only of string list | `All ]
+
+  type stm_opt = {
+    async_proofs_n_workers : int;
+    async_proofs_n_tacworkers : int;
+
+    async_proofs_cache : cache option;
+    async_proofs_mode : async_proofs;
+
+    async_proofs_private_flags : string option;
+    async_proofs_full : bool;
+    async_proofs_never_reopen_branch : bool;
+
+    async_proofs_tac_error_resilience : tac_error_filter;
+    async_proofs_cmd_error_resilience : bool;
+    async_proofs_delegation_threshold : float;
+  }
+
+  val default_opts : stm_opt
+
+end
+
 (** The STM doc type determines some properties such as what
     uncompleted proofs are allowed and recording of aux files. *)
 type stm_doc_type =
@@ -21,6 +48,7 @@ type stm_doc_type =
 type stm_init_options = {
   doc_type     : stm_doc_type;
   require_libs : (string * string option * bool option) list;
+  stm_options  : AsyncOpts.stm_opt;
 (*
   fb_handler   : Feedback.feedback -> unit;
   iload_path   : (string list * string * bool) list;
@@ -228,27 +256,3 @@ 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/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9719f60bb..572092e74 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -291,6 +291,8 @@ let ensure_exists f =
   if not (Sys.file_exists f) then
     compile_error (hov 0 (str "Can't find file" ++ spc () ++ str f))
 
+let top_stm_options = ref Stm.AsyncOpts.default_opts
+
 (* Compile a vernac file *)
 let compile ~time ~verbosely ~f_in ~f_out =
   let check_pending_proofs () =
@@ -314,7 +316,8 @@ let compile ~time ~verbosely ~f_in ~f_out =
 
       let doc, sid = Stm.(new_doc
           { doc_type = VoDoc long_f_dot_vo;
-            require_libs = require_libs ()
+            require_libs = require_libs ();
+            stm_options = !top_stm_options;
           }) in
 
       let doc, sid = load_init_vernaculars ~time doc sid in
@@ -349,7 +352,8 @@ let compile ~time ~verbosely ~f_in ~f_out =
 
       let doc, sid = Stm.(new_doc
           { doc_type = VioDoc long_f_dot_vio;
-            require_libs = require_libs ()
+            require_libs = require_libs ();
+            stm_options = !top_stm_options;
           }) in
 
       let doc, sid = load_init_vernaculars ~time doc sid in
@@ -650,23 +654,47 @@ let parse_args arglist =
     (* Options with one arg *)
     |"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ())
     |"-async-proofs" ->
-        Stm.AsyncOpts.async_proofs_mode := get_async_proofs_mode opt (next())
+      top_stm_options :=
+        { !top_stm_options with
+          Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next())
+        }
     |"-async-proofs-j" ->
-        Stm.AsyncOpts.async_proofs_n_workers := (get_int opt (next ()))
+      top_stm_options :=
+        { !top_stm_options with
+          Stm.AsyncOpts.async_proofs_n_workers = (get_int opt (next ()))
+        }
     |"-async-proofs-cache" ->
-        Stm.AsyncOpts.async_proofs_cache := get_cache opt (next ())
+      top_stm_options :=
+        { !top_stm_options with
+          Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ())
+        }
     |"-async-proofs-tac-j" ->
-        Stm.AsyncOpts.async_proofs_n_tacworkers := (get_int opt (next ()))
+      top_stm_options :=
+        { !top_stm_options with
+          Stm.AsyncOpts.async_proofs_n_tacworkers = (get_int opt (next ()))
+        }
     |"-async-proofs-worker-priority" ->
         WorkerLoop.async_proofs_worker_priority := get_priority opt (next ())
     |"-async-proofs-private-flags" ->
-        Stm.AsyncOpts.async_proofs_private_flags := Some (next ());
+      top_stm_options :=
+        { !top_stm_options with
+          Stm.AsyncOpts.async_proofs_private_flags = Some (next ());
+        }
     |"-async-proofs-tactic-error-resilience" ->
-        Stm.AsyncOpts.async_proofs_tac_error_resilience := get_error_resilience opt (next ())
+      top_stm_options :=
+        { !top_stm_options with
+          Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ());
+        }
     |"-async-proofs-command-error-resilience" ->
-        Stm.AsyncOpts.async_proofs_cmd_error_resilience := get_bool opt (next ())
+      top_stm_options :=
+        { !top_stm_options with
+          Stm.AsyncOpts.async_proofs_cmd_error_resilience = get_bool opt (next ())
+        }
     |"-async-proofs-delegation-threshold" ->
-        Stm.AsyncOpts.async_proofs_delegation_threshold:= get_float opt (next ())
+      top_stm_options :=
+        { !top_stm_options with
+          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
@@ -706,9 +734,15 @@ let parse_args arglist =
     |"-async-queries-always-delegate"
     |"-async-proofs-always-delegate"
     |"-async-proofs-full" ->
-        Stm.AsyncOpts.async_proofs_full := true;
+      top_stm_options :=
+        { !top_stm_options with
+          Stm.AsyncOpts.async_proofs_full = true;
+        }
     |"-async-proofs-never-reopen-branch" ->
-        Stm.AsyncOpts.async_proofs_never_reopen_branch := true;
+      top_stm_options :=
+        { !top_stm_options with
+          Stm.AsyncOpts.async_proofs_never_reopen_branch = true;
+        }
     |"-batch" -> set_batch_mode ()
     |"-test-mode" -> Flags.test_mode := true
     |"-beautify" -> Flags.beautify := true
@@ -812,7 +846,8 @@ let init_toplevel arglist =
         try
           let doc, sid = Stm.(new_doc
                                 { doc_type = Interactive !toplevel_name;
-                                  require_libs = require_libs ()
+                                  require_libs = require_libs ();
+                                  stm_options = !top_stm_options;
                                 }) in
           Some (load_init_vernaculars ~time:!measure_time doc sid)
         with any -> flush_all(); fatal_error any