Merge PR #13418: [sysinit] new component

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: JasonGross

16 files changed, 212 insertions, 1162 deletions

diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index b75a4199ea..ca09bad441 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 injections 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
@@ -104,9 +104,6 @@ let compile opts copts ~echo ~f_in ~f_out =
                         |> prlist_with_sep pr_comma Names.Id.print)
                     ++ str ".")
   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
@@ -129,9 +126,7 @@ let compile opts copts ~echo ~f_in ~f_out =
   | BuildVo | BuildVok ->
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
           Stm.new_doc
-          Stm.{ doc_type = VoDoc long_f_dot_out; ml_load_path;
-                vo_load_path; injections; stm_options;
-              } in
+          Stm.{ doc_type = VoDoc long_f_dot_out; injections; stm_options; } in
       let state = { doc; sid; proof = None; time = opts.config.time } in
       let state = load_init_vernaculars opts ~state in
       let ldir = Stm.get_ldir ~doc:state.doc in
@@ -181,8 +176,7 @@ let compile opts copts ~echo ~f_in ~f_out =
 
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
           Stm.new_doc
-          Stm.{ doc_type = VioDoc long_f_dot_out; ml_load_path;
-                vo_load_path; injections; stm_options;
+          Stm.{ doc_type = VioDoc long_f_dot_out; injections; stm_options;
               } in
 
       let state = { doc; sid; proof = None; time = opts.config.time } in
@@ -209,22 +203,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 injections ~echo ~f_in ~f_out =
   ignore(CoqworkmgrApi.get 1);
-  compile opts copts ~echo ~f_in ~f_out;
+  compile opts stm_opts injections copts ~echo ~f_in ~f_out;
   CoqworkmgrApi.giveback 1
 
-let compile_file opts copts (f_in, echo) =
+let compile_file opts stm_opts copts injections (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 injections ~echo ~f_in ~f_out) f_in
   else
-    compile opts copts ~echo ~f_in ~f_out
+    compile opts stm_opts copts injections ~echo ~f_in ~f_out
 
-let compile_files opts copts =
+let compile_files (opts, stm_opts) copts injections =
   let compile_list = copts.compile_list in
-  List.iter (compile_file opts copts) compile_list
+  List.iter (compile_file opts stm_opts copts injections) compile_list
 
 (******************************************************************************)
 (* VIO Dispatching                                                            *)
@@ -248,14 +242,7 @@ let schedule_vio copts =
   else
     Vio_checking.schedule_vio_compilation copts.vio_files_j l
 
-let do_vio opts copts =
-  (* We must initialize the loadpath here as the vio scheduling
-     process happens outside of the STM *)
-  if copts.vio_files <> [] || copts.vio_tasks <> [] then
-    let ml_lp, vo_lp = build_load_path opts in
-    List.iter Mltop.add_ml_dir ml_lp;
-    List.iter Loadpath.add_vo_path vo_lp;
-
+let do_vio opts copts _injections =
   (* Vio compile pass *)
   if copts.vio_files <> [] then schedule_vio copts;
   (* Vio task pass *)
diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli
index 8c154488d0..9f3783f32e 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 -> Coqargs.injection_command list -> unit
 
 (** [do_vio opts] process [.vio] files in [opts] *)
-val do_vio : Coqargs.t -> Coqcargs.t -> unit
+val do_vio : Coqargs.t -> Coqcargs.t -> Coqargs.injection_command list -> 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..a403640149 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -13,10 +13,11 @@ let outputstate opts =
     let fname = CUnix.make_suffix ostate_file ".coq" in
     Vernacstate.System.dump fname) opts.Coqcargs.outputstate
 
-let coqc_init _copts ~opts =
+let coqc_init ((_,color_mode),_) injections ~opts =
   Flags.quiet := true;
   System.trust_file_cache := true;
-  Coqtop.init_color opts.Coqargs.config
+  Coqtop.init_color (if opts.Coqargs.config.Coqargs.print_emacs then `EMACS else color_mode);
+  injections
 
 let coqc_specific_usage = Usage.{
   executable_name = "coqc";
@@ -41,30 +42,30 @@ coqc specific options:\
 \n"
 }
 
-let coqc_main copts ~opts =
+let coqc_main ((copts,_),stm_opts) injections ~opts =
   Topfmt.(in_phase ~phase:CompilationPhase)
-    Ccompile.compile_files opts copts;
+    Ccompile.compile_files (opts,stm_opts) copts injections;
 
   (* Careful this will modify the load-path and state so after this
      point some stuff may not be safe anymore. *)
   Topfmt.(in_phase ~phase:CompilationPhase)
-    Ccompile.do_vio opts copts;
+    Ccompile.do_vio opts copts injections;
 
   (* Allow the user to output an arbitrary state *)
   outputstate copts;
 
   flush_all();
 
-  if opts.Coqargs.post.Coqargs.output_context then begin
+  if copts.Coqcargs.output_context then begin
     let sigma, env = let e = Global.env () in Evd.from_env e, e in
     Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ())
   end;
   CProfile.print_profile ()
 
-let coqc_run copts ~opts () =
+let coqc_run copts ~opts injections =
   let _feeder = Feedback.add_feeder Coqloop.coqloop_feed in
   try
-    coqc_main ~opts copts;
+    coqc_main ~opts copts injections;
     exit 0
   with exn ->
     flush_all();
@@ -73,12 +74,17 @@ 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, []);
-  help = coqc_specific_usage;
-  init = coqc_init;
+let custom_coqc : ((Coqcargs.t * Coqtop.color) * Stm.AsyncOpts.stm_opt, 'b) Coqtop.custom_toplevel
+ = Coqtop.{
+  parse_extra = (fun extras ->
+    let color_mode, extras = Coqtop.parse_extra_colors extras in
+    let stm_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in
+    let coqc_opts = Coqcargs.parse extras in
+    ((coqc_opts, color_mode), stm_opts), []);
+  usage = coqc_specific_usage;
+  init_extra = coqc_init;
   run = coqc_run;
-  opts = Coqargs.default;
+  initial_args = Coqargs.default;
 }
 
 let main () =
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml
index 402a4d83c9..f84d73ed17 100644
--- a/toplevel/coqcargs.ml
+++ b/toplevel/coqcargs.ml
@@ -25,6 +25,8 @@ type t =
 
   ; outputstate : string option
   ; glob_out    : Dumpglob.glob_output
+
+  ; output_context : bool
   }
 
 let default =
@@ -42,6 +44,8 @@ let default =
 
   ; outputstate = None
   ; glob_out = Dumpglob.MultFiles
+
+  ; output_context = false
   }
 
 let depr opt =
@@ -162,6 +166,10 @@ let parse arglist : t =
           depr opt;
           let _ = next () in
           oval
+
+        (* Non deprecated options *)
+        | "-output-context" ->
+          { oval with output_context = true }
         (* Verbose == echo mode *)
         | "-verbose" ->
           echo := true;
diff --git a/toplevel/coqcargs.mli b/toplevel/coqcargs.mli
index a9fc27b1b4..905250e363 100644
--- a/toplevel/coqcargs.mli
+++ b/toplevel/coqcargs.mli
@@ -39,6 +39,8 @@ type t =
 
   ; outputstate : string option
   ; glob_out    : Dumpglob.glob_output
+
+  ; output_context : bool
   }
 
 val default : t
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..caf86ef870 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -33,18 +33,6 @@ let print_header () =
   Feedback.msg_info (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
   flush_all ()
 
-let print_memory_stat () =
-  (* -m|--memory from the command-line *)
-  Feedback.msg_notice
-    (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ());
-  (* operf-macro interface:
-     https://github.com/OCamlPro/operf-macro *)
-  try
-    let fn = Sys.getenv "OCAML_GC_STATS" in
-    let oc = open_out fn in
-    Gc.print_stat oc;
-    close_out oc
-  with _ -> ()
 
 (******************************************************************************)
 (* Input/Output State                                                         *)
@@ -68,11 +56,46 @@ let fatal_error_exn exn =
   in
   exit exit_code
 
-(******************************************************************************)
-(* Color Options                                                              *)
-(******************************************************************************)
+type ('a,'b) custom_toplevel =
+  { parse_extra : string list -> 'a * string list
+  ; usage : Usage.specific_usage
+  ; init_extra : 'a -> Coqargs.injection_command list -> opts:Coqargs.t -> 'b
+  ; initial_args : Coqargs.t
+  ; run : 'a -> opts:Coqargs.t -> 'b -> unit
+  }
+
+(** Main init routine *)
+let init_toplevel { parse_extra; init_extra; usage; initial_args } =
+  Coqinit.init_ocaml ();
+  let opts, customopts = Coqinit.parse_arguments ~parse_extra ~usage ~initial_args () in
+  Stm.init_process (snd customopts);
+  let injections = Coqinit.init_runtime opts in
+  (* Allow the user to load an arbitrary state here *)
+  inputstate opts.pre;
+  (* This state will be shared by all the documents *)
+  Stm.init_core ();
+  let customstate = init_extra ~opts customopts injections in
+  opts, customopts, customstate
+
+let start_coq custom =
+  let init_feeder = Feedback.add_feeder Coqloop.coqloop_feed in
+  (* Init phase *)
+  let opts, custom_opts, state =
+    try init_toplevel custom
+    with any ->
+      flush_all();
+      fatal_error_exn any in
+  Feedback.del_feeder init_feeder;
+  (* Run phase *)
+  custom.run ~opts custom_opts state
+
+(** ****************************************)
+(** Specific support for coqtop executable *)
+
+type color = [`ON | `AUTO | `EMACS | `OFF]
+
 let init_color opts =
-  let has_color = match opts.color with
+  let has_color = match opts with
   | `OFF -> false
   | `EMACS -> false
   | `ON -> true
@@ -95,7 +118,7 @@ let init_color opts =
       Topfmt.default_styles (); false                 (* textual markers, no color *)
     end
   in
-  if opts.color = `EMACS then
+  if opts = `EMACS then
     Topfmt.set_emacs_print_strings ()
   else if not term_color then begin
       Proof_diffs.write_color_enabled term_color;
@@ -120,131 +143,15 @@ let print_style_tags opts =
   let () = List.iter iter tags in
   flush_all ()
 
-let init_coqlib opts = match opts.config.coqlib with
-  | None when opts.pre.boot -> ()
-  | None ->
-    Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
-  | Some s ->
-    Envars.set_user_coqlib s
-
-let print_query opts = function
-  | PrintVersion -> Usage.version ()
-  | PrintMachineReadableVersion -> Usage.machine_readable_version ()
-  | PrintWhere ->
-    let () = init_coqlib opts in
-    print_endline (Envars.coqlib ())
-  | PrintHelp h -> Usage.print_usage stderr h
-  | PrintConfig ->
-    let () = init_coqlib opts in
-    Envars.print_config stdout Coq_config.all_src_dirs
-  | PrintTags -> print_style_tags opts.config
-
-(** GC tweaking *)
-
-(** Coq is a heavy user of persistent data structures and symbolic ASTs, so the
-    minor heap is heavily solicited. Unfortunately, the default size is far too
-    small, so we enlarge it a lot (128 times larger).
-
-    To better handle huge memory consumers, we also augment the default major
-    heap increment and the GC pressure coefficient.
-*)
-
-let set_gc_policy () =
-  Gc.set { (Gc.get ()) with
-           Gc.minor_heap_size = 32*1024*1024 (* 32Mwords x 8 bytes/word = 256Mb *)
-         ; Gc.space_overhead = 120
-         }
-
-let set_gc_best_fit () =
-  Gc.set { (Gc.get ()) with
-           Gc.allocation_policy = 2      (* best-fit *)
-         ; Gc.space_overhead = 200
-         }
-
-let init_gc () =
-  try
-    (* OCAMLRUNPARAM environment variable is set.
-     * In that case, we let ocamlrun to use the values provided by the user.
-     *)
-    ignore (Sys.getenv "OCAMLRUNPARAM")
-
-  with Not_found ->
-    (* OCAMLRUNPARAM environment variable is not set.
-     * In this case, we put in place our preferred configuration.
-     *)
-    set_gc_policy ();
-    if Coq_config.caml_version_nums >= [4;10;0] then set_gc_best_fit () else ()
-
-let init_process () =
-  (* Coq's init process, phase 1:
-     OCaml parameters, basic structures, and IO
-   *)
-  CProfile.init_profile ();
-  init_gc ();
-  Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
-  Lib.init ()
-
-let init_parse parse_extra help init_opts =
-  let opts, extras =
-    parse_args ~help:help ~init:init_opts
-      (List.tl (Array.to_list Sys.argv)) in
-  let customopts, extras = parse_extra ~opts extras in
-  if not (CList.is_empty extras) then begin
-    prerr_endline ("Don't know what to do with "^String.concat " " extras);
-    prerr_endline "See -help for the list of supported options";
-    exit 1
-    end;
-  opts, customopts
-
-(** 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;
-  Global.set_indices_matter opts.config.logic.indices_matter;
-  Global.set_VM opts.config.enable_VM;
-  Flags.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true);
-  Global.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true);
-
-  (* Native output dir *)
-  Nativelib.output_dir := opts.config.native_output_dir;
-  Nativelib.include_dirs := opts.config.native_include_dirs;
+type query = PrintTags | PrintModUid of string list
+type run_mode = Interactive | Batch | Query of query
 
-  (* Allow the user to load an arbitrary state here *)
-  inputstate opts.pre;
-
-  (* This state will be shared by all the documents *)
-  Stm.init_core ();
-  custom_init ~opts
-
-type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list
-
-type ('a,'b) custom_toplevel =
-  { parse_extra : 'a extra_args_fn
-  ; help : Usage.specific_usage
-  ; init : 'a -> opts:Coqargs.t -> 'b
-  ; run : 'a -> opts:Coqargs.t -> 'b -> unit
-  ; opts : Coqargs.t
-  }
-
-(** Main init routine *)
-let init_toplevel custom =
-  let () = init_process () in
-  let opts, customopts = init_parse custom.parse_extra custom.help custom.opts in
-  (* Querying or running? *)
-  match opts.main with
-  | Queries q -> List.iter (print_query opts) q; exit 0
-  | Run ->
-    let () = init_coqlib opts in
-    let customstate = init_execution opts (custom.init customopts) in
-    opts, customopts, customstate
+type toplevel_options = {
+  run_mode : run_mode;
+  color_mode : color;
+}
 
-let init_document opts =
+let init_document opts stm_options injections =
   (* Coq init process, phase 3: Stm initialization, backtracking state.
 
      It is essential that the module system is in a consistent
@@ -253,57 +160,70 @@ let init_document opts =
   *)
   (* Next line allows loading .vos files when in interactive mode *)
   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
            { doc_type = Interactive opts.config.logic.toplevel_name;
-             ml_load_path; vo_load_path; injections; stm_options;
+             injections; stm_options;
            }) in
   { doc; sid; proof = None; time = opts.config.time }
 
-let start_coq custom =
-  let init_feeder = Feedback.add_feeder Coqloop.coqloop_feed in
-  (* Init phase *)
-  let opts, custom_opts, state =
-    try init_toplevel custom
-    with any ->
-      flush_all();
-      fatal_error_exn any in
-  Feedback.del_feeder init_feeder;
-  (* Run phase *)
-  custom.run ~opts custom_opts state
-
-(** ****************************************)
-(** Specific support for coqtop executable *)
-
-type run_mode = Interactive | Batch
-
-let init_toploop opts =
-  let state = init_document opts in
+let init_toploop opts stm_opts injections =
+  let state = init_document opts stm_opts injections in
   let state = Ccompile.load_init_vernaculars opts ~state in
   state
 
-let coqtop_init run_mode ~opts =
+let coqtop_init ({ run_mode; color_mode }, async_opts) injections ~opts =
   if run_mode = Batch then Flags.quiet := true;
-  init_color opts.config;
+  init_color (if opts.config.print_emacs then `EMACS else color_mode);
   Flags.if_verbose print_header ();
-  init_toploop opts
-
-let coqtop_parse_extra ~opts extras =
-  let rec parse_extra run_mode = function
-  | "-batch" :: rest -> parse_extra Batch rest
+  init_toploop opts async_opts injections
+
+let set_color = function
+  | "yes" | "on" -> `ON
+  | "no" | "off" -> `OFF
+  | "auto" ->`AUTO
+  | _ ->
+    error_wrong_arg ("Error: on/off/auto expected after option color")
+
+let parse_extra_colors extras =
+  let rec parse_extra color_mode = function
+  | "-color" :: next :: rest -> parse_extra (set_color next) rest
+  | "-list-tags" :: rest -> parse_extra color_mode rest
   | x :: rest ->
+    let color_mode, rest = parse_extra color_mode rest in color_mode, x :: rest
+  | [] -> color_mode, [] in
+  parse_extra `AUTO extras
+
+let coqtop_parse_extra extras =
+  let rec parse_extra run_mode  = function
+  | "-batch" :: rest -> parse_extra Batch  rest
+  | "-print-mod-uid" :: rest -> Query (PrintModUid rest), []
+  |   x :: rest ->
     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 color_mode, extras = parse_extra_colors extras in
+  let async_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in
+  ({ run_mode; color_mode}, async_opts), extras
+
+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 coqtop_run run_mode ~opts state =
+let coqtop_run ({ run_mode; color_mode },_) ~opts state =
   match run_mode with
   | Interactive -> Coqloop.loop ~opts ~state;
+  | Query PrintTags -> print_style_tags color_mode; exit 0
+  | Query (PrintModUid sl) ->
+      let s = String.concat " " (List.map get_native_name sl) in
+      print_endline s;
+      exit 0
   | Batch -> exit 0
 
 let coqtop_specific_usage = Usage.{
@@ -317,8 +237,8 @@ coqtop specific options:\n\
 
 let coqtop_toplevel =
   { parse_extra = coqtop_parse_extra
-  ; help = coqtop_specific_usage
-  ; init = coqtop_init
+  ; usage = coqtop_specific_usage
+  ; init_extra = coqtop_init
   ; run = coqtop_run
-  ; opts = Coqargs.default
+  ; initial_args = Coqargs.default
   }
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index e535c19252..c675c6adec 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -9,18 +9,16 @@
 (************************************************************************)
 
 (** Definition of custom toplevels.
-    [init] is used to do custom command line argument parsing.
+    [init_extra] is used to do custom initialization
     [run] launches a custom toplevel.
 *)
 
-type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list
-
 type ('a,'b) custom_toplevel =
-  { parse_extra : 'a extra_args_fn
-  ; help : Usage.specific_usage
-  ; init : 'a -> opts:Coqargs.t -> 'b
+  { parse_extra : string list -> 'a * string list
+  ; usage : Usage.specific_usage
+  ; init_extra : 'a -> Coqargs.injection_command list -> opts:Coqargs.t -> 'b
+  ; initial_args : Coqargs.t
   ; run : 'a -> opts:Coqargs.t -> 'b -> unit
-  ; opts : Coqargs.t
   }
 
 (** The generic Coq main module. [start custom] will parse the command line,
@@ -28,18 +26,28 @@ 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 *)
 
-val init_color : Coqargs.coqargs_config -> unit
+type color = [`ON | `AUTO | `EMACS | `OFF]
+
+val init_color : color -> unit
+val parse_extra_colors : string list -> color * string list
+val print_style_tags : color -> unit
 
 (** Prepare state for interactive loop *)
 
-val init_toploop : Coqargs.t -> Vernac.State.t
+val init_toploop : Coqargs.t -> Stm.AsyncOpts.stm_opt -> Coqargs.injection_command list -> Vernac.State.t
 
 (** The specific characterization of the coqtop_toplevel *)
 
-type run_mode = Interactive | Batch
+type query = PrintTags | PrintModUid of string list
+type run_mode = Interactive | Batch | Query of query
+
+type toplevel_options = {
+  run_mode : run_mode;
+  color_mode : color;
+}
 
-val coqtop_toplevel : (run_mode,Vernac.State.t) custom_toplevel
+val coqtop_toplevel : (toplevel_options * 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..e72940d189 100644
--- a/toplevel/workerLoop.ml
+++ b/toplevel/workerLoop.ml
@@ -8,10 +8,11 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-let worker_parse_extra ~opts extra_args =
-  (), extra_args
+let worker_parse_extra 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 ((),_) _injections ~opts =
   Flags.quiet := true;
   init ();
   Coqtop.init_toploop opts
@@ -27,9 +28,9 @@ let start ~init ~loop name =
   let open Coqtop in
   let custom = {
     parse_extra = worker_parse_extra;
-    help = worker_specific_usage name;
-    opts = Coqargs.default;
-    init = worker_init init;
-    run = (fun () ~opts:_ _state (* why is state not used *) -> loop ());
+    usage = worker_specific_usage name;
+    initial_args = Coqargs.default;
+    init_extra = worker_init init;
+    run = (fun ((),_) ~opts:_ _state (* why is state not used *) -> loop ());
   } in
   start_coq custom