[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.

6 files changed, 130 insertions, 225 deletions

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