[sysinit] new component for system initialization

This component holds the code for initializing Coq:
- parsing arguments not specific to the toplevel
- initializing all components from vernac downwards (no stm)

This commit moves stm specific arguments parsing to stm/stmargs.ml

6 files changed, 172 insertions, 84 deletions

diff --git a/stm/dune b/stm/dune
index c369bd00fb..27d561334e 100644
--- a/stm/dune
+++ b/stm/dune
@@ -3,4 +3,4 @@
  (synopsis "Coq's Document Manager and Proof Checking Scheduler")
  (public_name coq.stm)
  (wrapped false)
- (libraries vernac))
+ (libraries sysinit))
diff --git a/stm/stm.ml b/stm/stm.ml
index 27f2b6fc5c..f4e370e7bc 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -297,13 +297,11 @@ end (* }}} *)
 (*************************** THE DOCUMENT *************************************)
 (******************************************************************************)
 
-type interactive_top = TopLogical of DirPath.t | TopPhysical of string
-
 (* The main document type associated to a VCS *)
 type stm_doc_type =
   | VoDoc       of string
   | VioDoc      of string
-  | Interactive of interactive_top
+  | Interactive of Coqargs.interactive_top
 
 (* Dummy until we land the functional interp patch + fixed start_library *)
 type doc = int
@@ -517,7 +515,7 @@ end = struct (* {{{ *)
   type vcs = (branch_type, transaction, vcs state_info, box) t
   let vcs : vcs ref = ref (empty Stateid.dummy)
 
-  let doc_type = ref (Interactive (TopLogical (Names.DirPath.make [])))
+  let doc_type = ref (Interactive (Coqargs.TopLogical (Names.DirPath.make [])))
   let ldir = ref Names.DirPath.empty
 
   let init dt id ps =
@@ -2308,23 +2306,6 @@ end (* }}} *)
 
 (** STM initialization options: *)
 
-type option_command =
-  | OptionSet of string option
-  | OptionAppend of string
-  | OptionUnset
-
-type injection_command =
-  | OptionInjection of (Goptions.option_name * option_command)
-  (** Set flags or options before the initial state is ready. *)
-  | RequireInjection of (string * string option * bool option)
-  (** Require libraries before the initial state is
-     ready. Parameters follow [Library], that is to say,
-     [lib,prefix,import_export] means require library [lib] from
-     optional [prefix] and [import_export] if [Some false/Some true]
-     is used.  *)
-  (* -load-vernac-source interleaving is not supported yet *)
-  (* | LoadInjection of (string * bool) *)
-
 type stm_init_options =
   { doc_type : stm_doc_type
   (** The STM does set some internal flags differently depending on
@@ -2338,7 +2319,7 @@ type stm_init_options =
   (** [vo] load paths for the document. Usually extracted from -R
      options / _CoqProject *)
 
-  ; injections : injection_command list
+  ; injections : Coqargs.injection_command list
   (** Injects Require and Set/Unset commands before the initial
      state is ready *)
 
@@ -2355,6 +2336,10 @@ let doc_type_module_name (std : stm_doc_type) =
   | Interactive mn -> Names.DirPath.to_string mn
 *)
 
+let init_process stm_flags =
+  Spawned.init_channels ();
+  CoqworkmgrApi.(init stm_flags.AsyncOpts.async_proofs_worker_priority)
+
 let init_core () =
   if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true;
   if !Flags.async_proofs_worker_id = "master" then Partac.enable_par ~nworkers:!cur_opt.async_proofs_n_tacworkers;
@@ -2379,44 +2364,10 @@ let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } =
     let mfrom = Option.map Libnames.qualid_of_string from in
     Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
 
-  let interp_set_option opt v old =
-    let open Goptions in
-    let err expect =
-      let opt = String.concat " " opt in
-      let got = v in (* avoid colliding with Pp.v *)
-      CErrors.user_err
-        Pp.(str "-set: " ++ str opt ++
-            str" expects " ++ str expect ++
-            str" but got " ++ str got)
-    in
-    match old with
-    | BoolValue _ ->
-      let v = match String.trim v with
-        | "true" -> true
-        | "false" | "" -> false
-        | _ -> err "a boolean"
-      in
-      BoolValue v
-    | IntValue _ ->
-      let v = String.trim v in
-      let v = match int_of_string_opt v with
-        | Some _ as v -> v
-        | None -> if v = "" then None else err "an int"
-      in
-      IntValue v
-    | StringValue _ -> StringValue v
-    | StringOptValue _ -> StringOptValue (Some v) in
-
-  let set_option = let open Goptions in function
-      | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt
-      | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true
-      | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v
-      | opt, OptionAppend v -> set_string_option_append_value_gen ~locality:OptLocal opt v in
-
   let handle_injection = function
-    | RequireInjection r -> require_file r
+    | Coqargs.RequireInjection r -> require_file r
     (* | LoadInjection l -> *)
-    | OptionInjection o -> set_option o in
+    | Coqargs.OptionInjection o -> Coqargs.set_option o in
 
   (* Set the options from the new documents *)
   AsyncOpts.cur_opt := stm_options;
@@ -2437,8 +2388,8 @@ let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } =
   begin match doc_type with
     | Interactive ln ->
       let dp = match ln with
-        | TopLogical dp -> dp
-        | TopPhysical f -> dirpath_of_file f
+        | Coqargs.TopLogical dp -> dp
+        | Coqargs.TopPhysical f -> dirpath_of_file f
       in
       Declaremods.start_library dp
 
diff --git a/stm/stm.mli b/stm/stm.mli
index e0c33a309b..dddd63cb52 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -42,32 +42,13 @@ module AsyncOpts : sig
 
 end
 
-type interactive_top = TopLogical of DirPath.t | TopPhysical of string
-
 (** The STM document type [stm_doc_type] determines some properties
    such as what uncompleted proofs are allowed and what gets recorded
    to aux files. *)
 type stm_doc_type =
   | VoDoc       of string       (* file path *)
   | VioDoc      of string       (* file path *)
-  | Interactive of interactive_top    (* module path *)
-
-type option_command =
-  | OptionSet of string option
-  | OptionAppend of string
-  | OptionUnset
-
-type injection_command =
-  | OptionInjection of (Goptions.option_name * option_command)
-  (** Set flags or options before the initial state is ready. *)
-  | RequireInjection of (string * string option * bool option)
-  (** Require libraries before the initial state is
-     ready. Parameters follow [Library], that is to say,
-     [lib,prefix,import_export] means require library [lib] from
-     optional [prefix] and [import_export] if [Some false/Some true]
-     is used.  *)
-  (* -load-vernac-source interleaving is not supported yet *)
-  (* | LoadInjection of (string * bool) *)
+  | Interactive of Coqargs.interactive_top    (* module path *)
 
 (** STM initialization options: *)
 type stm_init_options =
@@ -83,7 +64,7 @@ type stm_init_options =
   (** [vo] load paths for the document. Usually extracted from -R
      options / _CoqProject *)
 
-  ; injections : injection_command list
+  ; injections : Coqargs.injection_command list
   (** Injects Require and Set/Unset commands before the initial
      state is ready *)
 
@@ -94,8 +75,10 @@ type stm_init_options =
 (** The type of a STM document *)
 type doc
 
-(** [init_core] performs some low-level initialization; should go away
-   in future releases. *)
+(** [init_process] performs some low-level initialization, call early *)
+val init_process : AsyncOpts.stm_opt -> unit
+
+(** [init_core] snapshorts the initial system state *)
 val init_core : unit -> unit
 
 (** [new_doc opt] Creates a new document with options [opt] *)
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 49e7195e27..a77e0c79e7 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -7,5 +7,6 @@ CoqworkmgrApi
 AsyncTaskQueue
 Partac
 Stm
+Stmargs
 ProofBlockDelimiter
 Vio_checking
diff --git a/stm/stmargs.ml b/stm/stmargs.ml
new file mode 100644
index 0000000000..609d4f42e9
--- /dev/null
+++ b/stm/stmargs.ml
@@ -0,0 +1,140 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+let fatal_error exn =
+  Topfmt.(in_phase ~phase:ParsingCommandLine print_err_exn exn);
+  let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
+  exit exit_code
+
+let set_worker_id opt s =
+  assert (s <> "master");
+  Flags.async_proofs_worker_id := s
+
+let get_host_port opt s =
+  match String.split_on_char ':' s with
+  | [host; portr; portw] ->
+    Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
+  | ["stdfds"] -> Some Spawned.AnonPipe
+  | _ ->
+    Coqargs.error_wrong_arg ("Error: host:portr:portw or stdfds expected after option "^opt)
+
+let get_error_resilience opt = function
+  | "on" | "all" | "yes" -> `All
+  | "off" | "no" -> `None
+  | s -> `Only (String.split_on_char ',' s)
+
+let get_priority opt s =
+  try CoqworkmgrApi.priority_of_string s
+  with Invalid_argument _ ->
+    Coqargs.error_wrong_arg ("Error: low/high expected after "^opt)
+
+let get_async_proofs_mode opt = let open Stm.AsyncOpts in function
+  | "no" | "off" -> APoff
+  | "yes" | "on" -> APon
+  | "lazy" -> APonLazy
+  | _ ->
+    Coqargs.error_wrong_arg ("Error: on/off/lazy expected after "^opt)
+
+let get_cache opt = function
+  | "force" -> Some Stm.AsyncOpts.Force
+  | _ ->
+    Coqargs.error_wrong_arg ("Error: force expected after "^opt)
+
+let parse_args ~init arglist : Stm.AsyncOpts.stm_opt * string list =
+  let args = ref arglist in
+  let extras = ref [] in
+  let rec parse oval = match !args with
+  | [] ->
+    (oval, List.rev !extras)
+  | opt :: rem ->
+    args := rem;
+    let next () = match !args with
+      | x::rem -> args := rem; x
+      | [] -> Coqargs.error_missing_arg opt
+    in
+    let noval = begin match opt with
+
+    |"-async-proofs" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next())
+      }
+    |"-async-proofs-j" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_n_workers = (Coqargs.get_int ~opt (next ()))
+      }
+    |"-async-proofs-cache" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ())
+      }
+
+    |"-async-proofs-tac-j" ->
+      let j = Coqargs.get_int ~opt (next ()) in
+      if j <= 0 then begin
+        Coqargs.error_wrong_arg ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1")
+      end;
+      { oval with
+        Stm.AsyncOpts.async_proofs_n_tacworkers = j
+      }
+
+    |"-async-proofs-worker-priority" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_worker_priority = get_priority opt (next ())
+      }
+
+    |"-async-proofs-private-flags" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_private_flags = Some (next ());
+      }
+
+    |"-async-proofs-tactic-error-resilience" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ())
+      }
+
+    |"-async-proofs-command-error-resilience" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_cmd_error_resilience = Coqargs.get_bool ~opt (next ())
+      }
+
+    |"-async-proofs-delegation-threshold" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_delegation_threshold = Coqargs.get_float ~opt (next ())
+      }
+
+    |"-worker-id" -> set_worker_id opt (next ()); oval
+
+    |"-main-channel" ->
+      Spawned.main_channel := get_host_port opt (next()); oval
+
+    |"-control-channel" ->
+      Spawned.control_channel := get_host_port opt (next()); oval
+
+    (* Options with zero arg *)
+    |"-async-queries-always-delegate"
+    |"-async-proofs-always-delegate"
+    |"-async-proofs-never-reopen-branch" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_never_reopen_branch = true
+      }
+    |"-stm-debug" -> Stm.stm_debug := true; oval
+    (* Unknown option *)
+    | s ->
+      extras := s :: !extras;
+      oval
+    end in
+    parse noval
+  in
+  try
+    parse init
+  with any -> fatal_error any
+
+let usage = "\
+\n  -stm-debug             STM debug mode (will trace every transaction)\
+"
\ No newline at end of file
diff --git a/stm/stmargs.mli b/stm/stmargs.mli
new file mode 100644
index 0000000000..f760afdc98
--- /dev/null
+++ b/stm/stmargs.mli
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val parse_args : init:Stm.AsyncOpts.stm_opt -> string list -> Stm.AsyncOpts.stm_opt * string list
+
+val usage : string