[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

14 files changed, 79 insertions, 961 deletions

diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index b75a4199ea..4747abceb5 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -24,7 +24,7 @@ let fatal_error msg =
 let load_init_file opts ~state =
   if opts.pre.load_rcfile then
     Topfmt.(in_phase ~phase:LoadingRcFile) (fun () ->
-        Coqinit.load_rcfile ~rcfile:opts.config.rcfile ~state) ()
+        Coqrc.load_rcfile ~rcfile:opts.config.rcfile ~state) ()
   else begin
     Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.");
     state
@@ -93,7 +93,7 @@ let create_empty_file filename =
   close_out f
 
 (* Compile a vernac file *)
-let compile opts copts ~echo ~f_in ~f_out =
+let compile opts stm_options copts ~echo ~f_in ~f_out =
   let open Vernac.State in
   let check_pending_proofs () =
     let pfs = Vernacstate.Declare.get_all_proof_names () [@ocaml.warning "-3"] in
@@ -106,7 +106,6 @@ let compile opts copts ~echo ~f_in ~f_out =
   in
   let ml_load_path, vo_load_path = build_load_path opts in
   let injections = injection_commands opts in
-  let stm_options = opts.config.stm_flags in
   let output_native_objects = match opts.config.native_compiler with
     | NativeOff -> false | NativeOn {ondemand} -> not ondemand
   in
@@ -209,22 +208,22 @@ let compile opts copts ~echo ~f_in ~f_out =
       dump_empty_vos();
       create_empty_file (long_f_dot_out ^ "k")
 
-let compile opts copts ~echo ~f_in ~f_out =
+let compile opts stm_opts copts ~echo ~f_in ~f_out =
   ignore(CoqworkmgrApi.get 1);
-  compile opts copts ~echo ~f_in ~f_out;
+  compile opts stm_opts copts ~echo ~f_in ~f_out;
   CoqworkmgrApi.giveback 1
 
-let compile_file opts copts (f_in, echo) =
+let compile_file opts stm_opts copts (f_in, echo) =
   let f_out = copts.compilation_output_name in
   if !Flags.beautify then
     Flags.with_option Flags.beautify_file
-      (fun f_in -> compile opts copts ~echo ~f_in ~f_out) f_in
+      (fun f_in -> compile opts stm_opts copts ~echo ~f_in ~f_out) f_in
   else
-    compile opts copts ~echo ~f_in ~f_out
+    compile opts stm_opts copts ~echo ~f_in ~f_out
 
-let compile_files opts copts =
+let compile_files (opts, stm_opts) copts =
   let compile_list = copts.compile_list in
-  List.iter (compile_file opts copts) compile_list
+  List.iter (compile_file opts stm_opts copts) compile_list
 
 (******************************************************************************)
 (* VIO Dispatching                                                            *)
diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli
index 8c154488d0..1b670a8edc 100644
--- a/toplevel/ccompile.mli
+++ b/toplevel/ccompile.mli
@@ -13,7 +13,7 @@
 val load_init_vernaculars : Coqargs.t -> state:Vernac.State.t-> Vernac.State.t
 
 (** [compile_files opts] compile files specified in [opts] *)
-val compile_files : Coqargs.t -> Coqcargs.t -> unit
+val compile_files : Coqargs.t * Stm.AsyncOpts.stm_opt -> Coqcargs.t -> unit
 
 (** [do_vio opts] process [.vio] files in [opts] *)
 val do_vio : Coqargs.t -> Coqcargs.t -> unit
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
deleted file mode 100644
index c114c43e26..0000000000
--- a/toplevel/coqargs.ml
+++ /dev/null
@@ -1,580 +0,0 @@
-(************************************************************************)
-(*         *   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 error_wrong_arg msg =
-  prerr_endline msg; exit 1
-
-let error_missing_arg s =
-  prerr_endline ("Error: extra argument expected after option "^s);
-  prerr_endline "See -help for the syntax of supported options";
-  exit 1
-
-(******************************************************************************)
-(* Imperative effects! This must be fixed at some point.                      *)
-(******************************************************************************)
-let set_worker_id opt s =
-  assert (s <> "master");
-  Flags.async_proofs_worker_id := s
-
-let set_type_in_type () =
-  let typing_flags = Environ.typing_flags (Global.env ()) in
-  Global.set_typing_flags { typing_flags with Declarations.check_universes = false }
-
-(******************************************************************************)
-
-type color = [`ON | `AUTO | `EMACS | `OFF]
-
-type native_compiler = Coq_config.native_compiler =
-  NativeOff | NativeOn of { ondemand : bool }
-
-type coqargs_logic_config = {
-  impredicative_set : Declarations.set_predicativity;
-  indices_matter    : bool;
-  toplevel_name     : Stm.interactive_top;
-}
-
-type coqargs_config = {
-  logic       : coqargs_logic_config;
-  rcfile      : string option;
-  coqlib      : string option;
-  color       : color;
-  enable_VM   : bool;
-  native_compiler : native_compiler;
-  native_output_dir : CUnix.physical_path;
-  native_include_dirs : CUnix.physical_path list;
-  stm_flags   : Stm.AsyncOpts.stm_opt;
-  debug       : bool;
-  time        : bool;
-  print_emacs : bool;
-}
-
-type coqargs_pre = {
-  boot        : bool;
-  load_init   : bool;
-  load_rcfile : bool;
-
-  ml_includes : string list;
-  vo_includes : Loadpath.vo_path list;
-
-  load_vernacular_list : (string * bool) list;
-  injections  : Stm.injection_command list;
-
-  inputstate  : string option;
-}
-
-type coqargs_query =
-  | PrintTags | PrintWhere | PrintConfig
-  | PrintVersion | PrintMachineReadableVersion
-  | PrintHelp of Usage.specific_usage
-
-type coqargs_main =
-  | Queries of coqargs_query list
-  | Run
-
-type coqargs_post = {
-  memory_stat : bool;
-  output_context : bool;
-}
-
-type t = {
-  config : coqargs_config;
-  pre : coqargs_pre;
-  main : coqargs_main;
-  post : coqargs_post;
-}
-
-let default_toplevel = Names.(DirPath.make [Id.of_string "Top"])
-
-let default_native = Coq_config.native_compiler
-
-let default_logic_config = {
-  impredicative_set = Declarations.PredicativeSet;
-  indices_matter = false;
-  toplevel_name = Stm.TopLogical default_toplevel;
-}
-
-let default_config = {
-  logic        = default_logic_config;
-  rcfile       = None;
-  coqlib       = None;
-  color        = `AUTO;
-  enable_VM    = true;
-  native_compiler = default_native;
-  native_output_dir = ".coq-native";
-  native_include_dirs = [];
-  stm_flags    = Stm.AsyncOpts.default_opts;
-  debug        = false;
-  time         = false;
-  print_emacs  = false;
-
-  (* Quiet / verbosity options should be here *)
-}
-
-let default_pre = {
-  boot         = false;
-  load_init    = true;
-  load_rcfile  = true;
-  ml_includes  = [];
-  vo_includes  = [];
-  load_vernacular_list = [];
-  injections   = [];
-  inputstate   = None;
-}
-
-let default_queries = []
-
-let default_post = {
-  memory_stat  = false;
-  output_context = false;
-}
-
-let default = {
-  config = default_config;
-  pre    = default_pre;
-  main   = Run;
-  post   = default_post;
-}
-
-(******************************************************************************)
-(* Functional arguments                                                       *)
-(******************************************************************************)
-let add_ml_include opts s =
-  { opts with pre = { opts.pre with ml_includes = s :: opts.pre.ml_includes }}
-
-let add_vo_include opts unix_path coq_path implicit =
-  let open Loadpath in
-  let coq_path = Libnames.dirpath_of_string coq_path in
-  { opts with pre = { opts.pre with vo_includes = {
-        unix_path; coq_path; has_ml = false; implicit; recursive = true } :: opts.pre.vo_includes }}
-
-let add_vo_require opts d p export =
-  { opts with pre = { opts.pre with injections = Stm.RequireInjection (d, p, export) :: opts.pre.injections }}
-
-let add_load_vernacular opts verb s =
-    { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }}
-
-let add_set_option opts opt_name value =
-  { opts with pre = { opts.pre with injections = Stm.OptionInjection (opt_name, value) :: opts.pre.injections }}
-
-(** Options for proof general *)
-let set_emacs opts =
-  Goptions.set_bool_option_value Printer.print_goal_tag_opt_name true;
-  { opts with config = { opts.config with color = `EMACS; print_emacs = true }}
-
-let set_logic f oval =
-  { oval with config = { oval.config with logic = f oval.config.logic }}
-
-let set_color opts = function
-  | "yes" | "on" -> { opts with config = { opts.config with color = `ON }}
-  | "no" | "off" -> { opts with config = { opts.config with color = `OFF }}
-  | "auto" -> { opts with config = { opts.config with color = `AUTO }}
-  | _ ->
-    error_wrong_arg ("Error: on/off/auto expected after option color")
-
-let set_query opts q =
-  { opts with main = match opts.main with
-  | Run -> Queries (default_queries@[q])
-  | Queries queries -> Queries (queries@[q])
-  }
-
-let warn_deprecated_sprop_cumul =
-  CWarnings.create ~name:"deprecated-spropcumul" ~category:"deprecated"
-         (fun () -> Pp.strbrk "Use the \"Cumulative StrictProp\" flag instead.")
-
-let warn_deprecated_inputstate =
-  CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
-         (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.")
-
-let set_inputstate opts s =
-  warn_deprecated_inputstate ();
-  { opts with pre = { opts.pre with inputstate = Some s }}
-
-(******************************************************************************)
-(* Parsing helpers                                                            *)
-(******************************************************************************)
-let get_bool opt = function
-  | "yes" | "on" -> true
-  | "no" | "off" -> false
-  | _ ->
-    error_wrong_arg ("Error: yes/no expected after option "^opt)
-
-let get_int opt n =
-  try int_of_string n
-  with Failure _ ->
-    error_wrong_arg ("Error: integer expected after option "^opt)
-
-let get_float opt n =
-  try float_of_string n
-  with Failure _ ->
-    error_wrong_arg ("Error: float expected after option "^opt)
-
-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
-  | _ ->
-    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 _ ->
-    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
-  | _ ->
-    error_wrong_arg ("Error: on/off/lazy expected after "^opt)
-
-let get_cache opt = function
-  | "force" -> Some Stm.AsyncOpts.Force
-  | _ ->
-    error_wrong_arg ("Error: force expected after "^opt)
-
-
-let get_native_name s =
-  (* We ignore even critical errors because this mode has to be super silent *)
-  try
-    Filename.(List.fold_left concat (dirname s)
-                [ !Nativelib.output_dir
-                ; Library.native_name_from_filename s
-                ])
-  with _ -> ""
-
-let get_compat_file = function
-  | "8.14" -> "Coq.Compat.Coq814"
-  | "8.13" -> "Coq.Compat.Coq813"
-  | "8.12" -> "Coq.Compat.Coq812"
-  | "8.11" -> "Coq.Compat.Coq811"
-  | ("8.10" | "8.9" | "8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
-    CErrors.user_err ~hdr:"get_compat_file"
-      Pp.(str "Compatibility with version " ++ str s ++ str " not supported.")
-  | s ->
-    CErrors.user_err ~hdr:"get_compat_file"
-      Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".")
-
-let to_opt_key = Str.(split (regexp " +"))
-
-let parse_option_set opt =
-  match String.index_opt opt '=' with
-  | None -> to_opt_key opt, None
-  | Some eqi ->
-    let len = String.length opt in
-    let v = String.sub opt (eqi+1) (len - eqi - 1) in
-    to_opt_key (String.sub opt 0 eqi), Some v
-
-let warn_no_native_compiler =
-  CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler"
-    Pp.(fun s -> strbrk "Native compiler is disabled," ++
-                   strbrk " -native-compiler " ++ strbrk s ++
-                   strbrk " option ignored.")
-
-let get_native_compiler s =
-  (* We use two boolean flags because the four states make sense, even if
-  only three are accessible to the user at the moment. The selection of the
-  produced artifact(s) (`.vo`, `.vio`, `.coq-native`, ...) should be done by
-  a separate flag, and the "ondemand" value removed. Once this is done, use
-  [get_bool] here. *)
-  let n = match s with
-    | ("yes" | "on") -> NativeOn {ondemand=false}
-    | "ondemand" -> NativeOn {ondemand=true}
-    | ("no" | "off") -> NativeOff
-    | _ ->
-       error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") in
-  if Coq_config.native_compiler = NativeOff && n <> NativeOff then
-    let () = warn_no_native_compiler s in
-    NativeOff
-  else
-    n
-
-(* Main parsing routine *)
-(*s Parsing of the command line *)
-
-let parse_args ~help ~init arglist : t * 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
-      | [] -> error_missing_arg opt
-    in
-    let noval = begin match opt with
-
-    (* Complex options with many args *)
-    |"-I"|"-include" ->
-      begin match rem with
-      | d :: rem ->
-        args := rem;
-        add_ml_include oval d
-      | [] -> error_missing_arg opt
-      end
-    |"-Q" ->
-      begin match rem with
-      | d :: p :: rem ->
-        args := rem;
-        add_vo_include oval d p false
-      | _ -> error_missing_arg opt
-      end
-    |"-R" ->
-      begin match rem with
-      | d :: p :: rem ->
-        args := rem;
-        add_vo_include oval d p true
-      | _ -> error_missing_arg opt
-      end
-
-    (* Options with one arg *)
-    |"-coqlib" ->
-      { oval with config = { oval.config with coqlib = Some (next ())
-      }}
-
-    |"-async-proofs" ->
-      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
-        Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next())
-      }}}
-    |"-async-proofs-j" ->
-      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
-        Stm.AsyncOpts.async_proofs_n_workers = (get_int opt (next ()))
-      }}}
-    |"-async-proofs-cache" ->
-      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
-        Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ())
-      }}}
-
-    |"-async-proofs-tac-j" ->
-      let j = get_int opt (next ()) in
-      if j <= 0 then begin
-        error_wrong_arg ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1")
-      end;
-      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
-        Stm.AsyncOpts.async_proofs_n_tacworkers = j
-      }}}
-
-    |"-async-proofs-worker-priority" ->
-      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
-        Stm.AsyncOpts.async_proofs_worker_priority = get_priority opt (next ())
-      }}}
-
-    |"-async-proofs-private-flags" ->
-      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
-        Stm.AsyncOpts.async_proofs_private_flags = Some (next ());
-      }}}
-
-    |"-async-proofs-tactic-error-resilience" ->
-      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
-        Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ())
-      }}}
-
-    |"-async-proofs-command-error-resilience" ->
-      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
-        Stm.AsyncOpts.async_proofs_cmd_error_resilience = get_bool opt (next ())
-      }}}
-
-    |"-async-proofs-delegation-threshold" ->
-      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
-        Stm.AsyncOpts.async_proofs_delegation_threshold = get_float opt (next ())
-      }}}
-
-    |"-worker-id" -> set_worker_id opt (next ()); oval
-
-    |"-compat" ->
-      add_vo_require oval (get_compat_file (next ())) None (Some false)
-
-    |"-exclude-dir" ->
-      System.exclude_directory (next ()); oval
-
-    |"-init-file" ->
-      { oval with config = { oval.config with rcfile = Some (next ()); }}
-
-    |"-inputstate"|"-is" ->
-      set_inputstate oval (next ())
-
-    |"-load-vernac-object" ->
-      add_vo_require oval (next ()) None None
-
-    |"-load-vernac-source"|"-l" ->
-      add_load_vernacular oval false (next ())
-
-    |"-load-vernac-source-verbose"|"-lv" ->
-      add_load_vernacular oval true (next ())
-
-    |"-mangle-names" ->
-      Goptions.set_bool_option_value ["Mangle"; "Names"] true;
-      Goptions.set_string_option_value ["Mangle"; "Names"; "Prefix"] (next ());
-      oval
-
-    |"-print-mod-uid" ->
-      let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0
-
-    |"-profile-ltac-cutoff" ->
-      Flags.profile_ltac := true;
-      Flags.profile_ltac_cutoff := get_float opt (next ());
-      oval
-
-    |"-rfrom" ->
-      let from = next () in add_vo_require oval (next ()) (Some from) None
-
-    |"-require-import" | "-ri" -> add_vo_require oval (next ()) None (Some false)
-
-    |"-require-export" | "-re" -> add_vo_require oval (next ()) None (Some true)
-
-    |"-require-import-from" | "-rifrom" ->
-      let from = next () in add_vo_require oval (next ()) (Some from) (Some false)
-
-    |"-require-export-from" | "-refrom" ->
-      let from = next () in add_vo_require oval (next ()) (Some from) (Some true)
-
-    |"-top" ->
-      let topname = Libnames.dirpath_of_string (next ()) in
-      if Names.DirPath.is_empty topname then
-        CErrors.user_err Pp.(str "Need a non empty toplevel module name");
-      { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = Stm.TopLogical topname }}}
-
-    |"-topfile" ->
-      { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = Stm.TopPhysical (next()) }}}
-
-    |"-main-channel" ->
-      Spawned.main_channel := get_host_port opt (next()); oval
-
-    |"-control-channel" ->
-      Spawned.control_channel := get_host_port opt (next()); oval
-
-    |"-w" | "-W" ->
-      let w = next () in
-      if w = "none" then add_set_option oval ["Warnings"] (Stm.OptionSet(Some w))
-      else add_set_option oval ["Warnings"] (Stm.OptionAppend w)
-
-    |"-bytecode-compiler" ->
-      { oval with config = { oval.config with enable_VM = get_bool opt (next ()) }}
-
-    |"-native-compiler" ->
-      let native_compiler = get_native_compiler (next ()) in
-      { oval with config = { oval.config with native_compiler }}
-
-    | "-set" ->
-      let opt, v = parse_option_set @@ next() in
-      add_set_option oval opt (Stm.OptionSet v)
-
-    | "-unset" ->
-      add_set_option oval (to_opt_key @@ next ()) Stm.OptionUnset
-
-    |"-native-output-dir" ->
-      let native_output_dir = next () in
-      { oval with config = { oval.config with native_output_dir } }
-
-    |"-nI" ->
-      let include_dir = next () in
-      { oval with config = {oval.config with native_include_dirs = include_dir :: oval.config.native_include_dirs } }
-
-    (* Options with zero arg *)
-    |"-async-queries-always-delegate"
-    |"-async-proofs-always-delegate"
-    |"-async-proofs-never-reopen-branch" ->
-      { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
-        Stm.AsyncOpts.async_proofs_never_reopen_branch = true
-      }}}
-    |"-test-mode" -> Vernacinterp.test_mode := true; oval
-    |"-beautify" -> Flags.beautify := true; oval
-    |"-bt" -> Exninfo.record_backtrace true; oval
-    |"-color" -> set_color oval (next ())
-    |"-config"|"--config" -> set_query oval PrintConfig
-    |"-debug" -> Coqinit.set_debug (); oval
-    |"-xml-debug" -> Flags.xml_debug := true; Coqinit.set_debug (); oval
-    |"-diffs" ->
-      add_set_option oval Proof_diffs.opt_name @@ Stm.OptionSet (Some (next ()))
-    |"-stm-debug" -> Stm.stm_debug := true; oval
-    |"-emacs" -> set_emacs oval
-    |"-impredicative-set" ->
-      set_logic (fun o -> { o with impredicative_set = Declarations.ImpredicativeSet }) oval
-    |"-allow-sprop" ->
-      add_set_option oval Vernacentries.allow_sprop_opt_name (Stm.OptionSet None)
-    |"-disallow-sprop" ->
-      add_set_option oval Vernacentries.allow_sprop_opt_name Stm.OptionUnset
-    |"-sprop-cumulative" ->
-      warn_deprecated_sprop_cumul();
-      add_set_option oval Vernacentries.cumul_sprop_opt_name (Stm.OptionSet None)
-    |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval
-    |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }}
-    |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }}
-    |"-boot" -> { oval with pre = { oval.pre with boot = true }}
-    |"-output-context" -> { oval with post = { oval.post with output_context = true }}
-    |"-profile-ltac" -> Flags.profile_ltac := true; oval
-    |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }}
-    |"-quiet"|"-silent" ->
-      Flags.quiet := true;
-      Flags.make_warn false;
-      oval
-    |"-list-tags" -> set_query oval PrintTags
-    |"-time" -> { oval with config = { oval.config with time = true }}
-    |"-type-in-type" -> set_type_in_type (); oval
-    |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false)
-    |"-where" -> set_query oval PrintWhere
-    |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp help)
-    |"-v"|"--version" -> set_query oval PrintVersion
-    |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion
-
-    (* Unknown option *)
-    | s ->
-      extras := s :: !extras;
-      oval
-    end in
-    parse noval
-  in
-  try
-    parse init
-  with any -> fatal_error any
-
-(* We need to reverse a few lists *)
-let parse_args ~help ~init args =
-  let opts, extra = parse_args ~help ~init args in
-  let opts =
-    { opts with
-      pre = { opts.pre with
-              ml_includes = List.rev opts.pre.ml_includes
-            ; vo_includes = List.rev opts.pre.vo_includes
-            ; load_vernacular_list = List.rev opts.pre.load_vernacular_list
-            ; injections = List.rev opts.pre.injections
-            }
-    } in
-  opts, extra
-
-(******************************************************************************)
-(* Startup LoadPath and Modules                                               *)
-(******************************************************************************)
-(* prelude_data == From Coq Require Import Prelude. *)
-let prelude_data = "Prelude", Some "Coq", Some false
-
-let injection_commands opts =
-  if opts.pre.load_init then Stm.RequireInjection prelude_data :: opts.pre.injections else opts.pre.injections
-
-let build_load_path opts =
-  let ml_path, vo_path =
-    if opts.pre.boot then [],[]
-    else
-      let coqlib = Envars.coqlib () in
-      Coqinit.libs_init_load_path ~coqlib in
-  ml_path @ opts.pre.ml_includes ,
-  vo_path @ opts.pre.vo_includes
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
deleted file mode 100644
index f6222e4ec4..0000000000
--- a/toplevel/coqargs.mli
+++ /dev/null
@@ -1,81 +0,0 @@
-(************************************************************************)
-(*         *   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)         *)
-(************************************************************************)
-
-type color = [`ON | `AUTO | `EMACS | `OFF]
-
-val default_toplevel : Names.DirPath.t
-
-type native_compiler = Coq_config.native_compiler =
-  NativeOff | NativeOn of { ondemand : bool }
-
-type coqargs_logic_config = {
-  impredicative_set : Declarations.set_predicativity;
-  indices_matter    : bool;
-  toplevel_name     : Stm.interactive_top;
-}
-
-type coqargs_config = {
-  logic       : coqargs_logic_config;
-  rcfile      : string option;
-  coqlib      : string option;
-  color       : color;
-  enable_VM   : bool;
-  native_compiler : native_compiler;
-  native_output_dir : CUnix.physical_path;
-  native_include_dirs : CUnix.physical_path list;
-  stm_flags   : Stm.AsyncOpts.stm_opt;
-  debug       : bool;
-  time        : bool;
-  print_emacs : bool;
-}
-
-type coqargs_pre = {
-  boot        : bool;
-  load_init   : bool;
-  load_rcfile : bool;
-
-  ml_includes : CUnix.physical_path list;
-  vo_includes : Loadpath.vo_path list;
-
-  load_vernacular_list : (string * bool) list;
-  injections  : Stm.injection_command list;
-
-  inputstate  : string option;
-}
-
-type coqargs_query =
-  | PrintTags | PrintWhere | PrintConfig
-  | PrintVersion | PrintMachineReadableVersion
-  | PrintHelp of Usage.specific_usage
-
-type coqargs_main =
-  | Queries of coqargs_query list
-  | Run
-
-type coqargs_post = {
-  memory_stat : bool;
-  output_context : bool;
-}
-
-type t = {
-  config : coqargs_config;
-  pre : coqargs_pre;
-  main : coqargs_main;
-  post : coqargs_post;
-}
-
-(* Default options *)
-val default : t
-
-val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * string list
-val error_wrong_arg : string -> unit
-
-val injection_commands : t -> Stm.injection_command list
-val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index 03c53d6991..0c23c9f4e9 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -41,9 +41,9 @@ coqc specific options:\
 \n"
 }
 
-let coqc_main copts ~opts =
+let coqc_main (copts,stm_opts) ~opts =
   Topfmt.(in_phase ~phase:CompilationPhase)
-    Ccompile.compile_files opts copts;
+    Ccompile.compile_files (opts,stm_opts) copts;
 
   (* Careful this will modify the load-path and state so after this
      point some stuff may not be safe anymore. *)
@@ -73,8 +73,11 @@ let coqc_run copts ~opts () =
     let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
     exit exit_code
 
-let custom_coqc = Coqtop.{
-  parse_extra = (fun ~opts extras -> Coqcargs.parse extras, []);
+let custom_coqc : (Coqcargs.t * Stm.AsyncOpts.stm_opt, 'b) Coqtop.custom_toplevel
+ = Coqtop.{
+  parse_extra = (fun ~opts extras ->
+    let stm_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in
+    (Coqcargs.parse extras, stm_opts), []);
   help = coqc_specific_usage;
   init = coqc_init;
   run = coqc_run;
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
deleted file mode 100644
index 501047c520..0000000000
--- a/toplevel/coqinit.ml
+++ /dev/null
@@ -1,111 +0,0 @@
-(************************************************************************)
-(*         *   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)         *)
-(************************************************************************)
-
-open Util
-open Pp
-
-let ( / ) s1 s2 = Filename.concat s1 s2
-
-let set_debug () =
-  let () = Exninfo.record_backtrace true in
-  Flags.debug := true
-
-(* Loading of the resource file.
-   rcfile is either $XDG_CONFIG_HOME/.coqrc.VERSION, or $XDG_CONFIG_HOME/.coqrc if the first one
-  does not exist. *)
-
-let rcdefaultname = "coqrc"
-
-let load_rcfile ~rcfile ~state =
-    try
-      match rcfile with
-      | Some rcfile ->
-        if CUnix.file_readable_p rcfile then
-          Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state rcfile
-        else raise (Sys_error ("Cannot read rcfile: "^ rcfile))
-      | None ->
-        try
-          let warn x = Feedback.msg_warning (str x) in
-          let inferedrc = List.find CUnix.file_readable_p [
-            Envars.xdg_config_home warn / rcdefaultname^"."^Coq_config.version;
-            Envars.xdg_config_home warn / rcdefaultname;
-            Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
-            Envars.home ~warn / "."^rcdefaultname
-          ] in
-          Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state inferedrc
-        with Not_found -> state
-        (*
-        Flags.if_verbose
-          mSGNL (str ("No coqrc or coqrc."^Coq_config.version^
-                         " found. Skipping rcfile loading."))
-        *)
-    with reraise ->
-      let reraise = Exninfo.capture reraise in
-      let () = Feedback.msg_info (str"Load of rcfile failed.") in
-      Exninfo.iraise reraise
-
-(* Recursively puts `.v` files in the LoadPath *)
-let build_stdlib_vo_path ~unix_path ~coq_path =
-  let open Loadpath in
-  { unix_path; coq_path ; has_ml = false; implicit = true; recursive = true }
-
-(* Note we don't use has_ml=true due to #12771 , we need to see if we
-   should just remove that option *)
-let build_userlib_path ~unix_path =
-  let open Loadpath in
-  if Sys.file_exists unix_path then
-    let ml_path = System.all_subdirs ~unix_path |> List.map fst in
-    let vo_path =
-      { unix_path
-      ; coq_path = Libnames.default_root_prefix
-      ; has_ml = false
-      ; implicit = false
-      ; recursive = true
-      } in
-    ml_path, [vo_path]
-  else [], []
-
-(* LoadPath for Coq user libraries *)
-let libs_init_load_path ~coqlib =
-
-  let open Loadpath in
-  let user_contrib = coqlib/"user-contrib" in
-  let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in
-  let coqpath = Envars.coqpath in
-  let coq_path = Names.DirPath.make [Libnames.coq_root] in
-
-  (* ML includes *)
-  let plugins_dirs = System.all_subdirs ~unix_path:(coqlib/"plugins") |> List.map fst in
-
-  let contrib_ml, contrib_vo = build_userlib_path ~unix_path:user_contrib in
-
-  let misc_ml, misc_vo =
-    List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) |> List.split in
-
-  let ml_loadpath = plugins_dirs @ contrib_ml @ List.concat misc_ml in
-  let vo_loadpath =
-    (* current directory (not recursively!) *)
-    [ { unix_path = "."
-      ; coq_path = Libnames.default_root_prefix
-      ; implicit = false
-      ; has_ml = true
-      ; recursive = false
-      } ] @
-
-    (* then standard library *)
-    [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @
-
-    (* then user-contrib *)
-    contrib_vo @
-
-    (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *)
-    List.concat misc_vo
-  in
-  ml_loadpath, vo_loadpath
diff --git a/toplevel/coqrc.ml b/toplevel/coqrc.ml
new file mode 100644
index 0000000000..e074e621da
--- /dev/null
+++ b/toplevel/coqrc.ml
@@ -0,0 +1,45 @@
+(************************************************************************)
+(*         *   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 ( / ) s1 s2 = Filename.concat s1 s2
+
+(* Loading of the resource file.
+   rcfile is either $XDG_CONFIG_HOME/.coqrc.VERSION, or $XDG_CONFIG_HOME/.coqrc if the first one
+  does not exist. *)
+
+let rcdefaultname = "coqrc"
+
+let load_rcfile ~rcfile ~state =
+    try
+      match rcfile with
+      | Some rcfile ->
+        if CUnix.file_readable_p rcfile then
+          Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state rcfile
+        else raise (Sys_error ("Cannot read rcfile: "^ rcfile))
+      | None ->
+        try
+          let warn x = Feedback.msg_warning (Pp.str x) in
+          let inferedrc = List.find CUnix.file_readable_p [
+            Envars.xdg_config_home warn / rcdefaultname^"."^Coq_config.version;
+            Envars.xdg_config_home warn / rcdefaultname;
+            Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
+            Envars.home ~warn / "."^rcdefaultname
+          ] in
+          Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state inferedrc
+        with Not_found -> state
+        (*
+        Flags.if_verbose
+          mSGNL (str ("No coqrc or coqrc."^Coq_config.version^
+                         " found. Skipping rcfile loading."))
+        *)
+    with reraise ->
+      let reraise = Exninfo.capture reraise in
+      let () = Feedback.msg_info (Pp.str"Load of rcfile failed.") in
+      Exninfo.iraise reraise
diff --git a/toplevel/coqinit.mli b/toplevel/coqrc.mli
index b96a0ef162..3b8a31b2a5 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqrc.mli
@@ -8,15 +8,4 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** Initialization. *)
-
-val set_debug : unit -> unit
-
 val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State.t
-
-(** Standard LoadPath for Coq user libraries; in particular it
-   includes (in-order) Coq's standard library, Coq's [user-contrib]
-   folder, and directories specified in [COQPATH] and [XDG_DIRS] *)
-val libs_init_load_path
-  : coqlib:CUnix.physical_path
-  -> CUnix.physical_path list * Loadpath.vo_path list
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index d0d50aee70..7596df788b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -198,11 +198,7 @@ let init_parse parse_extra help init_opts =
 
 (** Coq's init process, phase 2: Basic Coq environment, plugins. *)
 let init_execution opts custom_init =
-  (* If we have been spawned by the Spawn module, this has to be done
-   * early since the master waits us to connect back *)
-  Spawned.init_channels ();
   if opts.post.memory_stat then at_exit print_memory_stat;
-  CoqworkmgrApi.(init opts.config.stm_flags.Stm.AsyncOpts.async_proofs_worker_priority);
   Mltop.init_known_plugins ();
   (* Configuration *)
   Global.set_engagement opts.config.logic.impredicative_set;
@@ -241,10 +237,11 @@ let init_toplevel custom =
   | Queries q -> List.iter (print_query opts) q; exit 0
   | Run ->
     let () = init_coqlib opts in
+    Stm.init_process (snd customopts);
     let customstate = init_execution opts (custom.init customopts) in
     opts, customopts, customstate
 
-let init_document opts =
+let init_document opts stm_options =
   (* Coq init process, phase 3: Stm initialization, backtracking state.
 
      It is essential that the module system is in a consistent
@@ -255,7 +252,6 @@ let init_document opts =
   Flags.load_vos_libraries := true;
   let ml_load_path, vo_load_path = build_load_path opts in
   let injections = injection_commands opts in
-  let stm_options = opts.config.stm_flags in
   let open Vernac.State in
   let doc, sid =
     Stm.(new_doc
@@ -281,16 +277,16 @@ let start_coq custom =
 
 type run_mode = Interactive | Batch
 
-let init_toploop opts =
-  let state = init_document opts in
+let init_toploop opts stm_opts =
+  let state = init_document opts stm_opts in
   let state = Ccompile.load_init_vernaculars opts ~state in
   state
 
-let coqtop_init run_mode ~opts =
+let coqtop_init (run_mode,stm_opts) ~opts =
   if run_mode = Batch then Flags.quiet := true;
   init_color opts.config;
   Flags.if_verbose print_header ();
-  init_toploop opts
+  init_toploop opts stm_opts
 
 let coqtop_parse_extra ~opts extras =
   let rec parse_extra run_mode = function
@@ -299,9 +295,10 @@ let coqtop_parse_extra ~opts extras =
     let run_mode, rest = parse_extra run_mode rest in run_mode, x :: rest
   | [] -> run_mode, [] in
   let run_mode, extras = parse_extra Interactive extras in
-  run_mode, extras
+  let stm_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in
+  (run_mode, stm_opts), extras
 
-let coqtop_run run_mode ~opts state =
+let coqtop_run (run_mode,_) ~opts state =
   match run_mode with
   | Interactive -> Coqloop.loop ~opts ~state;
   | Batch -> exit 0
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index e535c19252..9ae0d86cf1 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -28,7 +28,7 @@ type ('a,'b) custom_toplevel =
    load the files given on the command line, load the resource file,
    produce the output state if any, and finally will launch
    [custom.run]. *)
-val start_coq : ('a,'b) custom_toplevel -> unit
+val start_coq : ('a * Stm.AsyncOpts.stm_opt,'b) custom_toplevel -> unit
 
 (** Initializer color for output *)
 
@@ -36,10 +36,10 @@ val init_color : Coqargs.coqargs_config -> unit
 
 (** Prepare state for interactive loop *)
 
-val init_toploop : Coqargs.t -> Vernac.State.t
+val init_toploop : Coqargs.t -> Stm.AsyncOpts.stm_opt -> Vernac.State.t
 
 (** The specific characterization of the coqtop_toplevel *)
 
 type run_mode = Interactive | Batch
 
-val coqtop_toplevel : (run_mode,Vernac.State.t) custom_toplevel
+val coqtop_toplevel : (run_mode * Stm.AsyncOpts.stm_opt,Vernac.State.t) custom_toplevel
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index ddd11fd160..90f8fb9686 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -1,7 +1,5 @@
 Vernac
-Usage
-Coqinit
-Coqargs
+Coqrc
 Coqcargs
 G_toplevel
 Coqloop
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
deleted file mode 100644
index 6fb5f821ee..0000000000
--- a/toplevel/usage.ml
+++ /dev/null
@@ -1,113 +0,0 @@
-(************************************************************************)
-(*         *   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 version () =
-  Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
-    Coq_config.version Coq_config.date;
-  Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version
-
-let machine_readable_version () =
-  Printf.printf "%s %s\n"
-    Coq_config.version Coq_config.caml_version
-
-(* print the usage of coqtop (or coqc) on channel co *)
-
-let print_usage_common co command =
-  output_string co command;
-  output_string co "Coq options are:\n";
-  output_string co
-"  -I dir                 look for ML files in dir\
-\n  -include dir           (idem)\
-\n  -R dir coqdir          recursively map physical dir to logical coqdir\
-\n  -Q dir coqdir          map physical dir to logical coqdir\
-\n  -top coqdir            set the toplevel name to be coqdir instead of Top\
-\n  -topfile f             set the toplevel name as though compiling f\
-\n  -coqlib dir            set the coq standard library directory\
-\n  -exclude-dir f         exclude subdirectories named f for option -R\
-\n\
-\n  -boot                  don't bind the `Coq.` prefix to the default -coqlib dir\
-\n  -noinit                don't load Coq.Init.Prelude on start \
-\n  -nois                  (idem)\
-\n  -compat X.Y            provides compatibility support for Coq version X.Y\
-\n\
-\n  -load-vernac-source f  load Coq file f.v (Load \"f\".)\
-\n  -l f                   (idem)\
-\n  -load-vernac-source-verbose f  load Coq file f.v (Load Verbose \"f\".)\
-\n  -lv f	           (idem)\
-\n  -load-vernac-object lib\
-\n                         load Coq library lib (Require lib)\
-\n  -rfrom root lib        load Coq library lib (From root Require lib.)\
-\n  -require-import lib, -ri lib\
-\n                         load and import Coq library lib\
-\n                         (equivalent to Require Import lib.)\
-\n  -require-export lib, -re lib\
-\n                         load and transitively import Coq library lib\
-\n                         (equivalent to Require Export lib.)\
-\n  -require-import-from root lib, -rifrom root lib\
-\n                         load and import Coq library lib\
-\n                         (equivalent to From root Require Import lib.)\
-\n  -require-export-from root lib, -refrom root lib\
-\n                         load and transitively import Coq library lib\
-\n                         (equivalent to From root Require Export lib.)\
-\n\
-\n  -where                 print Coq's standard library location and exit\
-\n  -config, --config      print Coq's configuration information and exit\
-\n  -v, --version          print Coq version and exit\
-\n  -print-version         print Coq version in easy to parse format and exit\
-\n  -list-tags             print highlight color tags known by Coq and exit\
-\n\
-\n  -quiet                 unset display of extra information (implies -w \"-all\")\
-\n  -w (w1,..,wn)          configure display of warnings\
-\n  -color (yes|no|auto)   configure color output\
-\n  -emacs                 tells Coq it is executed under Emacs\
-\n\
-\n  -q                     skip loading of rcfile\
-\n  -init-file f           set the rcfile to f\
-\n  -bt                    print backtraces (requires configure debug flag)\
-\n  -debug                 debug mode (implies -bt)\
-\n  -xml-debug             debug mode and print XML messages to/from coqide\
-\n  -diffs (on|off|removed) highlight differences between proof steps\
-\n  -stm-debug             STM debug mode (will trace every transaction)\
-\n  -noglob                do not dump globalizations\
-\n  -dump-glob f           dump globalizations in file f (to be used by coqdoc)\
-\n  -impredicative-set     set sort Set impredicative\
-\n  -allow-sprop           allow using the proof irrelevant SProp sort\
-\n  -disallow-sprop        forbid using the proof irrelevant SProp sort\
-\n  -sprop-cumulative      make sort SProp cumulative with the rest of the hierarchy\
-\n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
-\n  -type-in-type          disable universe consistency checking\
-\n  -mangle-names x        mangle auto-generated names using prefix x\
-\n  -set \"Foo Bar\"         enable Foo Bar (as Set Foo Bar. in a file)\
-\n  -set \"Foo Bar=value\"   set Foo Bar to value (value is interpreted according to Foo Bar's type)\
-\n  -unset \"Foo Bar\"       disable Foo Bar (as Unset Foo Bar. in a file)\
-\n  -time                  display the time taken by each command\
-\n  -profile-ltac          display the time taken by each (sub)tactic\
-\n  -m, --memory           display total heap size at program exit\
-\n                         (use environment variable\
-\n                          OCAML_GC_STATS=\"/tmp/gclog.txt\"\
-\n                          for full Gc stats dump)\
-\n  -bytecode-compiler (yes|no)        enable the vm_compute reduction machine\
-\n  -native-compiler (yes|no|ondemand) enable the native_compute reduction machine\
-\n  -native-output-dir     <directory> set the output directory for native objects\
-\n  -nI dir                OCaml include directories for the native compiler (default if not set) \
-\n  -h, -help, --help      print this list of options\
-\n"
-
-(* print the usage *)
-
-type specific_usage = {
-  executable_name : string;
-  extra_args : string;
-  extra_options : string;
-}
-
-let print_usage co { executable_name; extra_args; extra_options } =
-  print_usage_common co ("Usage: " ^ executable_name ^ " <options> " ^ extra_args ^ "\n\n");
-  output_string co extra_options
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
deleted file mode 100644
index cbc3b4f7e8..0000000000
--- a/toplevel/usage.mli
+++ /dev/null
@@ -1,29 +0,0 @@
-(************************************************************************)
-(*         *   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)         *)
-(************************************************************************)
-
-(** {6 Prints the version number on the standard output. } *)
-
-val version : unit -> unit
-val machine_readable_version : unit -> unit
-
-(** {6 extra arguments or options to print when asking usage for a
-     given executable. } *)
-
-type specific_usage = {
-  executable_name : string;
-  extra_args : string;
-  extra_options : string;
-}
-
-(** {6 Prints the generic part and specific part of usage for a
-       given executable. } *)
-
-val print_usage : out_channel -> specific_usage -> unit
-
diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml
index 59e10b09a0..b0d7bb6f78 100644
--- a/toplevel/workerLoop.ml
+++ b/toplevel/workerLoop.ml
@@ -9,9 +9,10 @@
 (************************************************************************)
 
 let worker_parse_extra ~opts extra_args =
-  (), extra_args
+  let stm_opts, extra_args = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extra_args in
+  ((),stm_opts), extra_args
 
-let worker_init init () ~opts =
+let worker_init init ((),_) ~opts =
   Flags.quiet := true;
   init ();
   Coqtop.init_toploop opts
@@ -30,6 +31,6 @@ let start ~init ~loop name =
     help = worker_specific_usage name;
     opts = Coqargs.default;
     init = worker_init init;
-    run = (fun () ~opts:_ _state (* why is state not used *) -> loop ());
+    run = (fun ((),_) ~opts:_ _state (* why is state not used *) -> loop ());
   } in
   start_coq custom