Merge PR #13418: [sysinit] new component

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

46 files changed, 785 insertions, 626 deletions

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index fe7913a3d2..56f48aaa4f 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -228,6 +228,7 @@
 
 /toplevel/   @coq/toplevel-maintainers
 /topbin/     @coq/toplevel-maintainers
+/sysinit/    @coq/toplevel-maintainers
 
 ########## Vernacular ##########
 
diff --git a/META.coq.in b/META.coq.in
index 68ab0733ee..7a9818da08 100644
--- a/META.coq.in
+++ b/META.coq.in
@@ -207,10 +207,10 @@ package "vernac" (
 
 package "stm" (
 
-  description = "Coq State Transactional Machine"
+  description = "Coq State Transaction Machine"
   version     = "8.14"
 
-  requires    = "coq.vernac"
+  requires    = "coq.sysinit"
   directory   = "stm"
 
   archive(byte)    = "stm.cma"
@@ -218,6 +218,19 @@ package "stm" (
 
 )
 
+package "sysinit" (
+
+  description = "Coq initialization"
+  version     = "8.14"
+
+  requires    = "coq.vernac"
+  directory   = "sysinit"
+
+  archive(byte)    = "sysinit.cma"
+  archive(native)  = "sysinit.cmxa"
+
+)
+
 package "toplevel" (
 
   description = "Coq Toplevel"
diff --git a/Makefile.common b/Makefile.common
index 82d9b89c4f..415454df79 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -99,7 +99,7 @@ CORESRCDIRS:=\
   coqpp                                                                                 \
   config 	clib 		lib		kernel		kernel/byterun	library \
   engine 	pretyping	interp	proofs	gramlib/.pack 	parsing 	printing \
-  tactics 	vernac		stm		toplevel
+  tactics 	vernac		stm   sysinit   toplevel
 
 PLUGINDIRS:=\
   omega		micromega \
@@ -132,7 +132,7 @@ CORECMA:=config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma library/l
         engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
 	gramlib/.pack/gramlib.cma \
         parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
-        stm/stm.cma toplevel/toplevel.cma
+        sysinit/sysinit.cma stm/stm.cma toplevel/toplevel.cma
 
 ###########################################################################
 # plugins object files
diff --git a/Makefile.dev b/Makefile.dev
index 5825a884c2..cfb02b6d80 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -91,10 +91,11 @@ interp: interp/interp.cma
 parsing: parsing/parsing.cma
 pretyping: pretyping/pretyping.cma
 stm: stm/stm.cma
+sysinit: sysinit/sysinit.cma
 toplevel: toplevel/toplevel.cma
 
 .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping
-.PHONY: engine stm toplevel
+.PHONY: engine stm sysinit toplevel
 
 ######################
 ### 3) theories files
diff --git a/dev/base_include b/dev/base_include
index daee2d97c5..f375a867bc 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -134,7 +134,6 @@ open ComDefinition
 open Indschemes
 open Ind_tables
 open Auto_ind_decl
-open Coqinit
 open Coqtop
 open Himsg
 open Metasyntax
diff --git a/dev/core.dbg b/dev/core.dbg
index 6d52bae773..dcf9910b0b 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -16,5 +16,6 @@ load_printer parsing.cma
 load_printer printing.cma
 load_printer tactics.cma
 load_printer vernac.cma
+load_printer sysinit.cma
 load_printer stm.cma
 load_printer toplevel.cma
diff --git a/dev/core_dune.dbg b/dev/core_dune.dbg
index 3f73cf126a..da3022644d 100644
--- a/dev/core_dune.dbg
+++ b/dev/core_dune.dbg
@@ -17,5 +17,6 @@ load_printer parsing.cma
 load_printer printing.cma
 load_printer tactics.cma
 load_printer vernac.cma
+load_printer sysinit.cma
 load_printer stm.cma
 load_printer toplevel.cma
diff --git a/dev/dune b/dev/dune
index a6d88c94d2..ae801f9e83 100644
--- a/dev/dune
+++ b/dev/dune
@@ -34,6 +34,7 @@
     %{lib:coq.tactics:tactics.cma}
     %{lib:coq.vernac:vernac.cma}
     %{lib:coq.stm:stm.cma}
+    %{lib:coq.sysinit:sysinit.cma}
     %{lib:coq.toplevel:toplevel.cma}
     %{lib:coq.plugins.ltac:ltac_plugin.cma}
     %{lib:coq.top_printers:top_printers.cmi}
diff --git a/dev/dune_db_408 b/dev/dune_db_408
index 5f826fe383..bc86020d56 100644
--- a/dev/dune_db_408
+++ b/dev/dune_db_408
@@ -17,6 +17,7 @@ load_printer parsing.cma
 load_printer printing.cma
 load_printer tactics.cma
 load_printer vernac.cma
+load_printer sysinit.cma
 load_printer stm.cma
 load_printer toplevel.cma
 
diff --git a/dev/dune_db_409 b/dev/dune_db_409
index 2e58272c75..adb1f76872 100644
--- a/dev/dune_db_409
+++ b/dev/dune_db_409
@@ -16,6 +16,7 @@ load_printer parsing.cma
 load_printer printing.cma
 load_printer tactics.cma
 load_printer vernac.cma
+load_printer sysinit.cma
 load_printer stm.cma
 load_printer toplevel.cma
 
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 534f20f85b..db15d9705a 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -19,7 +19,7 @@ exec $OCAMLDEBUG \
     -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
     -I $COQTOP/gramlib/.pack \
     -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
-    -I $COQTOP/library -I $COQTOP/engine \
+    -I $COQTOP/library -I $COQTOP/engine -I $COQTOP/sysinit \
     -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
     -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
     -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
index 666fb6cc91..a14b98c73c 100755
--- a/dev/tools/update-compat.py
+++ b/dev/tools/update-compat.py
@@ -64,7 +64,7 @@ DEFAULT_NUMBER_OF_OLD_VERSIONS = 2
 RELEASE_NUMBER_OF_OLD_VERSIONS = 2
 MASTER_NUMBER_OF_OLD_VERSIONS = 3
 EXTRA_HEADER = '\n(** Compatibility file for making Coq act similar to Coq v%s *)\n'
-COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml')
+COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'sysinit', 'coqargs.ml')
 DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template')
 TEST_SUITE_RUN_PATH = os.path.join(ROOT_PATH, 'test-suite', 'tools', 'update-compat', 'run.sh')
 TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i)
diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index 528e2a756b..b42c705add 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -513,9 +513,11 @@ let msg_format = ref (fun () ->
 
 (* The loop ignores the command line arguments as the current model delegates
    its handing to the toplevel container. *)
-let loop run_mode ~opts:_ state =
+let loop ( { Coqtop.run_mode; color_mode },_) ~opts:_ state =
   match run_mode with
   | Coqtop.Batch -> exit 0
+  | Coqtop.(Query PrintTags) -> Coqtop.print_style_tags color_mode; exit 0
+  | Coqtop.(Query _) -> Printf.eprintf "Unknown query"; exit 1
   | Coqtop.Interactive ->
   let open Vernac.State in
   set_doc state.doc;
@@ -580,32 +582,28 @@ coqidetop specific options:\n\
 \n  --help-XML-protocol    print documentation of the Coq XML protocol\n"
 }
 
-let islave_parse ~opts extra_args =
+let islave_parse extra_args =
   let open Coqtop in
-  let run_mode, extra_args = coqtop_toplevel.parse_extra ~opts extra_args in
+  let ({ run_mode; color_mode }, stm_opts), extra_args = coqtop_toplevel.parse_extra extra_args in
   let extra_args = parse extra_args in
   (* One of the role of coqidetop is to find the name of buffers to open *)
   (* in the command line; Coqide is waiting these names on stdout *)
   (* (see filter_coq_opts in coq.ml), so we send them now *)
   print_string (String.concat "\n" extra_args);
-  run_mode, []
+  ( { Coqtop.run_mode; color_mode }, stm_opts), []
 
-let islave_init run_mode ~opts =
+let islave_init ( { Coqtop.run_mode; color_mode }, stm_opts) injections ~opts =
   if run_mode = Coqtop.Batch then Flags.quiet := true;
-  Coqtop.init_toploop opts
+  Coqtop.init_toploop opts stm_opts injections
 
-let islave_default_opts =
-  Coqargs.{ default with
-    config = { default.config with
-      stm_flags = { default.config.stm_flags with
-         Stm.AsyncOpts.async_proofs_worker_priority = CoqworkmgrApi.High }}}
+let islave_default_opts = Coqargs.default
 
 let () =
   let open Coqtop in
   let custom = {
       parse_extra = islave_parse ;
-      help = coqidetop_specific_usage;
-      init = islave_init;
+      usage = coqidetop_specific_usage;
+      init_extra = islave_init;
       run = loop;
-      opts = islave_default_opts } in
+      initial_args = islave_default_opts } in
   start_coq custom
diff --git a/lib/stateid.ml b/lib/stateid.ml
index a1328f156c..2a41cb7866 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -45,3 +45,6 @@ type ('a,'b) request = {
   name     : string
 }
 
+let is_valid_ref = ref (fun ~doc:_ (_ : t) -> true)
+let is_valid ~doc id = !is_valid_ref ~doc id
+let set_is_valid f = is_valid_ref := f
diff --git a/lib/stateid.mli b/lib/stateid.mli
index 9b2de9c894..00acc962a2 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -42,3 +42,10 @@ type ('a,'b) request = {
   name     : string
 }
 
+(* Asks the document manager if the given state is valid (or belongs to an
+   old version of the document) *)
+val is_valid : doc:int -> t -> bool
+
+(* By default [is_valid] always answers true, but a document manager supporting
+   undo operations like the STM can override this. *)
+val set_is_valid : (doc:int -> t -> bool) -> unit
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index aa2449d962..937d579012 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -436,11 +436,7 @@ let finish_timing ~prefix name =
 (* ******************** *)
 
 let print_results_filter ~cutoff ~filter =
-  (* The STM doesn't provide yet a proper document query and traversal
-     API, thus we need to re-check if some states are current anymore
-     (due to backtracking) using the `state_of_id` API. *)
-  let valid (did,id) _ = Stm.(state_of_id ~doc:(get_doc did) id) <> `Expired in
-  data := SM.filter valid !data;
+  data := SM.filter (fun (doc,id) _ -> Stateid.is_valid ~doc id) !data;
   let results =
     SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
   let results = merge_roots results Local.(CList.last !stack) in
diff --git a/stm/dune b/stm/dune
index c369bd00fb..27d561334e 100644
--- a/stm/dune
+++ b/stm/dune
@@ -3,4 +3,4 @@
  (synopsis "Coq's Document Manager and Proof Checking Scheduler")
  (public_name coq.stm)
  (wrapped false)
- (libraries vernac))
+ (libraries sysinit))
diff --git a/stm/stm.ml b/stm/stm.ml
index 0b00524bd5..7de109e596 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -297,13 +297,11 @@ end (* }}} *)
 (*************************** THE DOCUMENT *************************************)
 (******************************************************************************)
 
-type interactive_top = TopLogical of DirPath.t | TopPhysical of string
-
 (* The main document type associated to a VCS *)
 type stm_doc_type =
   | VoDoc       of string
   | VioDoc      of string
-  | Interactive of interactive_top
+  | Interactive of Coqargs.top
 
 (* Dummy until we land the functional interp patch + fixed start_library *)
 type doc = int
@@ -517,7 +515,7 @@ end = struct (* {{{ *)
   type vcs = (branch_type, transaction, vcs state_info, box) t
   let vcs : vcs ref = ref (empty Stateid.dummy)
 
-  let doc_type = ref (Interactive (TopLogical (Names.DirPath.make [])))
+  let doc_type = ref (Interactive (Coqargs.TopLogical (Names.DirPath.make [])))
   let ldir = ref Names.DirPath.empty
 
   let init dt id ps =
@@ -801,6 +799,9 @@ let state_of_id ~doc id =
     | EmptyState | ParsingState _ -> `Valid None
   with VCS.Expired -> `Expired
 
+let () =
+  Stateid.set_is_valid (fun ~doc id -> state_of_id ~doc id <> `Expired)
+
 (****** A cache: fills in the nodes of the VCS document with their value ******)
 module State : sig
 
@@ -2305,37 +2306,13 @@ end (* }}} *)
 
 (** STM initialization options: *)
 
-type option_command =
-  | OptionSet of string option
-  | OptionAppend of string
-  | OptionUnset
-
-type injection_command =
-  | OptionInjection of (Goptions.option_name * option_command)
-  (** Set flags or options before the initial state is ready. *)
-  | RequireInjection of (string * string option * bool option)
-  (** Require libraries before the initial state is
-     ready. Parameters follow [Library], that is to say,
-     [lib,prefix,import_export] means require library [lib] from
-     optional [prefix] and [import_export] if [Some false/Some true]
-     is used.  *)
-  (* -load-vernac-source interleaving is not supported yet *)
-  (* | LoadInjection of (string * bool) *)
-
 type stm_init_options =
   { doc_type : stm_doc_type
   (** The STM does set some internal flags differently depending on
      the specified [doc_type]. This distinction should disappear at
      some some point. *)
 
-  ; ml_load_path : CUnix.physical_path list
-  (** OCaml load paths for the document. *)
-
-  ; vo_load_path   : Loadpath.vo_path list
-  (** [vo] load paths for the document. Usually extracted from -R
-     options / _CoqProject *)
-
-  ; injections : injection_command list
+  ; injections : Coqargs.injection_command list
   (** Injects Require and Set/Unset commands before the initial
      state is ready *)
 
@@ -2352,68 +2329,17 @@ let doc_type_module_name (std : stm_doc_type) =
   | Interactive mn -> Names.DirPath.to_string mn
 *)
 
+let init_process stm_flags =
+  Spawned.init_channels ();
+  CoqworkmgrApi.(init stm_flags.AsyncOpts.async_proofs_worker_priority)
+
 let init_core () =
   if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true;
   if !Flags.async_proofs_worker_id = "master" then Partac.enable_par ~nworkers:!cur_opt.async_proofs_n_tacworkers;
   State.register_root_state ()
 
-let dirpath_of_file f =
-  let ldir0 =
-    try
-      let lp = Loadpath.find_load_path (Filename.dirname f) in
-      Loadpath.logical lp
-    with Not_found -> Libnames.default_root_prefix
-  in
-  let f = try Filename.chop_extension (Filename.basename f) with Invalid_argument _ -> f in
-  let id = Id.of_string f in
-  let ldir = Libnames.add_dirpath_suffix ldir0 id in
-  ldir
-
-let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } =
-
-  let require_file (dir, from, exp) =
-    let mp = Libnames.qualid_of_string dir in
-    let mfrom = Option.map Libnames.qualid_of_string from in
-    Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
-
-  let interp_set_option opt v old =
-    let open Goptions in
-    let err expect =
-      let opt = String.concat " " opt in
-      let got = v in (* avoid colliding with Pp.v *)
-      CErrors.user_err
-        Pp.(str "-set: " ++ str opt ++
-            str" expects " ++ str expect ++
-            str" but got " ++ str got)
-    in
-    match old with
-    | BoolValue _ ->
-      let v = match String.trim v with
-        | "true" -> true
-        | "false" | "" -> false
-        | _ -> err "a boolean"
-      in
-      BoolValue v
-    | IntValue _ ->
-      let v = String.trim v in
-      let v = match int_of_string_opt v with
-        | Some _ as v -> v
-        | None -> if v = "" then None else err "an int"
-      in
-      IntValue v
-    | StringValue _ -> StringValue v
-    | StringOptValue _ -> StringOptValue (Some v) in
-
-  let set_option = let open Goptions in function
-      | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt
-      | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true
-      | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v
-      | opt, OptionAppend v -> set_string_option_append_value_gen ~locality:OptLocal opt v in
 
-  let handle_injection = function
-    | RequireInjection r -> require_file r
-    (* | LoadInjection l -> *)
-    | OptionInjection o -> set_option o in
+let new_doc { doc_type ; injections; stm_options } =
 
   (* Set the options from the new documents *)
   AsyncOpts.cur_opt := stm_options;
@@ -2423,37 +2349,27 @@ let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } =
 
   let doc = VCS.init doc_type Stateid.initial (Vernacstate.Parser.init ()) in
 
-  (* Set load path; important, this has to happen before we declare
-     the library below as [Declaremods/Library] will infer the module
-     name by looking at the load path! *)
-  List.iter Mltop.add_ml_dir ml_load_path;
-  List.iter Loadpath.add_vo_path vo_load_path;
-
   Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff;
 
-  begin match doc_type with
-    | Interactive ln ->
-      let dp = match ln with
-        | TopLogical dp -> dp
-        | TopPhysical f -> dirpath_of_file f
-      in
-      Declaremods.start_library dp
+  let top =
+    match doc_type with
+    | Interactive top -> Coqargs.dirpath_of_top top
 
     | VoDoc f ->
-      let ldir = dirpath_of_file f in
-      let () = Flags.verbosely Declaremods.start_library ldir in
+      let ldir = Coqargs.(dirpath_of_top (TopPhysical f)) in
       VCS.set_ldir ldir;
-      set_compilation_hints f
+      set_compilation_hints f;
+      ldir
 
     | VioDoc f ->
-      let ldir = dirpath_of_file f in
-      let () = Flags.verbosely Declaremods.start_library ldir in
+      let ldir = Coqargs.(dirpath_of_top (TopPhysical f)) in
       VCS.set_ldir ldir;
-      set_compilation_hints f
-  end;
+      set_compilation_hints f;
+      ldir
+    in
 
-  (* Import initial libraries. *)
-  List.iter handle_injection injections;
+  (* Start this library and import initial libraries. *)
+  Coqinit.start_library ~top injections;
 
   (* We record the state at this point! *)
   State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial;
diff --git a/stm/stm.mli b/stm/stm.mli
index e0c33a309b..bd42359cea 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -42,32 +42,13 @@ module AsyncOpts : sig
 
 end
 
-type interactive_top = TopLogical of DirPath.t | TopPhysical of string
-
 (** The STM document type [stm_doc_type] determines some properties
    such as what uncompleted proofs are allowed and what gets recorded
    to aux files. *)
 type stm_doc_type =
   | VoDoc       of string       (* file path *)
   | VioDoc      of string       (* file path *)
-  | Interactive of interactive_top    (* module path *)
-
-type option_command =
-  | OptionSet of string option
-  | OptionAppend of string
-  | OptionUnset
-
-type injection_command =
-  | OptionInjection of (Goptions.option_name * option_command)
-  (** Set flags or options before the initial state is ready. *)
-  | RequireInjection of (string * string option * bool option)
-  (** Require libraries before the initial state is
-     ready. Parameters follow [Library], that is to say,
-     [lib,prefix,import_export] means require library [lib] from
-     optional [prefix] and [import_export] if [Some false/Some true]
-     is used.  *)
-  (* -load-vernac-source interleaving is not supported yet *)
-  (* | LoadInjection of (string * bool) *)
+  | Interactive of Coqargs.top    (* module path *)
 
 (** STM initialization options: *)
 type stm_init_options =
@@ -76,14 +57,7 @@ type stm_init_options =
      the specified [doc_type]. This distinction should disappear at
      some some point. *)
 
-  ; ml_load_path : CUnix.physical_path list
-  (** OCaml load paths for the document. *)
-
-  ; vo_load_path   : Loadpath.vo_path list
-  (** [vo] load paths for the document. Usually extracted from -R
-     options / _CoqProject *)
-
-  ; injections : injection_command list
+  ; injections : Coqargs.injection_command list
   (** Injects Require and Set/Unset commands before the initial
      state is ready *)
 
@@ -94,8 +68,10 @@ type stm_init_options =
 (** The type of a STM document *)
 type doc
 
-(** [init_core] performs some low-level initialization; should go away
-   in future releases. *)
+(** [init_process] performs some low-level initialization, call early *)
+val init_process : AsyncOpts.stm_opt -> unit
+
+(** [init_core] snapshorts the initial system state *)
 val init_core : unit -> unit
 
 (** [new_doc opt] Creates a new document with options [opt] *)
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 831369625f..a77e0c79e7 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -3,10 +3,10 @@ Dag
 Vcs
 TQueue
 WorkerPool
-Vernac_classifier
 CoqworkmgrApi
 AsyncTaskQueue
 Partac
 Stm
+Stmargs
 ProofBlockDelimiter
 Vio_checking
diff --git a/stm/stmargs.ml b/stm/stmargs.ml
new file mode 100644
index 0000000000..e2c7649a8f
--- /dev/null
+++ b/stm/stmargs.ml
@@ -0,0 +1,140 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+let fatal_error exn =
+  Topfmt.(in_phase ~phase:ParsingCommandLine print_err_exn exn);
+  let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
+  exit exit_code
+
+let set_worker_id opt s =
+  assert (s <> "master");
+  Flags.async_proofs_worker_id := s
+
+let get_host_port opt s =
+  match String.split_on_char ':' s with
+  | [host; portr; portw] ->
+    Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
+  | ["stdfds"] -> Some Spawned.AnonPipe
+  | _ ->
+    Coqargs.error_wrong_arg ("Error: host:portr:portw or stdfds expected after option "^opt)
+
+let get_error_resilience opt = function
+  | "on" | "all" | "yes" -> `All
+  | "off" | "no" -> `None
+  | s -> `Only (String.split_on_char ',' s)
+
+let get_priority opt s =
+  try CoqworkmgrApi.priority_of_string s
+  with Invalid_argument _ ->
+    Coqargs.error_wrong_arg ("Error: low/high expected after "^opt)
+
+let get_async_proofs_mode opt = let open Stm.AsyncOpts in function
+  | "no" | "off" -> APoff
+  | "yes" | "on" -> APon
+  | "lazy" -> APonLazy
+  | _ ->
+    Coqargs.error_wrong_arg ("Error: on/off/lazy expected after "^opt)
+
+let get_cache opt = function
+  | "force" -> Some Stm.AsyncOpts.Force
+  | _ ->
+    Coqargs.error_wrong_arg ("Error: force expected after "^opt)
+
+let parse_args ~init arglist : Stm.AsyncOpts.stm_opt * string list =
+  let args = ref arglist in
+  let extras = ref [] in
+  let rec parse oval = match !args with
+  | [] ->
+    (oval, List.rev !extras)
+  | opt :: rem ->
+    args := rem;
+    let next () = match !args with
+      | x::rem -> args := rem; x
+      | [] -> Coqargs.error_missing_arg opt
+    in
+    let noval = begin match opt with
+
+    |"-async-proofs" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next())
+      }
+    |"-async-proofs-j" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_n_workers = (Coqargs.get_int ~opt (next ()))
+      }
+    |"-async-proofs-cache" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ())
+      }
+
+    |"-async-proofs-tac-j" ->
+      let j = Coqargs.get_int ~opt (next ()) in
+      if j <= 0 then begin
+        Coqargs.error_wrong_arg ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1")
+      end;
+      { oval with
+        Stm.AsyncOpts.async_proofs_n_tacworkers = j
+      }
+
+    |"-async-proofs-worker-priority" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_worker_priority = get_priority opt (next ())
+      }
+
+    |"-async-proofs-private-flags" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_private_flags = Some (next ());
+      }
+
+    |"-async-proofs-tactic-error-resilience" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ())
+      }
+
+    |"-async-proofs-command-error-resilience" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_cmd_error_resilience = Coqargs.get_bool ~opt (next ())
+      }
+
+    |"-async-proofs-delegation-threshold" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_delegation_threshold = Coqargs.get_float ~opt (next ())
+      }
+
+    |"-worker-id" -> set_worker_id opt (next ()); oval
+
+    |"-main-channel" ->
+      Spawned.main_channel := get_host_port opt (next()); oval
+
+    |"-control-channel" ->
+      Spawned.control_channel := get_host_port opt (next()); oval
+
+    (* Options with zero arg *)
+    |"-async-queries-always-delegate"
+    |"-async-proofs-always-delegate"
+    |"-async-proofs-never-reopen-branch" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_never_reopen_branch = true
+      }
+    |"-stm-debug" -> Stm.stm_debug := true; oval
+    (* Unknown option *)
+    | s ->
+      extras := s :: !extras;
+      oval
+    end in
+    parse noval
+  in
+  try
+    parse init
+  with any -> fatal_error any
+
+let usage = "\
+\n  -stm-debug             STM debug mode (will trace every transaction)\
+"
diff --git a/stm/stmargs.mli b/stm/stmargs.mli
new file mode 100644
index 0000000000..f760afdc98
--- /dev/null
+++ b/stm/stmargs.mli
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val parse_args : init:Stm.AsyncOpts.stm_opt -> string list -> Stm.AsyncOpts.stm_opt * string list
+
+val usage : string
diff --git a/toplevel/coqargs.ml b/sysinit/coqargs.ml
index c114c43e26..c4f12f6bb7 100644
--- a/toplevel/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -24,37 +24,42 @@ let error_missing_arg s =
 (******************************************************************************)
 (* 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 }
+let set_debug () =
+  let () = Exninfo.record_backtrace true in
+  Flags.debug := true
 
 (******************************************************************************)
 
-type color = [`ON | `AUTO | `EMACS | `OFF]
-
 type native_compiler = Coq_config.native_compiler =
   NativeOff | NativeOn of { ondemand : bool }
 
+type top = TopLogical of Names.DirPath.t | TopPhysical of string
+
+type option_command =
+  | OptionSet of string option
+  | OptionUnset
+  | OptionAppend of string
+
+type injection_command =
+  | OptionInjection of (Goptions.option_name * option_command)
+  | RequireInjection of (string * string option * bool option)
+
 type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
   indices_matter    : bool;
-  toplevel_name     : Stm.interactive_top;
+  type_in_type      : bool;
+  toplevel_name     : 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;
@@ -69,13 +74,13 @@ type coqargs_pre = {
   vo_includes : Loadpath.vo_path list;
 
   load_vernacular_list : (string * bool) list;
-  injections  : Stm.injection_command list;
+  injections  : injection_command list;
 
   inputstate  : string option;
 }
 
 type coqargs_query =
-  | PrintTags | PrintWhere | PrintConfig
+  | PrintWhere | PrintConfig
   | PrintVersion | PrintMachineReadableVersion
   | PrintHelp of Usage.specific_usage
 
@@ -85,7 +90,6 @@ type coqargs_main =
 
 type coqargs_post = {
   memory_stat : bool;
-  output_context : bool;
 }
 
 type t = {
@@ -102,19 +106,18 @@ let default_native = Coq_config.native_compiler
 let default_logic_config = {
   impredicative_set = Declarations.PredicativeSet;
   indices_matter = false;
-  toplevel_name = Stm.TopLogical default_toplevel;
+  type_in_type = false;
+  toplevel_name = 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;
@@ -137,7 +140,6 @@ let default_queries = []
 
 let default_post = {
   memory_stat  = false;
-  output_context = false;
 }
 
 let default = {
@@ -160,29 +162,22 @@ let add_vo_include opts unix_path coq_path implicit =
         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 }}
+  { opts with pre = { opts.pre with injections = 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 }}
+  { opts with pre = { opts.pre with injections = 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 opts = add_set_option opts Printer.print_goal_tag_opt_name (OptionSet None) in
+  { opts with config = { opts.config with 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])
@@ -204,61 +199,39 @@ let set_inputstate opts s =
 (******************************************************************************)
 (* Parsing helpers                                                            *)
 (******************************************************************************)
-let get_bool opt = function
+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 =
+let get_int ~opt n =
   try int_of_string n
   with Failure _ ->
     error_wrong_arg ("Error: integer expected after option "^opt)
+let get_int_opt ~opt n =
+  if n = "" then None
+  else Some (get_int ~opt n)
 
-let get_float opt n =
+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 interp_set_option opt v old =
+  let open Goptions in
+  let opt = String.concat " " opt in
+  match old with
+  | BoolValue _ -> BoolValue (get_bool ~opt v)
+  | IntValue _ -> IntValue (get_int_opt ~opt v)
+  | StringValue _ -> StringValue v
+  | StringOptValue _ -> StringOptValue (Some v)
+
+let set_option = let open Goptions in function
+  | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt
+  | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true
+  | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v
+  | opt, OptionAppend v -> set_string_option_append_value_gen ~locality:OptLocal opt v
 
 let get_compat_file = function
   | "8.14" -> "Coq.Compat.Coq814"
@@ -309,7 +282,7 @@ let get_native_compiler s =
 (* Main parsing routine *)
 (*s Parsing of the command line *)
 
-let parse_args ~help ~init arglist : t * string list =
+let parse_args ~usage ~init arglist : t * string list =
   let args = ref arglist in
   let extras = ref [] in
   let rec parse oval = match !args with
@@ -351,55 +324,6 @@ let parse_args ~help ~init arglist : t * string list =
       { 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)
 
@@ -422,16 +346,12 @@ let parse_args ~help ~init arglist : t * string list =
       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
+      let oval = add_set_option oval ["Mangle"; "Names"] (OptionSet None) in
+      add_set_option oval ["Mangle"; "Names"; "Prefix"] (OptionSet(Some(next ())))
 
     |"-profile-ltac-cutoff" ->
       Flags.profile_ltac := true;
-      Flags.profile_ltac_cutoff := get_float opt (next ());
+      Flags.profile_ltac_cutoff := get_float ~opt (next ());
       oval
 
     |"-rfrom" ->
@@ -451,24 +371,18 @@ let parse_args ~help ~init arglist : t * string list =
       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 }}}
+      { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = 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
+      { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = TopPhysical (next()) }}}
 
     |"-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)
+      if w = "none" then add_set_option oval ["Warnings"] (OptionSet(Some w))
+      else add_set_option oval ["Warnings"] (OptionAppend w)
 
     |"-bytecode-compiler" ->
-      { oval with config = { oval.config with enable_VM = get_bool opt (next ()) }}
+      { oval with config = { oval.config with enable_VM = get_bool ~opt (next ()) }}
 
     |"-native-compiler" ->
       let native_compiler = get_native_compiler (next ()) in
@@ -476,10 +390,10 @@ let parse_args ~help ~init arglist : t * string list =
 
     | "-set" ->
       let opt, v = parse_option_set @@ next() in
-      add_set_option oval opt (Stm.OptionSet v)
+      add_set_option oval opt (OptionSet v)
 
     | "-unset" ->
-      add_set_option oval (to_opt_key @@ next ()) Stm.OptionUnset
+      add_set_option oval (to_opt_key @@ next ()) OptionUnset
 
     |"-native-output-dir" ->
       let native_output_dir = next () in
@@ -490,49 +404,39 @@ let parse_args ~help ~init arglist : t * string list =
       { 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
+    |"-debug" -> set_debug (); oval
+    |"-xml-debug" -> Flags.xml_debug := true; set_debug (); oval
     |"-diffs" ->
-      add_set_option oval Proof_diffs.opt_name @@ Stm.OptionSet (Some (next ()))
-    |"-stm-debug" -> Stm.stm_debug := true; oval
+      add_set_option oval Proof_diffs.opt_name @@ OptionSet (Some (next ()))
     |"-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)
+      add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None)
     |"-disallow-sprop" ->
-      add_set_option oval Vernacentries.allow_sprop_opt_name Stm.OptionUnset
+      add_set_option oval Vernacentries.allow_sprop_opt_name OptionUnset
     |"-sprop-cumulative" ->
       warn_deprecated_sprop_cumul();
-      add_set_option oval Vernacentries.cumul_sprop_opt_name (Stm.OptionSet None)
+      add_set_option oval Vernacentries.cumul_sprop_opt_name (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 }}
+    |"-m"|"--memory" -> { oval with post = { 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
+    |"-type-in-type" -> set_logic (fun o -> { o with type_in_type = true }) 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)
+    |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp usage)
     |"-v"|"--version" -> set_query oval PrintVersion
     |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion
 
@@ -548,8 +452,8 @@ let parse_args ~help ~init arglist : t * string list =
   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 parse_args ~usage ~init args =
+  let opts, extra = parse_args ~usage ~init args in
   let opts =
     { opts with
       pre = { opts.pre with
@@ -568,13 +472,29 @@ let parse_args ~help ~init args =
 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
+  if opts.pre.load_init then 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
+      Coqloadpath.init_load_path ~coqlib in
   ml_path @ opts.pre.ml_includes ,
   vo_path @ opts.pre.vo_includes
+
+let dirpath_of_file f =
+  let ldir0 =
+    try
+      let lp = Loadpath.find_load_path (Filename.dirname f) in
+      Loadpath.logical lp
+    with Not_found -> Libnames.default_root_prefix
+  in
+  let f = try Filename.chop_extension (Filename.basename f) with Invalid_argument _ -> f in
+  let id = Names.Id.of_string f in
+  let ldir = Libnames.add_dirpath_suffix ldir0 id in
+  ldir
+
+let dirpath_of_top = function
+  | TopPhysical f -> dirpath_of_file f
+  | TopLogical dp -> dp
diff --git a/toplevel/coqargs.mli b/sysinit/coqargs.mli
index f6222e4ec4..aef50193f2 100644
--- a/toplevel/coqargs.mli
+++ b/sysinit/coqargs.mli
@@ -8,29 +8,43 @@
 (*         *     (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 top = TopLogical of Names.DirPath.t | TopPhysical of string
+
+type option_command =
+  | OptionSet of string option
+  | OptionUnset
+  | OptionAppend of string
+
+type injection_command =
+  | OptionInjection of (Goptions.option_name * option_command)
+  (** Set flags or options before the initial state is ready. *)
+  | RequireInjection of (string * string option * bool option)
+  (** Require libraries before the initial state is
+     ready. Parameters follow [Library], that is to say,
+     [lib,prefix,import_export] means require library [lib] from
+     optional [prefix] and [import_export] if [Some false/Some true]
+     is used.  *)
+
 type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
   indices_matter    : bool;
-  toplevel_name     : Stm.interactive_top;
+  type_in_type      : bool;
+  toplevel_name     : 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;
@@ -45,13 +59,13 @@ type coqargs_pre = {
   vo_includes : Loadpath.vo_path list;
 
   load_vernacular_list : (string * bool) list;
-  injections  : Stm.injection_command list;
+  injections  : injection_command list;
 
   inputstate  : string option;
 }
 
 type coqargs_query =
-  | PrintTags | PrintWhere | PrintConfig
+  | PrintWhere | PrintConfig
   | PrintVersion | PrintMachineReadableVersion
   | PrintHelp of Usage.specific_usage
 
@@ -61,7 +75,6 @@ type coqargs_main =
 
 type coqargs_post = {
   memory_stat : bool;
-  output_context : bool;
 }
 
 type t = {
@@ -74,8 +87,20 @@ type t = {
 (* 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 parse_args : usage:Usage.specific_usage -> init:t -> string list -> t * string list
 
-val injection_commands : t -> Stm.injection_command list
+val injection_commands : t -> injection_command list
 val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list
+
+val dirpath_of_top : top -> Names.DirPath.t
+
+(* Common utilities *)
+
+val get_int : opt:string -> string -> int
+val get_int_opt : opt:string -> string -> int option
+val get_bool : opt:string -> string -> bool
+val get_float : opt:string -> string -> float
+val error_missing_arg : string -> 'a
+val error_wrong_arg : string -> 'a
+
+val set_option : Goptions.option_name * option_command -> unit
diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml
new file mode 100644
index 0000000000..16c8389de5
--- /dev/null
+++ b/sysinit/coqinit.ml
@@ -0,0 +1,136 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(** 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_ocaml () =
+  CProfile.init_profile ();
+  init_gc ();
+  Sys.catch_break false (* Ctrl-C is fatal during the initialisation *)
+
+let init_coqlib opts = match opts.Coqargs.config.Coqargs.coqlib with
+  | None when opts.Coqargs.pre.Coqargs.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 = let open Coqargs in 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
+
+let parse_arguments ~parse_extra ~usage ?(initial_args=Coqargs.default) () =
+  let opts, extras =
+    Coqargs.parse_args ~usage ~init:initial_args
+      (List.tl (Array.to_list Sys.argv)) in
+  let customopts, extras = parse_extra 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;
+  match opts.Coqargs.main with
+  | Coqargs.Queries q -> List.iter (print_query opts) q; exit 0
+  | Coqargs.Run -> opts, customopts
+
+let print_memory_stat () =
+  let open Pp in
+  (* -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 _ -> ()
+
+let init_runtime opts =
+  let open Coqargs in
+  Lib.init ();
+  init_coqlib opts;
+  if opts.post.memory_stat then at_exit print_memory_stat;
+  Mltop.init_known_plugins ();
+
+  (* Configuration *)
+  Global.set_engagement opts.config.logic.impredicative_set;
+  Global.set_indices_matter opts.config.logic.indices_matter;
+  Global.set_check_universes (not opts.config.logic.type_in_type);
+  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;
+
+  (* Paths for loading stuff *)
+  let ml_load_path, vo_load_path = Coqargs.build_load_path opts in
+  List.iter Mltop.add_ml_dir ml_load_path;
+  List.iter Loadpath.add_vo_path vo_load_path;
+
+  injection_commands opts
+
+let require_file (dir, from, exp) =
+  let mp = Libnames.qualid_of_string dir in
+  let mfrom = Option.map Libnames.qualid_of_string from in
+  Flags.silently (Vernacentries.vernac_require mfrom exp) [mp]
+
+let handle_injection = function
+  | Coqargs.RequireInjection r -> require_file r
+  (* | LoadInjection l -> *)
+  | Coqargs.OptionInjection o -> Coqargs.set_option o
+
+let start_library ~top injections =
+  Flags.verbosely Declaremods.start_library top;
+  List.iter handle_injection injections
diff --git a/sysinit/coqinit.mli b/sysinit/coqinit.mli
new file mode 100644
index 0000000000..bea2186d81
--- /dev/null
+++ b/sysinit/coqinit.mli
@@ -0,0 +1,58 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(** Main etry point to the sysinit component, all other modules are private.
+
+    The following API shoud be called in order, and the first 3 steps only once
+    since they initialize global data. On the contrary step 4 can be called
+    many times to init the compilation of a unit.
+*)
+
+(** 1 initialization of OCaml's runtime
+
+    Profiling, GC parameters and signals. Nothing specific to Coq per se, but
+    the defaults here are good for Coq.
+    This API should be called up very early, or not at all. *)
+val init_ocaml : unit -> unit
+
+(** 2 parsing of Sys.argv
+
+    This API parses command line options which are known by Coq components.
+    Ideally it is functional, but some values in the `Flags` modules are set
+    on the spot instead of being represented as "injection commands" (a field
+    of Coqargs.t).
+
+    [parse_extra] and [usage] can be used to parse/document more options. *)
+val parse_arguments :
+  parse_extra:(string list -> 'a * string list) ->
+  usage:Usage.specific_usage ->
+  ?initial_args:Coqargs.t ->
+  unit ->
+  Coqargs.t * 'a
+
+(** 3 initialization of global runtime data
+
+    All global setup is done here, like COQLIB and the paths for native
+    compilation. If Coq is used to process multiple libraries, what is set up
+    here is really global and common to all of them.
+
+    The returned injections are options (as in "Set This Thing" or "Require
+    that") as specified on the command line.
+    The prelude is one of these (unless "-nois" is passed).
+
+    This API must be called, typically jsut after parsing arguments. *)
+val init_runtime : Coqargs.t -> Coqargs.injection_command list
+
+(** 4 Start a library (sets options and loads objects like the prelude)
+
+    Given the logical name [top] of the current library and the set of initial
+    options and required libraries, it starts its processing (see also
+    Declaremods.start_library) *)
+val start_library : top:Names.DirPath.t -> Coqargs.injection_command list -> unit
diff --git a/toplevel/coqinit.ml b/sysinit/coqloadpath.ml
index 501047c520..8635345e00 100644
--- a/toplevel/coqinit.ml
+++ b/sysinit/coqloadpath.ml
@@ -13,44 +13,6 @@ 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
@@ -73,7 +35,7 @@ let build_userlib_path ~unix_path =
   else [], []
 
 (* LoadPath for Coq user libraries *)
-let libs_init_load_path ~coqlib =
+let init_load_path ~coqlib =
 
   let open Loadpath in
   let user_contrib = coqlib/"user-contrib" in
diff --git a/toplevel/coqinit.mli b/sysinit/coqloadpath.mli
index b96a0ef162..d853e9ea54 100644
--- a/toplevel/coqinit.mli
+++ b/sysinit/coqloadpath.mli
@@ -8,15 +8,9 @@
 (*         *     (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
+val init_load_path
   : coqlib:CUnix.physical_path
   -> CUnix.physical_path list * Loadpath.vo_path list
diff --git a/sysinit/dune b/sysinit/dune
new file mode 100644
index 0000000000..04b46fb2a2
--- /dev/null
+++ b/sysinit/dune
@@ -0,0 +1,7 @@
+(library
+ (name sysinit)
+ (public_name coq.sysinit)
+ (synopsis "Coq's initialization")
+ (wrapped false)
+ (libraries coq.vernac)
+ )
diff --git a/sysinit/sysinit.mllib b/sysinit/sysinit.mllib
new file mode 100644
index 0000000000..6e86536648
--- /dev/null
+++ b/sysinit/sysinit.mllib
@@ -0,0 +1,4 @@
+Usage
+Coqloadpath
+Coqargs
+Coqinit
diff --git a/toplevel/usage.ml b/sysinit/usage.ml
index 6fb5f821ee..1831a3f9b2 100644
--- a/toplevel/usage.ml
+++ b/sysinit/usage.ml
@@ -74,7 +74,6 @@ let print_usage_common co command =
 \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\
diff --git a/toplevel/usage.mli b/sysinit/usage.mli
index cbc3b4f7e8..2d1a8e94cc 100644
--- a/toplevel/usage.mli
+++ b/sysinit/usage.mli
@@ -26,4 +26,3 @@ type specific_usage = {
        given executable. } *)
 
 val print_usage : out_channel -> specific_usage -> unit
-
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/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/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/coqrc.mli b/toplevel/coqrc.mli
new file mode 100644
index 0000000000..3b8a31b2a5
--- /dev/null
+++ b/toplevel/coqrc.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State.t
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/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
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index cd0dd5e9a6..007a3b05fc 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -45,3 +45,4 @@ ComArguments
 Vernacentries
 ComTactic
 Vernacinterp
+Vernac_classifier
diff --git a/stm/vernac_classifier.ml b/vernac/vernac_classifier.ml
index ffae2866c0..ffae2866c0 100644
--- a/stm/vernac_classifier.ml
+++ b/vernac/vernac_classifier.ml
diff --git a/stm/vernac_classifier.mli b/vernac/vernac_classifier.mli
index 61bf3a503a..61bf3a503a 100644
--- a/stm/vernac_classifier.mli
+++ b/vernac/vernac_classifier.mli