From 4264aec518d5407f345c58e18e014e15e9ae96af Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 5 Jan 2021 11:34:35 +0100
Subject: [sysinit] new component for system initialization

This component holds the code for initializing Coq:
- parsing arguments not specific to the toplevel
- initializing all components from vernac downwards (no stm)

This commit moves stm specific arguments parsing to stm/stmargs.ml
---
 sysinit/coqargs.ml      | 515 ++++++++++++++++++++++++++++++++++++++++++++++++
 sysinit/coqargs.mli     | 107 ++++++++++
 sysinit/coqloadpath.ml  |  73 +++++++
 sysinit/coqloadpath.mli |  16 ++
 sysinit/dune            |   8 +
 sysinit/sysinit.mllib   |   3 +
 sysinit/usage.ml        | 112 +++++++++++
 sysinit/usage.mli       |  28 +++
 8 files changed, 862 insertions(+)
 create mode 100644 sysinit/coqargs.ml
 create mode 100644 sysinit/coqargs.mli
 create mode 100644 sysinit/coqloadpath.ml
 create mode 100644 sysinit/coqloadpath.mli
 create mode 100644 sysinit/dune
 create mode 100644 sysinit/sysinit.mllib
 create mode 100644 sysinit/usage.ml
 create mode 100644 sysinit/usage.mli

(limited to 'sysinit')

diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
new file mode 100644
index 0000000000..930c3b135f
--- /dev/null
+++ b/sysinit/coqargs.ml
@@ -0,0 +1,515 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+let fatal_error exn =
+  Topfmt.(in_phase ~phase:ParsingCommandLine print_err_exn exn);
+  let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
+  exit exit_code
+
+let error_wrong_arg msg =
+  prerr_endline msg; exit 1
+
+let error_missing_arg s =
+  prerr_endline ("Error: extra argument expected after option "^s);
+  prerr_endline "See -help for the syntax of supported options";
+  exit 1
+
+(******************************************************************************)
+(* Imperative effects! This must be fixed at some point.                      *)
+(******************************************************************************)
+
+let set_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 interactive_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     : interactive_top;
+}
+
+type coqargs_config = {
+  logic       : coqargs_logic_config;
+  rcfile      : string option;
+  coqlib      : string option;
+  color       : color;
+  enable_VM   : bool;
+  native_compiler : native_compiler;
+  native_output_dir : CUnix.physical_path;
+  native_include_dirs : CUnix.physical_path list;
+  debug       : bool;
+  time        : bool;
+  print_emacs : bool;
+}
+
+type coqargs_pre = {
+  boot        : bool;
+  load_init   : bool;
+  load_rcfile : bool;
+
+  ml_includes : string list;
+  vo_includes : Loadpath.vo_path list;
+
+  load_vernacular_list : (string * bool) list;
+  injections  : injection_command list;
+
+  inputstate  : string option;
+}
+
+type coqargs_query =
+  | PrintTags | PrintWhere | PrintConfig
+  | PrintVersion | PrintMachineReadableVersion
+  | PrintHelp of Usage.specific_usage
+
+type coqargs_main =
+  | Queries of coqargs_query list
+  | Run
+
+type coqargs_post = {
+  memory_stat : bool;
+  output_context : bool;
+}
+
+type t = {
+  config : coqargs_config;
+  pre : coqargs_pre;
+  main : coqargs_main;
+  post : coqargs_post;
+}
+
+let default_toplevel = Names.(DirPath.make [Id.of_string "Top"])
+
+let default_native = Coq_config.native_compiler
+
+let default_logic_config = {
+  impredicative_set = Declarations.PredicativeSet;
+  indices_matter = false;
+  toplevel_name = 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 = [];
+  debug        = false;
+  time         = false;
+  print_emacs  = false;
+
+  (* Quiet / verbosity options should be here *)
+}
+
+let default_pre = {
+  boot         = false;
+  load_init    = true;
+  load_rcfile  = true;
+  ml_includes  = [];
+  vo_includes  = [];
+  load_vernacular_list = [];
+  injections   = [];
+  inputstate   = None;
+}
+
+let default_queries = []
+
+let default_post = {
+  memory_stat  = false;
+  output_context = false;
+}
+
+let default = {
+  config = default_config;
+  pre    = default_pre;
+  main   = Run;
+  post   = default_post;
+}
+
+(******************************************************************************)
+(* Functional arguments                                                       *)
+(******************************************************************************)
+let add_ml_include opts s =
+  { opts with pre = { opts.pre with ml_includes = s :: opts.pre.ml_includes }}
+
+let add_vo_include opts unix_path coq_path implicit =
+  let open Loadpath in
+  let coq_path = Libnames.dirpath_of_string coq_path in
+  { opts with pre = { opts.pre with vo_includes = {
+        unix_path; coq_path; has_ml = false; implicit; recursive = true } :: opts.pre.vo_includes }}
+
+let add_vo_require opts d p export =
+  { opts with pre = { opts.pre with injections = 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 = OptionInjection (opt_name, value) :: opts.pre.injections }}
+
+(** Options for proof general *)
+let set_emacs opts =
+  Goptions.set_bool_option_value Printer.print_goal_tag_opt_name true;
+  { opts with config = { opts.config with color = `EMACS; print_emacs = true }}
+
+let set_logic f oval =
+  { oval with config = { oval.config with logic = f oval.config.logic }}
+
+let set_color opts = function
+  | "yes" | "on" -> { opts with config = { opts.config with color = `ON }}
+  | "no" | "off" -> { opts with config = { opts.config with color = `OFF }}
+  | "auto" -> { opts with config = { opts.config with color = `AUTO }}
+  | _ ->
+    error_wrong_arg ("Error: on/off/auto expected after option color")
+
+let set_query opts q =
+  { opts with main = match opts.main with
+  | Run -> Queries (default_queries@[q])
+  | Queries queries -> Queries (queries@[q])
+  }
+
+let warn_deprecated_sprop_cumul =
+  CWarnings.create ~name:"deprecated-spropcumul" ~category:"deprecated"
+         (fun () -> Pp.strbrk "Use the \"Cumulative StrictProp\" flag instead.")
+
+let warn_deprecated_inputstate =
+  CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
+         (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.")
+
+let set_inputstate opts s =
+  warn_deprecated_inputstate ();
+  { opts with pre = { opts.pre with inputstate = Some s }}
+
+(******************************************************************************)
+(* Parsing helpers                                                            *)
+(******************************************************************************)
+let get_bool ~opt = function
+  | "yes" | "on" -> true
+  | "no" | "off" -> false
+  | _ ->
+    error_wrong_arg ("Error: yes/no expected after option "^opt)
+
+let get_int ~opt n =
+  try int_of_string n
+  with Failure _ ->
+    error_wrong_arg ("Error: integer expected after option "^opt)
+let get_int_opt ~opt n =
+  if n = "" then None
+  else Some (get_int ~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_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"
+  | "8.13" -> "Coq.Compat.Coq813"
+  | "8.12" -> "Coq.Compat.Coq812"
+  | "8.11" -> "Coq.Compat.Coq811"
+  | ("8.10" | "8.9" | "8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
+    CErrors.user_err ~hdr:"get_compat_file"
+      Pp.(str "Compatibility with version " ++ str s ++ str " not supported.")
+  | s ->
+    CErrors.user_err ~hdr:"get_compat_file"
+      Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".")
+
+let to_opt_key = Str.(split (regexp " +"))
+
+let parse_option_set opt =
+  match String.index_opt opt '=' with
+  | None -> to_opt_key opt, None
+  | Some eqi ->
+    let len = String.length opt in
+    let v = String.sub opt (eqi+1) (len - eqi - 1) in
+    to_opt_key (String.sub opt 0 eqi), Some v
+
+let warn_no_native_compiler =
+  CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler"
+    Pp.(fun s -> strbrk "Native compiler is disabled," ++
+                   strbrk " -native-compiler " ++ strbrk s ++
+                   strbrk " option ignored.")
+
+let get_native_compiler s =
+  (* We use two boolean flags because the four states make sense, even if
+  only three are accessible to the user at the moment. The selection of the
+  produced artifact(s) (`.vo`, `.vio`, `.coq-native`, ...) should be done by
+  a separate flag, and the "ondemand" value removed. Once this is done, use
+  [get_bool] here. *)
+  let n = match s with
+    | ("yes" | "on") -> NativeOn {ondemand=false}
+    | "ondemand" -> NativeOn {ondemand=true}
+    | ("no" | "off") -> NativeOff
+    | _ ->
+       error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") in
+  if Coq_config.native_compiler = NativeOff && n <> NativeOff then
+    let () = warn_no_native_compiler s in
+    NativeOff
+  else
+    n
+
+(* Main parsing routine *)
+(*s Parsing of the command line *)
+
+let parse_args ~help ~init arglist : t * string list =
+  let args = ref arglist in
+  let extras = ref [] in
+  let rec parse oval = match !args with
+  | [] ->
+    (oval, List.rev !extras)
+  | opt :: rem ->
+    args := rem;
+    let next () = match !args with
+      | x::rem -> args := rem; x
+      | [] -> error_missing_arg opt
+    in
+    let noval = begin match opt with
+
+    (* Complex options with many args *)
+    |"-I"|"-include" ->
+      begin match rem with
+      | d :: rem ->
+        args := rem;
+        add_ml_include oval d
+      | [] -> error_missing_arg opt
+      end
+    |"-Q" ->
+      begin match rem with
+      | d :: p :: rem ->
+        args := rem;
+        add_vo_include oval d p false
+      | _ -> error_missing_arg opt
+      end
+    |"-R" ->
+      begin match rem with
+      | d :: p :: rem ->
+        args := rem;
+        add_vo_include oval d p true
+      | _ -> error_missing_arg opt
+      end
+
+    (* Options with one arg *)
+    |"-coqlib" ->
+      { oval with config = { oval.config with coqlib = Some (next ())
+      }}
+
+    |"-compat" ->
+      add_vo_require oval (get_compat_file (next ())) None (Some false)
+
+    |"-exclude-dir" ->
+      System.exclude_directory (next ()); oval
+
+    |"-init-file" ->
+      { oval with config = { oval.config with rcfile = Some (next ()); }}
+
+    |"-inputstate"|"-is" ->
+      set_inputstate oval (next ())
+
+    |"-load-vernac-object" ->
+      add_vo_require oval (next ()) None None
+
+    |"-load-vernac-source"|"-l" ->
+      add_load_vernacular oval false (next ())
+
+    |"-load-vernac-source-verbose"|"-lv" ->
+      add_load_vernacular oval true (next ())
+
+    |"-mangle-names" ->
+      Goptions.set_bool_option_value ["Mangle"; "Names"] true;
+      Goptions.set_string_option_value ["Mangle"; "Names"; "Prefix"] (next ());
+      oval
+
+    |"-print-mod-uid" ->
+      let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0
+
+    |"-profile-ltac-cutoff" ->
+      Flags.profile_ltac := true;
+      Flags.profile_ltac_cutoff := get_float ~opt (next ());
+      oval
+
+    |"-rfrom" ->
+      let from = next () in add_vo_require oval (next ()) (Some from) None
+
+    |"-require-import" | "-ri" -> add_vo_require oval (next ()) None (Some false)
+
+    |"-require-export" | "-re" -> add_vo_require oval (next ()) None (Some true)
+
+    |"-require-import-from" | "-rifrom" ->
+      let from = next () in add_vo_require oval (next ()) (Some from) (Some false)
+
+    |"-require-export-from" | "-refrom" ->
+      let from = next () in add_vo_require oval (next ()) (Some from) (Some true)
+
+    |"-top" ->
+      let topname = Libnames.dirpath_of_string (next ()) in
+      if Names.DirPath.is_empty topname then
+        CErrors.user_err Pp.(str "Need a non empty toplevel module name");
+      { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = TopLogical topname }}}
+
+    |"-topfile" ->
+      { 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"] (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 ()) }}
+
+    |"-native-compiler" ->
+      let native_compiler = get_native_compiler (next ()) in
+      { oval with config = { oval.config with native_compiler }}
+
+    | "-set" ->
+      let opt, v = parse_option_set @@ next() in
+      add_set_option oval opt (OptionSet v)
+
+    | "-unset" ->
+      add_set_option oval (to_opt_key @@ next ()) OptionUnset
+
+    |"-native-output-dir" ->
+      let native_output_dir = next () in
+      { oval with config = { oval.config with native_output_dir } }
+
+    |"-nI" ->
+      let include_dir = next () in
+      { oval with config = {oval.config with native_include_dirs = include_dir :: oval.config.native_include_dirs } }
+
+    (* Options with zero arg *)
+    |"-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
+    |"-diffs" ->
+      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 (OptionSet None)
+    |"-disallow-sprop" ->
+      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 (OptionSet None)
+    |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval
+    |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }}
+    |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }}
+    |"-boot" -> { oval with pre = { oval.pre with boot = true }}
+    |"-output-context" -> { oval with post = { oval.post with output_context = true }}
+    |"-profile-ltac" -> Flags.profile_ltac := true; oval
+    |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }}
+    |"-quiet"|"-silent" ->
+      Flags.quiet := true;
+      Flags.make_warn false;
+      oval
+    |"-list-tags" -> set_query oval PrintTags
+    |"-time" -> { oval with config = { oval.config with time = true }}
+    |"-type-in-type" -> set_type_in_type (); oval
+    |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false)
+    |"-where" -> set_query oval PrintWhere
+    |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp help)
+    |"-v"|"--version" -> set_query oval PrintVersion
+    |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion
+
+    (* Unknown option *)
+    | s ->
+      extras := s :: !extras;
+      oval
+    end in
+    parse noval
+  in
+  try
+    parse init
+  with any -> fatal_error any
+
+(* We need to reverse a few lists *)
+let parse_args ~help ~init args =
+  let opts, extra = parse_args ~help ~init args in
+  let opts =
+    { opts with
+      pre = { opts.pre with
+              ml_includes = List.rev opts.pre.ml_includes
+            ; vo_includes = List.rev opts.pre.vo_includes
+            ; load_vernacular_list = List.rev opts.pre.load_vernacular_list
+            ; injections = List.rev opts.pre.injections
+            }
+    } in
+  opts, extra
+
+(******************************************************************************)
+(* Startup LoadPath and Modules                                               *)
+(******************************************************************************)
+(* prelude_data == From Coq Require Import Prelude. *)
+let prelude_data = "Prelude", Some "Coq", Some false
+
+let injection_commands opts =
+  if opts.pre.load_init then 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
+      Coqloadpath.init_load_path ~coqlib in
+  ml_path @ opts.pre.ml_includes ,
+  vo_path @ opts.pre.vo_includes
diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli
new file mode 100644
index 0000000000..894e0f2ef3
--- /dev/null
+++ b/sysinit/coqargs.mli
@@ -0,0 +1,107 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type color = [`ON | `AUTO | `EMACS | `OFF]
+
+val default_toplevel : Names.DirPath.t
+
+type native_compiler = Coq_config.native_compiler =
+  NativeOff | NativeOn of { ondemand : bool }
+
+type interactive_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     : interactive_top;
+}
+
+type coqargs_config = {
+  logic       : coqargs_logic_config;
+  rcfile      : string option;
+  coqlib      : string option;
+  color       : color;
+  enable_VM   : bool;
+  native_compiler : native_compiler;
+  native_output_dir : CUnix.physical_path;
+  native_include_dirs : CUnix.physical_path list;
+  debug       : bool;
+  time        : bool;
+  print_emacs : bool;
+}
+
+type coqargs_pre = {
+  boot        : bool;
+  load_init   : bool;
+  load_rcfile : bool;
+
+  ml_includes : CUnix.physical_path list;
+  vo_includes : Loadpath.vo_path list;
+
+  load_vernacular_list : (string * bool) list;
+  injections  : injection_command list;
+
+  inputstate  : string option;
+}
+
+type coqargs_query =
+  | PrintTags | PrintWhere | PrintConfig
+  | PrintVersion | PrintMachineReadableVersion
+  | PrintHelp of Usage.specific_usage
+
+type coqargs_main =
+  | Queries of coqargs_query list
+  | Run
+
+type coqargs_post = {
+  memory_stat : bool;
+  output_context : bool;
+}
+
+type t = {
+  config : coqargs_config;
+  pre : coqargs_pre;
+  main : coqargs_main;
+  post : coqargs_post;
+}
+
+(* Default options *)
+val default : t
+
+val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * string list
+
+val injection_commands : t -> injection_command list
+val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list
+
+(* 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
\ No newline at end of file
diff --git a/sysinit/coqloadpath.ml b/sysinit/coqloadpath.ml
new file mode 100644
index 0000000000..8635345e00
--- /dev/null
+++ b/sysinit/coqloadpath.ml
@@ -0,0 +1,73 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Util
+open Pp
+
+let ( / ) s1 s2 = Filename.concat s1 s2
+
+(* Recursively puts `.v` files in the LoadPath *)
+let build_stdlib_vo_path ~unix_path ~coq_path =
+  let open Loadpath in
+  { unix_path; coq_path ; has_ml = false; implicit = true; recursive = true }
+
+(* Note we don't use has_ml=true due to #12771 , we need to see if we
+   should just remove that option *)
+let build_userlib_path ~unix_path =
+  let open Loadpath in
+  if Sys.file_exists unix_path then
+    let ml_path = System.all_subdirs ~unix_path |> List.map fst in
+    let vo_path =
+      { unix_path
+      ; coq_path = Libnames.default_root_prefix
+      ; has_ml = false
+      ; implicit = false
+      ; recursive = true
+      } in
+    ml_path, [vo_path]
+  else [], []
+
+(* LoadPath for Coq user libraries *)
+let init_load_path ~coqlib =
+
+  let open Loadpath in
+  let user_contrib = coqlib/"user-contrib" in
+  let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in
+  let coqpath = Envars.coqpath in
+  let coq_path = Names.DirPath.make [Libnames.coq_root] in
+
+  (* ML includes *)
+  let plugins_dirs = System.all_subdirs ~unix_path:(coqlib/"plugins") |> List.map fst in
+
+  let contrib_ml, contrib_vo = build_userlib_path ~unix_path:user_contrib in
+
+  let misc_ml, misc_vo =
+    List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) |> List.split in
+
+  let ml_loadpath = plugins_dirs @ contrib_ml @ List.concat misc_ml in
+  let vo_loadpath =
+    (* current directory (not recursively!) *)
+    [ { unix_path = "."
+      ; coq_path = Libnames.default_root_prefix
+      ; implicit = false
+      ; has_ml = true
+      ; recursive = false
+      } ] @
+
+    (* then standard library *)
+    [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @
+
+    (* then user-contrib *)
+    contrib_vo @
+
+    (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *)
+    List.concat misc_vo
+  in
+  ml_loadpath, vo_loadpath
diff --git a/sysinit/coqloadpath.mli b/sysinit/coqloadpath.mli
new file mode 100644
index 0000000000..d853e9ea54
--- /dev/null
+++ b/sysinit/coqloadpath.mli
@@ -0,0 +1,16 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(** 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 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..6146aa60d0
--- /dev/null
+++ b/sysinit/dune
@@ -0,0 +1,8 @@
+(library
+ (name sysinit)
+ (public_name coq.sysinit)
+ (synopsis "Coq's initialization")
+ (wrapped false)
+ (libraries coq.vernac)
+ (modules coqloadpath coqargs usage)
+ )
diff --git a/sysinit/sysinit.mllib b/sysinit/sysinit.mllib
new file mode 100644
index 0000000000..9d35a931bc
--- /dev/null
+++ b/sysinit/sysinit.mllib
@@ -0,0 +1,3 @@
+Usage
+Coqloadpath
+Coqargs
diff --git a/sysinit/usage.ml b/sysinit/usage.ml
new file mode 100644
index 0000000000..1831a3f9b2
--- /dev/null
+++ b/sysinit/usage.ml
@@ -0,0 +1,112 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+let version () =
+  Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
+    Coq_config.version Coq_config.date;
+  Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version
+
+let machine_readable_version () =
+  Printf.printf "%s %s\n"
+    Coq_config.version Coq_config.caml_version
+
+(* print the usage of coqtop (or coqc) on channel co *)
+
+let print_usage_common co command =
+  output_string co command;
+  output_string co "Coq options are:\n";
+  output_string co
+"  -I dir                 look for ML files in dir\
+\n  -include dir           (idem)\
+\n  -R dir coqdir          recursively map physical dir to logical coqdir\
+\n  -Q dir coqdir          map physical dir to logical coqdir\
+\n  -top coqdir            set the toplevel name to be coqdir instead of Top\
+\n  -topfile f             set the toplevel name as though compiling f\
+\n  -coqlib dir            set the coq standard library directory\
+\n  -exclude-dir f         exclude subdirectories named f for option -R\
+\n\
+\n  -boot                  don't bind the `Coq.` prefix to the default -coqlib dir\
+\n  -noinit                don't load Coq.Init.Prelude on start \
+\n  -nois                  (idem)\
+\n  -compat X.Y            provides compatibility support for Coq version X.Y\
+\n\
+\n  -load-vernac-source f  load Coq file f.v (Load \"f\".)\
+\n  -l f                   (idem)\
+\n  -load-vernac-source-verbose f  load Coq file f.v (Load Verbose \"f\".)\
+\n  -lv f	           (idem)\
+\n  -load-vernac-object lib\
+\n                         load Coq library lib (Require lib)\
+\n  -rfrom root lib        load Coq library lib (From root Require lib.)\
+\n  -require-import lib, -ri lib\
+\n                         load and import Coq library lib\
+\n                         (equivalent to Require Import lib.)\
+\n  -require-export lib, -re lib\
+\n                         load and transitively import Coq library lib\
+\n                         (equivalent to Require Export lib.)\
+\n  -require-import-from root lib, -rifrom root lib\
+\n                         load and import Coq library lib\
+\n                         (equivalent to From root Require Import lib.)\
+\n  -require-export-from root lib, -refrom root lib\
+\n                         load and transitively import Coq library lib\
+\n                         (equivalent to From root Require Export lib.)\
+\n\
+\n  -where                 print Coq's standard library location and exit\
+\n  -config, --config      print Coq's configuration information and exit\
+\n  -v, --version          print Coq version and exit\
+\n  -print-version         print Coq version in easy to parse format and exit\
+\n  -list-tags             print highlight color tags known by Coq and exit\
+\n\
+\n  -quiet                 unset display of extra information (implies -w \"-all\")\
+\n  -w (w1,..,wn)          configure display of warnings\
+\n  -color (yes|no|auto)   configure color output\
+\n  -emacs                 tells Coq it is executed under Emacs\
+\n\
+\n  -q                     skip loading of rcfile\
+\n  -init-file f           set the rcfile to f\
+\n  -bt                    print backtraces (requires configure debug flag)\
+\n  -debug                 debug mode (implies -bt)\
+\n  -xml-debug             debug mode and print XML messages to/from coqide\
+\n  -diffs (on|off|removed) highlight differences between proof steps\
+\n  -noglob                do not dump globalizations\
+\n  -dump-glob f           dump globalizations in file f (to be used by coqdoc)\
+\n  -impredicative-set     set sort Set impredicative\
+\n  -allow-sprop           allow using the proof irrelevant SProp sort\
+\n  -disallow-sprop        forbid using the proof irrelevant SProp sort\
+\n  -sprop-cumulative      make sort SProp cumulative with the rest of the hierarchy\
+\n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
+\n  -type-in-type          disable universe consistency checking\
+\n  -mangle-names x        mangle auto-generated names using prefix x\
+\n  -set \"Foo Bar\"         enable Foo Bar (as Set Foo Bar. in a file)\
+\n  -set \"Foo Bar=value\"   set Foo Bar to value (value is interpreted according to Foo Bar's type)\
+\n  -unset \"Foo Bar\"       disable Foo Bar (as Unset Foo Bar. in a file)\
+\n  -time                  display the time taken by each command\
+\n  -profile-ltac          display the time taken by each (sub)tactic\
+\n  -m, --memory           display total heap size at program exit\
+\n                         (use environment variable\
+\n                          OCAML_GC_STATS=\"/tmp/gclog.txt\"\
+\n                          for full Gc stats dump)\
+\n  -bytecode-compiler (yes|no)        enable the vm_compute reduction machine\
+\n  -native-compiler (yes|no|ondemand) enable the native_compute reduction machine\
+\n  -native-output-dir     <directory> set the output directory for native objects\
+\n  -nI dir                OCaml include directories for the native compiler (default if not set) \
+\n  -h, -help, --help      print this list of options\
+\n"
+
+(* print the usage *)
+
+type specific_usage = {
+  executable_name : string;
+  extra_args : string;
+  extra_options : string;
+}
+
+let print_usage co { executable_name; extra_args; extra_options } =
+  print_usage_common co ("Usage: " ^ executable_name ^ " <options> " ^ extra_args ^ "\n\n");
+  output_string co extra_options
diff --git a/sysinit/usage.mli b/sysinit/usage.mli
new file mode 100644
index 0000000000..2d1a8e94cc
--- /dev/null
+++ b/sysinit/usage.mli
@@ -0,0 +1,28 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** {6 Prints the version number on the standard output. } *)
+
+val version : unit -> unit
+val machine_readable_version : unit -> unit
+
+(** {6 extra arguments or options to print when asking usage for a
+     given executable. } *)
+
+type specific_usage = {
+  executable_name : string;
+  extra_args : string;
+  extra_options : string;
+}
+
+(** {6 Prints the generic part and specific part of usage for a
+       given executable. } *)
+
+val print_usage : out_channel -> specific_usage -> unit
-- 
cgit v1.2.3


From 4c4d6cfacf92b555546055a45edc19b68245b83c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 6 Jan 2021 14:19:59 +0100
Subject: [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.
---
 sysinit/coqargs.ml    |  45 +++++++++--------
 sysinit/coqargs.mli   |  13 +++--
 sysinit/coqinit.ml    | 135 ++++++++++++++++++++++++++++++++++++++++++++++++++
 sysinit/coqinit.mli   |  58 ++++++++++++++++++++++
 sysinit/dune          |   1 -
 sysinit/sysinit.mllib |   1 +
 6 files changed, 224 insertions(+), 29 deletions(-)
 create mode 100644 sysinit/coqinit.ml
 create mode 100644 sysinit/coqinit.mli

(limited to 'sysinit')

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
-- 
cgit v1.2.3


From b9bac1d7ef4a4c06ebe842ffd9aac322186a65d3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 6 Jan 2021 14:31:34 +0100
Subject: [coqc] move -output-context from sysinit/coqargs to coqc proper

---
 sysinit/coqargs.ml  | 5 +----
 sysinit/coqargs.mli | 1 -
 2 files changed, 1 insertion(+), 5 deletions(-)

(limited to 'sysinit')

diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index 32025ac434..bb0c4882e6 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -93,7 +93,6 @@ type coqargs_main =
 
 type coqargs_post = {
   memory_stat : bool;
-  output_context : bool;
 }
 
 type t = {
@@ -143,7 +142,6 @@ let default_queries = []
 
 let default_post = {
   memory_stat  = false;
-  output_context = false;
 }
 
 let default = {
@@ -440,10 +438,9 @@ let parse_args ~usage ~init arglist : t * string list =
       warn_deprecated_sprop_cumul();
       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" ->
diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli
index ebf367270d..acf941f730 100644
--- a/sysinit/coqargs.mli
+++ b/sysinit/coqargs.mli
@@ -74,7 +74,6 @@ type coqargs_main =
 
 type coqargs_post = {
   memory_stat : bool;
-  output_context : bool;
 }
 
 type t = {
-- 
cgit v1.2.3


From f5ec3f5cbd4bc2e0f65e1c52143b199ce7c2a5ad Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 6 Jan 2021 17:13:59 +0100
Subject: [coqtop] handle -print-module-uid after initialization

---
 sysinit/coqargs.ml | 12 ------------
 1 file changed, 12 deletions(-)

(limited to 'sysinit')

diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index bb0c4882e6..19350b7e98 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -220,15 +220,6 @@ let get_float ~opt n =
   with Failure _ ->
     error_wrong_arg ("Error: float expected after option "^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
@@ -361,9 +352,6 @@ let parse_args ~usage ~init arglist : t * string list =
       Goptions.set_string_option_value ["Mangle"; "Names"; "Prefix"] (next ());
       oval
 
-    |"-print-mod-uid" ->
-      let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0
-
     |"-profile-ltac-cutoff" ->
       Flags.profile_ltac := true;
       Flags.profile_ltac_cutoff := get_float ~opt (next ());
-- 
cgit v1.2.3


From 2caae4d530ba97ced98711986dc504f9becdab81 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 6 Jan 2021 17:14:22 +0100
Subject: [coqargs] use standard option injection for -mangle-names

---
 sysinit/coqargs.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'sysinit')

diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index 19350b7e98..ac9e430d31 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -348,9 +348,8 @@ let parse_args ~usage ~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
+      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;
-- 
cgit v1.2.3


From 0a531fae53c31ef76ff25fbfd3ceb8b5b33aa264 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 6 Jan 2021 17:31:33 +0100
Subject: [coqargs] use standard option injection for -type-in-type

---
 sysinit/coqargs.ml  | 8 +++-----
 sysinit/coqargs.mli | 1 +
 sysinit/coqinit.ml  | 1 +
 3 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'sysinit')

diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index ac9e430d31..faa26423e5 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -25,10 +25,6 @@ let error_missing_arg s =
 (* Imperative effects! This must be fixed at some point.                      *)
 (******************************************************************************)
 
-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
@@ -52,6 +48,7 @@ type injection_command =
 type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
   indices_matter    : bool;
+  type_in_type      : bool;
   toplevel_name     : top;
 }
 
@@ -109,6 +106,7 @@ let default_native = Coq_config.native_compiler
 let default_logic_config = {
   impredicative_set = Declarations.PredicativeSet;
   indices_matter = false;
+  type_in_type = false;
   toplevel_name = TopLogical default_toplevel;
 }
 
@@ -435,7 +433,7 @@ let parse_args ~usage ~init arglist : t * string list =
       Flags.make_warn false;
       oval
     |"-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 usage)
diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli
index acf941f730..cc622fabe3 100644
--- a/sysinit/coqargs.mli
+++ b/sysinit/coqargs.mli
@@ -33,6 +33,7 @@ type injection_command =
 type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
   indices_matter    : bool;
+  type_in_type      : bool;
   toplevel_name     : top;
 }
 
diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml
index cbecc52827..16c8389de5 100644
--- a/sysinit/coqinit.ml
+++ b/sysinit/coqinit.ml
@@ -105,6 +105,7 @@ let init_runtime opts =
   (* 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);
-- 
cgit v1.2.3


From d414273bbd53681baecf3ddc6d343243c80e8103 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 6 Jan 2021 18:21:55 +0100
Subject: [coqargs] use standard option injection for -print-emacs

---
 sysinit/coqargs.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'sysinit')

diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index faa26423e5..c4f12f6bb7 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -172,7 +172,7 @@ 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;
+  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 =
-- 
cgit v1.2.3


From 6e258b391363aa2345c4dc265ba381b1712fe083 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 6 Jan 2021 19:57:08 +0100
Subject: make the linter happy

---
 sysinit/coqargs.mli   | 2 +-
 sysinit/sysinit.mllib | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'sysinit')

diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli
index cc622fabe3..aef50193f2 100644
--- a/sysinit/coqargs.mli
+++ b/sysinit/coqargs.mli
@@ -103,4 +103,4 @@ 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
\ No newline at end of file
+val set_option : Goptions.option_name * option_command -> unit
diff --git a/sysinit/sysinit.mllib b/sysinit/sysinit.mllib
index 715de2bb82..6e86536648 100644
--- a/sysinit/sysinit.mllib
+++ b/sysinit/sysinit.mllib
@@ -1,4 +1,4 @@
 Usage
 Coqloadpath
 Coqargs
-Coqinit
\ No newline at end of file
+Coqinit
-- 
cgit v1.2.3