[sysinit] move initialization code from coqtop to here

We also spill (some) non-generic arguments and initialization code
out of coqargs and to coqtop, namely colors for the terminal. There are
more of these, left to later commits.

16 files changed, 380 insertions, 323 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/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index ed0eb8f34b..2941497c12 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -513,9 +513,10 @@ 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.Interactive ->
   let open Vernac.State in
   set_doc state.doc;
@@ -580,19 +581,19 @@ 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, stm_opts), 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, stm_opts), []
+  ( { Coqtop.run_mode; color_mode }, stm_opts), []
 
-let islave_init (run_mode, stm_opts) ~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 stm_opts
+  Coqtop.init_toploop opts stm_opts injections
 
 let islave_default_opts = Coqargs.default
 
@@ -600,8 +601,8 @@ 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/stm/stm.ml b/stm/stm.ml
index f4e370e7bc..7de109e596 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -301,7 +301,7 @@ end (* }}} *)
 type stm_doc_type =
   | VoDoc       of string
   | VioDoc      of string
-  | Interactive of Coqargs.interactive_top
+  | Interactive of Coqargs.top
 
 (* Dummy until we land the functional interp patch + fixed start_library *)
 type doc = int
@@ -2312,13 +2312,6 @@ 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 : Coqargs.injection_command list
   (** Injects Require and Set/Unset commands before the initial
      state is ready *)
@@ -2345,29 +2338,8 @@ let init_core () =
   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 handle_injection = function
-    | Coqargs.RequireInjection r -> require_file r
-    (* | LoadInjection l -> *)
-    | Coqargs.OptionInjection o -> Coqargs.set_option o in
+let new_doc { doc_type ; injections; stm_options } =
 
   (* Set the options from the new documents *)
   AsyncOpts.cur_opt := stm_options;
@@ -2377,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
-        | Coqargs.TopLogical dp -> dp
-        | Coqargs.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 dddd63cb52..bd42359cea 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -48,7 +48,7 @@ end
 type stm_doc_type =
   | VoDoc       of string       (* file path *)
   | VioDoc      of string       (* file path *)
-  | Interactive of Coqargs.interactive_top    (* module path *)
+  | Interactive of Coqargs.top    (* module path *)
 
 (** STM initialization options: *)
 type stm_init_options =
@@ -57,13 +57,6 @@ 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 : Coqargs.injection_command list
   (** Injects Require and Set/Unset commands before the initial
      state is ready *)
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index 930c3b135f..32025ac434 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -35,12 +35,10 @@ let set_debug () =
 
 (******************************************************************************)
 
-type color = [`ON | `AUTO | `EMACS | `OFF]
-
 type native_compiler = Coq_config.native_compiler =
   NativeOff | NativeOn of { ondemand : bool }
 
-type interactive_top = TopLogical of Names.DirPath.t | TopPhysical of string
+type top = TopLogical of Names.DirPath.t | TopPhysical of string
 
 type option_command =
   | OptionSet of string option
@@ -54,14 +52,13 @@ type injection_command =
 type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
   indices_matter    : bool;
-  toplevel_name     : interactive_top;
+  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;
@@ -86,7 +83,7 @@ type coqargs_pre = {
 }
 
 type coqargs_query =
-  | PrintTags | PrintWhere | PrintConfig
+  | PrintWhere | PrintConfig
   | PrintVersion | PrintMachineReadableVersion
   | PrintHelp of Usage.specific_usage
 
@@ -120,7 +117,6 @@ 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";
@@ -181,18 +177,11 @@ let add_set_option opts opt_name value =
 (** 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 }}
+  { 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])
@@ -306,7 +295,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
@@ -435,7 +424,6 @@ let parse_args ~help ~init arglist : t * string list =
     |"-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" -> set_debug (); oval
     |"-xml-debug" -> Flags.xml_debug := true; set_debug (); oval
@@ -462,12 +450,11 @@ let parse_args ~help ~init arglist : t * string list =
       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)
+    |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp usage)
     |"-v"|"--version" -> set_query oval PrintVersion
     |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion
 
@@ -483,8 +470,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
@@ -513,3 +500,19 @@ let build_load_path opts =
       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/sysinit/coqargs.mli b/sysinit/coqargs.mli
index 894e0f2ef3..ebf367270d 100644
--- a/sysinit/coqargs.mli
+++ b/sysinit/coqargs.mli
@@ -8,14 +8,12 @@
 (*         *     (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 interactive_top = TopLogical of Names.DirPath.t | TopPhysical of string
+type top = TopLogical of Names.DirPath.t | TopPhysical of string
 
 type option_command =
   | OptionSet of string option
@@ -35,14 +33,13 @@ type injection_command =
 type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
   indices_matter    : bool;
-  toplevel_name     : interactive_top;
+  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;
@@ -67,7 +64,7 @@ type coqargs_pre = {
 }
 
 type coqargs_query =
-  | PrintTags | PrintWhere | PrintConfig
+  | PrintWhere | PrintConfig
   | PrintVersion | PrintMachineReadableVersion
   | PrintHelp of Usage.specific_usage
 
@@ -90,11 +87,13 @@ type t = {
 (* Default options *)
 val default : t
 
-val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * string list
+val parse_args : usage:Usage.specific_usage -> init:t -> string list -> t * string 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
diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml
new file mode 100644
index 0000000000..cbecc52827
--- /dev/null
+++ b/sysinit/coqinit.ml
@@ -0,0 +1,135 @@
+(************************************************************************)
+(*         *   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_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/sysinit/dune b/sysinit/dune
index 6146aa60d0..04b46fb2a2 100644
--- a/sysinit/dune
+++ b/sysinit/dune
@@ -4,5 +4,4 @@
  (synopsis "Coq's initialization")
  (wrapped false)
  (libraries coq.vernac)
- (modules coqloadpath coqargs usage)
  )
diff --git a/sysinit/sysinit.mllib b/sysinit/sysinit.mllib
index 9d35a931bc..715de2bb82 100644
--- a/sysinit/sysinit.mllib
+++ b/sysinit/sysinit.mllib
@@ -1,3 +1,4 @@
 Usage
 Coqloadpath
 Coqargs
+Coqinit
\ No newline at end of file
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 4747abceb5..ca09bad441 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -93,7 +93,7 @@ let create_empty_file filename =
   close_out f
 
 (* Compile a vernac file *)
-let compile opts stm_options 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,8 +104,6 @@ let compile opts stm_options 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 output_native_objects = match opts.config.native_compiler with
     | NativeOff -> false | NativeOn {ondemand} -> not ondemand
   in
@@ -128,9 +126,7 @@ let compile opts stm_options 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
@@ -180,8 +176,7 @@ let compile opts stm_options 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
@@ -208,22 +203,22 @@ let compile opts stm_options copts ~echo ~f_in ~f_out =
       dump_empty_vos();
       create_empty_file (long_f_dot_out ^ "k")
 
-let compile opts stm_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 stm_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 stm_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 stm_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 stm_opts copts ~echo ~f_in ~f_out
+    compile opts stm_opts copts injections ~echo ~f_in ~f_out
 
-let compile_files (opts, stm_opts) copts =
+let compile_files (opts, stm_opts) copts injections =
   let compile_list = copts.compile_list in
-  List.iter (compile_file opts stm_opts copts) compile_list
+  List.iter (compile_file opts stm_opts copts injections) compile_list
 
 (******************************************************************************)
 (* VIO Dispatching                                                            *)
@@ -247,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 1b670a8edc..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 * Stm.AsyncOpts.stm_opt -> 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 0c23c9f4e9..a896541573 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,14 +42,14 @@ coqc specific options:\
 \n"
 }
 
-let coqc_main (copts,stm_opts) ~opts =
+let coqc_main ((copts,_),stm_opts) injections ~opts =
   Topfmt.(in_phase ~phase:CompilationPhase)
-    Ccompile.compile_files (opts,stm_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;
@@ -61,10 +62,10 @@ let coqc_main (copts,stm_opts) ~opts =
   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,15 +74,16 @@ let coqc_run copts ~opts () =
     let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
     exit exit_code
 
-let custom_coqc : (Coqcargs.t * Stm.AsyncOpts.stm_opt, 'b) Coqtop.custom_toplevel
+let custom_coqc : ((Coqcargs.t * Coqtop.color) * Stm.AsyncOpts.stm_opt, 'b) Coqtop.custom_toplevel
  = Coqtop.{
-  parse_extra = (fun ~opts extras ->
+  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
-    (Coqcargs.parse extras, stm_opts), []);
-  help = coqc_specific_usage;
-  init = coqc_init;
+    ((Coqcargs.parse extras, 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/coqtop.ml b/toplevel/coqtop.ml
index 7596df788b..714af6f51a 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,128 +143,14 @@ 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 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_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;
-
-  (* Allow the user to load an arbitrary state here *)
-  inputstate opts.pre;
+type run_mode = Interactive | Batch | Query_PrintTags
 
-  (* 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
-    Stm.init_process (snd customopts);
-    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 stm_options =
+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
@@ -250,57 +159,56 @@ let init_document opts stm_options =
   *)
   (* 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 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 stm_opts =
-  let state = init_document opts stm_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,stm_opts) ~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 stm_opts
+  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 ~opts extras =
-  let rec parse_extra run_mode = function
-  | "-batch" :: rest -> parse_extra Batch rest
+let coqtop_parse_extra extras =
+  let rec parse_extra run_mode  = function
+  | "-batch" :: rest -> parse_extra Batch  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
-  let stm_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in
-  (run_mode, stm_opts), 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 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
   | Batch -> exit 0
 
 let coqtop_specific_usage = Usage.{
@@ -314,8 +222,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 9ae0d86cf1..f51df102bd 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,
@@ -32,14 +30,23 @@ 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 -> Stm.AsyncOpts.stm_opt -> 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 run_mode = Interactive | Batch | Query_PrintTags
+
+type toplevel_options = {
+  run_mode : run_mode;
+  color_mode : color;
+}
 
-val coqtop_toplevel : (run_mode * Stm.AsyncOpts.stm_opt,Vernac.State.t) custom_toplevel
+val coqtop_toplevel : (toplevel_options * Stm.AsyncOpts.stm_opt,Vernac.State.t) custom_toplevel
diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml
index b0d7bb6f78..e72940d189 100644
--- a/toplevel/workerLoop.ml
+++ b/toplevel/workerLoop.ml
@@ -8,11 +8,11 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-let worker_parse_extra ~opts 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
@@ -28,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;
+    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