Merge PR #6693: [toplevel] Refactor command line argument handling.

7 files changed, 831 insertions, 632 deletions

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
new file mode 100644
index 000000000..5b73471c5
--- /dev/null
+++ b/toplevel/coqargs.ml
@@ -0,0 +1,575 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+let warning s = Flags.(with_option warn Feedback.msg_warning (Pp.strbrk s))
+
+let fatal_error ?extra exn =
+  Topfmt.print_err_exn ?extra exn;
+  let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in
+  exit exit_code
+
+let error_missing_arg s =
+  prerr_endline ("Error: extra argument expected after option "^s);
+  prerr_endline "See -help for the syntax of supported options";
+  exit 1
+
+(******************************************************************************)
+(* Imperative effects! This must be fixed at some point.                      *)
+(******************************************************************************)
+let set_worker_id opt s =
+  assert (s <> "master");
+  Flags.async_proofs_worker_id := s
+
+let set_type_in_type () =
+  let typing_flags = Environ.typing_flags (Global.env ()) in
+  Global.set_typing_flags { typing_flags with Declarations.check_universes = false }
+
+(******************************************************************************)
+
+type compilation_mode = BuildVo | BuildVio | Vio2Vo
+type color = [`ON | `AUTO | `OFF]
+
+type coq_cmdopts = {
+
+  load_init   : bool;
+  load_rcfile : bool;
+  rcfile      : string option;
+
+  ml_includes : string list;
+  vo_includes : (string * Names.DirPath.t * bool) list;
+  vo_requires : (string * string option * bool option) list;
+  (* None = No Import; Some false = Import; Some true = Export *)
+
+  (* XXX: Fusion? *)
+  batch_mode : bool;
+  compilation_mode : compilation_mode;
+
+  toplevel_name : Names.DirPath.t;
+  toploop : string option;
+
+  compile_list: (string * bool) list;  (* bool is verbosity  *)
+  compilation_output_name : string option;
+
+  load_vernacular_list : (string * bool) list;
+
+  vio_checking: bool;
+  vio_tasks   : (int list * string) list;
+  vio_files   : string list;
+  vio_files_j : int;
+
+  color : color;
+
+  impredicative_set : Declarations.set_predicativity;
+  stm_flags   : Stm.AsyncOpts.stm_opt;
+  debug       : bool;
+  time        : bool;
+
+  filter_opts : bool;
+
+  glob_opt    : bool;
+
+  memory_stat : bool;
+  print_tags  : bool;
+  print_where : bool;
+  print_config: bool;
+  output_context : bool;
+
+  inputstate  : string option;
+  outputstate : string option;
+
+}
+
+let init_args = {
+
+  load_init   = true;
+  load_rcfile = true;
+  rcfile      = None;
+
+  ml_includes = [];
+  vo_includes = [];
+  vo_requires = [];
+
+  batch_mode = false;
+  compilation_mode = BuildVo;
+
+  toplevel_name = Names.(DirPath.make [Id.of_string "Top"]);
+  toploop = None;
+
+  compile_list = [];
+  compilation_output_name = None;
+
+  load_vernacular_list = [];
+
+  vio_checking = false;
+  vio_tasks    = [];
+  vio_files    = [];
+  vio_files_j  = 0;
+
+  color = `AUTO;
+
+  impredicative_set = Declarations.PredicativeSet;
+  stm_flags    = Stm.AsyncOpts.default_opts;
+  debug        = false;
+  time         = false;
+
+  filter_opts  = false;
+
+  glob_opt     = false;
+
+  memory_stat  = false;
+  print_tags   = false;
+  print_where  = false;
+  print_config = false;
+  output_context = false;
+
+  inputstate  = None;
+  outputstate = None;
+}
+
+(******************************************************************************)
+(* Functional arguments                                                       *)
+(******************************************************************************)
+let add_ml_include opts s =
+  { opts with ml_includes = s :: opts.ml_includes }
+
+let add_vo_include opts d p implicit =
+  let p = Libnames.dirpath_of_string p in
+  { opts with vo_includes = (d, p, implicit) :: opts.vo_includes }
+
+let add_vo_require opts d p export =
+  { opts with vo_requires = (d, p, export) :: opts.vo_requires }
+
+let add_compat_require opts v =
+  match v with
+  | Flags.V8_5 -> add_vo_require opts "Coq.Compat.Coq85" None (Some false)
+  | Flags.V8_6 -> add_vo_require opts "Coq.Compat.Coq86" None (Some false)
+  | Flags.V8_7 -> add_vo_require opts "Coq.Compat.Coq87" None (Some false)
+  | Flags.VOld | Flags.Current -> opts
+
+let set_batch_mode opts =
+  Flags.quiet := true;
+  System.trust_file_cache := false;
+  { opts with batch_mode = true }
+
+let add_compile opts verbose s =
+  let opts = set_batch_mode opts in
+  if not opts.glob_opt then Dumpglob.dump_to_dotglob ();
+  (** make the file name explicit; needed not to break up Coq loadpath stuff. *)
+  let s =
+    let open Filename in
+    if is_implicit s
+    then concat current_dir_name s
+    else s
+  in
+  { opts with compile_list = (s,verbose) :: opts.compile_list }
+
+let add_load_vernacular opts verb s =
+  { opts with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.load_vernacular_list }
+
+let add_vio_task opts f =
+  let opts = set_batch_mode opts in
+  { opts with vio_tasks = f :: opts.vio_tasks }
+
+let add_vio_file opts f =
+  let opts = set_batch_mode opts in
+  { opts with vio_files = f :: opts.vio_files }
+
+let set_vio_checking_j opts opt j =
+  try { opts with vio_files_j = int_of_string j }
+  with Failure _ ->
+    prerr_endline ("The first argument of " ^ opt ^ " must the number");
+    prerr_endline "of concurrent workers to be used (a positive integer).";
+    prerr_endline "Makefiles generated by coq_makefile should be called";
+    prerr_endline "setting the J variable like in 'make vio2vo J=3'";
+    exit 1
+
+(** Options for proof general *)
+let set_emacs opts =
+  if not (Option.is_empty opts.toploop) then
+    CErrors.user_err Pp.(str "Flag -emacs is incompatible with a custom toplevel loop");
+  Coqloop.print_emacs := true;
+  Printer.enable_goal_tags_printing := true;
+  { opts with color = `OFF }
+
+let set_color opts = function
+| "yes" | "on" -> { opts with color = `ON }
+| "no" | "off" -> { opts with color = `OFF }
+| "auto" -> { opts with color = `AUTO }
+| _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1
+
+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 inputstate = Some s }
+
+let warn_deprecated_outputstate =
+  CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated"
+         (fun () ->
+          Pp.strbrk "The outputstate option is deprecated and discouraged.")
+
+let set_outputstate opts s =
+  warn_deprecated_outputstate ();
+  { opts with outputstate = Some s }
+
+let exitcode opts = if opts.filter_opts then 2 else 0
+
+(******************************************************************************)
+(* Parsing helpers                                                            *)
+(******************************************************************************)
+let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
+
+let get_bool opt = function
+  | "yes" | "on" -> true
+  | "no" | "off" -> false
+  | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1
+
+let get_int opt n =
+  try int_of_string n
+  with Failure _ ->
+    prerr_endline ("Error: integer expected after option "^opt); exit 1
+
+let get_float opt n =
+  try float_of_string n
+  with Failure _ ->
+    prerr_endline ("Error: float expected after option "^opt); exit 1
+
+let get_host_port opt s =
+  match CString.split ':' s with
+  | [host; portr; portw] ->
+       Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
+  | ["stdfds"] -> Some Spawned.AnonPipe
+  | _ ->
+     prerr_endline ("Error: host:portr:portw or stdfds expected after option "^opt);
+     exit 1
+
+let get_error_resilience opt = function
+  | "on" | "all" | "yes" -> `All
+  | "off" | "no" -> `None
+  | s -> `Only (CString.split ',' s)
+
+let get_priority opt s =
+  try CoqworkmgrApi.priority_of_string s
+  with Invalid_argument _ ->
+    prerr_endline ("Error: low/high expected after "^opt); exit 1
+
+let get_async_proofs_mode opt = let open Stm.AsyncOpts in function
+  | "no" | "off" -> APoff
+  | "yes" | "on" -> APon
+  | "lazy" -> APonLazy
+  | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1
+
+let get_cache opt = function
+  | "force" -> Some Stm.AsyncOpts.Force
+  | _ -> prerr_endline ("Error: force expected after "^opt); exit 1
+
+let is_not_dash_option = function
+  | Some f when String.length f > 0 && f.[0] <> '-' -> true
+  | _ -> false
+
+let rec add_vio_args peek next oval =
+  if is_not_dash_option (peek ()) then
+    let oval = add_vio_file oval (next ()) in
+    add_vio_args peek next oval
+  else oval
+
+let get_native_name s =
+  (* We ignore even critical errors because this mode has to be super silent *)
+  try
+    String.concat "/" [Filename.dirname s;
+      Nativelib.output_dir; Library.native_name_from_filename s]
+  with _ -> ""
+
+(*s Parsing of the command line.
+    We no longer use [Arg.parse], in order to use share [Usage.print_usage]
+    between coqtop and coqc. *)
+
+let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesystem"
+    (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned")
+
+exception NoCoqLib
+
+let usage batch =
+  begin
+    try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib)
+    with NoCoqLib -> usage_no_coqlib ()
+  end;
+  let lp = Coqinit.toplevel_init_load_path () in
+  (* Necessary for finding the toplevels below *)
+  List.iter Mltop.add_coq_path lp;
+  if batch then Usage.print_usage_coqc ()
+  else begin
+    Mltop.load_ml_objects_raw_rex
+      (Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$"));
+    Usage.print_usage_coqtop ()
+  end
+
+(* Main parsing routine *)
+let parse_args arglist : coq_cmdopts * 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 peek_next () = match !args with
+      | x::_ -> Some x
+      | [] -> None
+    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 two arg *)
+    |"-check-vio-tasks" ->
+      let tno = get_task_list (next ()) in
+      let tfile = next () in
+      add_vio_task oval (tno,tfile)
+
+    |"-schedule-vio-checking" ->
+      let oval = { oval with vio_checking = true } in
+      let oval = set_vio_checking_j oval opt (next ()) in
+      let oval = add_vio_file oval (next ()) in
+      add_vio_args peek_next next oval
+
+    |"-schedule-vio2vo" ->
+      let oval = set_vio_checking_j oval opt (next ()) in
+      let oval = add_vio_file oval (next ()) in
+      add_vio_args peek_next next oval
+
+    (* Options with one arg *)
+    |"-coqlib" ->
+      Flags.coqlib_spec := true;
+      Flags.coqlib := (next ());
+      oval
+
+    |"-async-proofs" ->
+      { oval with stm_flags = { oval.stm_flags with
+        Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next())
+      }}
+    |"-async-proofs-j" ->
+      { oval with stm_flags = { oval.stm_flags with
+        Stm.AsyncOpts.async_proofs_n_workers = (get_int opt (next ()))
+      }}
+    |"-async-proofs-cache" ->
+      { oval with stm_flags = { oval.stm_flags with
+        Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ())
+      }}
+
+    |"-async-proofs-tac-j" ->
+      { oval with stm_flags = { oval.stm_flags with
+        Stm.AsyncOpts.async_proofs_n_tacworkers = (get_int opt (next ()))
+      }}
+
+    |"-async-proofs-worker-priority" ->
+      WorkerLoop.async_proofs_worker_priority := get_priority opt (next ());
+      oval
+
+    |"-async-proofs-private-flags" ->
+      { oval with stm_flags = { oval.stm_flags with
+        Stm.AsyncOpts.async_proofs_private_flags = Some (next ());
+      }}
+
+    |"-async-proofs-tactic-error-resilience" ->
+      { oval with stm_flags = { oval.stm_flags with
+        Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ())
+      }}
+
+    |"-async-proofs-command-error-resilience" ->
+      { oval with stm_flags = { oval.stm_flags with
+        Stm.AsyncOpts.async_proofs_cmd_error_resilience = get_bool opt (next ())
+      }}
+
+    |"-async-proofs-delegation-threshold" ->
+      { oval with stm_flags = { oval.stm_flags with
+        Stm.AsyncOpts.async_proofs_delegation_threshold = get_float opt (next ())
+      }}
+
+    |"-worker-id" -> set_worker_id opt (next ()); oval
+
+    |"-compat" ->
+      let v = G_vernac.parse_compat_version ~allow_old:false (next ()) in
+      Flags.compat_version := v;
+      add_compat_require oval v
+
+    |"-compile" ->
+      add_compile oval false (next ())
+
+    |"-compile-verbose" ->
+      add_compile oval true (next ())
+
+    |"-dump-glob" ->
+      Dumpglob.dump_into_file (next ());
+      { oval with glob_opt = true }
+
+    |"-feedback-glob" ->
+      Dumpglob.feedback_glob (); oval
+
+    |"-exclude-dir" ->
+      System.exclude_directory (next ()); oval
+
+    |"-init-file" ->
+      { oval with rcfile = Some (next ()); }
+
+    |"-inputstate"|"-is" ->
+      set_inputstate oval (next ())
+
+    |"-outputstate" ->
+      set_outputstate oval (next ())
+
+    |"-load-ml-object" ->
+      Mltop.dir_ml_load (next ()); oval
+
+    |"-load-ml-source" ->
+      Mltop.dir_ml_use (next ()); oval
+
+    |"-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 ())
+
+    |"-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
+
+    |"-require" -> add_vo_require oval (next ()) None (Some false)
+
+    |"-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 toplevel_name = topname }
+
+    |"-main-channel" ->
+      Spawned.main_channel := get_host_port opt (next()); oval
+
+    |"-control-channel" ->
+      Spawned.control_channel := get_host_port opt (next()); oval
+
+    |"-vio2vo" ->
+      let oval = add_compile oval false (next ()) in
+      { oval with compilation_mode = Vio2Vo }
+
+    |"-toploop" ->
+      if !Coqloop.print_emacs then
+        CErrors.user_err Pp.(str "Flags -toploop and -emacs are incompatible");
+      { oval with toploop = Some (next ()) }
+
+    |"-w" | "-W" ->
+      let w = next () in
+      if w = "none" then
+        (CWarnings.set_flags w; oval)
+      else
+        let w = CWarnings.get_flags () ^ "," ^ w in
+        CWarnings.set_flags (CWarnings.normalize_flags_string w);
+        oval
+
+    |"-o" -> { oval with compilation_output_name = Some (next()) }
+
+    (* Options with zero arg *)
+    |"-async-queries-always-delegate"
+    |"-async-proofs-always-delegate"
+    |"-async-proofs-full" ->
+      { oval with stm_flags = { oval.stm_flags with
+        Stm.AsyncOpts.async_proofs_full = true;
+      }}
+    |"-async-proofs-never-reopen-branch" ->
+      { oval with stm_flags = { oval.stm_flags with
+        Stm.AsyncOpts.async_proofs_never_reopen_branch = true
+      }}
+    |"-batch" -> set_batch_mode oval
+    |"-test-mode" -> Flags.test_mode := true; oval
+    |"-beautify" -> Flags.beautify := true; oval
+    |"-boot" -> Flags.boot := true; { oval with load_rcfile = false; }
+    |"-bt" -> Backtrace.record_backtrace true; oval
+    |"-color" -> set_color oval (next ())
+    |"-config"|"--config" -> { oval with print_config = true }
+    |"-debug" -> Coqinit.set_debug (); oval
+    |"-stm-debug" -> Stm.stm_debug := true; oval
+    |"-emacs" -> set_emacs oval
+    |"-filteropts" -> { oval with filter_opts = true }
+    |"-ideslave" ->
+      if !Coqloop.print_emacs then
+        CErrors.user_err Pp.(str "Flags -ideslave and -emacs are incompatible");
+      Flags.ide_slave := true;
+      { oval with toploop = Some "coqidetop" }
+
+    |"-impredicative-set" ->
+      { oval with impredicative_set = Declarations.ImpredicativeSet }
+    |"-indices-matter" -> Indtypes.enforce_indices_matter (); oval
+    |"-m"|"--memory" -> { oval with memory_stat = true }
+    |"-noinit"|"-nois" -> { oval with load_init = false }
+    |"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with glob_opt = true }
+    |"-native-compiler" ->
+      if not Coq_config.native_compiler then
+        warning "Native compilation was disabled at configure time."
+      else Flags.output_native_objects := true; oval
+    |"-output-context" -> { oval with output_context = true }
+    |"-profile-ltac" -> Flags.profile_ltac := true; oval
+    |"-q" -> { oval with load_rcfile = false; }
+    |"-quiet"|"-silent" ->
+      Flags.quiet := true;
+      Flags.make_warn false;
+      oval
+    |"-quick" -> { oval with compilation_mode = BuildVio }
+    |"-list-tags" -> { oval with print_tags = true }
+    |"-time" -> { oval with time = true }
+    |"-type-in-type" -> set_type_in_type (); oval
+    |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false)
+    |"-where" -> { oval with print_where = true }
+    |"-h"|"-H"|"-?"|"-help"|"--help" -> usage oval.batch_mode; oval
+    |"-v"|"--version" -> Usage.version (exitcode oval)
+    |"-print-version"|"--print-version" ->
+      Usage.machine_readable_version (exitcode oval)
+
+    (* Unknown option *)
+    | s ->
+      extras := s :: !extras;
+      oval
+    end in
+    parse noval
+  in
+  try
+    parse init_args
+  with any -> fatal_error any
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
new file mode 100644
index 000000000..8ee1a8f55
--- /dev/null
+++ b/toplevel/coqargs.mli
@@ -0,0 +1,63 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type compilation_mode = BuildVo | BuildVio | Vio2Vo
+type color = [`ON | `AUTO | `OFF]
+
+type coq_cmdopts = {
+
+  load_init   : bool;
+  load_rcfile : bool;
+  rcfile      : string option;
+
+  ml_includes : string list;
+  vo_includes : (string * Names.DirPath.t * bool) list;
+  vo_requires : (string * string option * bool option) list;
+
+  (* Fuse these two? Currently, [batch_mode] is only used to
+     distinguish coqc / coqtop in help display. *)
+  batch_mode : bool;
+  compilation_mode : compilation_mode;
+
+  toplevel_name : Names.DirPath.t;
+  toploop : string option;
+
+  compile_list: (string * bool) list;  (* bool is verbosity  *)
+  compilation_output_name : string option;
+
+  load_vernacular_list : (string * bool) list;
+
+  vio_checking: bool;
+  vio_tasks   : (int list * string) list;
+  vio_files   : string list;
+  vio_files_j : int;
+
+  color : color;
+
+  impredicative_set : Declarations.set_predicativity;
+  stm_flags   : Stm.AsyncOpts.stm_opt;
+  debug       : bool;
+  time        : bool;
+
+  filter_opts : bool;
+
+  glob_opt    : bool;
+
+  memory_stat : bool;
+  print_tags  : bool;
+  print_where : bool;
+  print_config: bool;
+  output_context : bool;
+
+  inputstate  : string option;
+  outputstate : string option;
+
+}
+
+val parse_args : string list -> coq_cmdopts * string list
+val exitcode : coq_cmdopts -> int
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 10205964a..8574092b8 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -20,21 +20,15 @@ let set_debug () =
   does not exist. *)
 
 let rcdefaultname = "coqrc"
-let rcfile = ref ""
-let rcfile_specified = ref false
-let set_rcfile s = rcfile := s; rcfile_specified := true
 
-let load_rc = ref true
-let no_load_rc () = load_rc := false
-
-let load_rcfile ~time doc sid =
-  if !load_rc then
+let load_rcfile ~rcfile ~time doc sid =
     try
-      if !rcfile_specified then
-        if CUnix.file_readable_p !rcfile then
-          Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid !rcfile
-        else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
-      else
+      match rcfile with
+      | Some rcfile ->
+        if CUnix.file_readable_p rcfile then
+          Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid rcfile
+        else raise (Sys_error ("Cannot read rcfile: "^ rcfile))
+      | None ->
 	try
 	  let warn x = Feedback.msg_warning (str x) in
 	  let inferedrc = List.find CUnix.file_readable_p [
@@ -54,9 +48,6 @@ let load_rcfile ~time doc sid =
       let reraise = CErrors.push reraise in
       let () = Feedback.msg_info (str"Load of rcfile failed.") in
       iraise reraise
-  else
-    (Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.");
-     doc, sid)
 
 (* Recursively puts dir in the LoadPath if -nois was not passed *)
 let build_stdlib_path ~load_init ~unix_path ~coq_path ~with_ml =
@@ -77,13 +68,6 @@ let build_userlib_path ~unix_path =
       }
   }
 
-(* Options -I, -I-as, and -R of the command line *)
-let includes = ref []
-let push_include s alias implicit =
-  includes := (s, alias, implicit) :: !includes
-let ml_includes = ref []
-let push_ml_include s = ml_includes := s :: !ml_includes
-
 let ml_path_if c p =
   let open Mltop in
   let f x = { recursive = false; path_spec = MlPath x } in
@@ -128,17 +112,7 @@ let libs_init_load_path ~load_init =
                            coq_path = Libnames.default_root_prefix;
                            implicit = false;
                            has_ml = AddTopML }
-    } ] @
-
-  (* additional loadpaths, given with options -Q and -R *)
-  List.map
-    (fun (unix_path, coq_path, implicit) ->
-       { recursive = true;
-         path_spec = VoPath { unix_path; coq_path; has_ml = Mltop.AddNoML; implicit } })
-      (List.rev !includes) @
-
-  (* additional ml directories, given with option -I *)
-  List.map (fun s -> {recursive = false; path_spec = MlPath s}) (List.rev !ml_includes)
+    } ]
 
 (* Initialises the Ocaml toplevel before launching it, so that it can
    find the "include" file in the *source* directory *)
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 0d2da84bb..0ceba5b38 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -10,19 +10,12 @@
 
 val set_debug : unit -> unit
 
-val set_rcfile : string -> unit
-
-val no_load_rc : unit -> unit
-val load_rcfile : time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
-
-val push_include : string -> Names.DirPath.t -> bool -> unit
-(** [push_include phys_path log_path implicit] *)
-
-val push_ml_include : string -> unit
+val load_rcfile : rcfile:(string option) -> time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
 
 val init_ocaml_path : unit -> unit
 
 (* LoadPath for toploop toplevels *)
 val toplevel_init_load_path : unit ->  Mltop.coq_path list
+
 (* LoadPath for Coq user libraries *)
 val libs_init_load_path : load_init:bool -> Mltop.coq_path list
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 329107093..9058f0846 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -7,8 +7,7 @@
 (************************************************************************)
 
 open Pp
-open CErrors
-open Libnames
+open Coqargs
 
 let () = at_exit flush_all
 
@@ -31,66 +30,21 @@ let print_header () =
 
 let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s))
 
-let toploop = ref None
-
-let color : [`ON | `AUTO | `OFF] ref = ref `AUTO
-let set_color = function
-| "yes" | "on" -> color := `ON
-| "no" | "off" -> color := `OFF
-| "auto" -> color := `AUTO
-| _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1
-
-let init_color () =
-  let has_color = match !color with
-  | `OFF -> false
-  | `ON -> true
-  | `AUTO ->
-    Terminal.has_style Unix.stdout &&
-    Terminal.has_style Unix.stderr &&
-    (* emacs compilation buffer does not support colors by default,
-       its TERM variable is set to "dumb". *)
-    try Sys.getenv "TERM" <> "dumb" with Not_found -> false
-  in
-  if has_color then begin
-    let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in
-    match colors with
-    | None ->
-      (** Default colors *)
-      Topfmt.init_terminal_output ~color:true
-    | Some "" ->
-      (** No color output *)
-      Topfmt.init_terminal_output ~color:false
-    | Some s ->
-      (** Overwrite all colors *)
-      Topfmt.clear_styles ();
-      Topfmt.parse_color_config s;
-      Topfmt.init_terminal_output ~color:true
-  end
-  else
-    Topfmt.init_terminal_output ~color:false
-
-let toploop_init = ref begin fun x ->
-  let () = init_color () in
-  let () = CoqworkmgrApi.init !WorkerLoop.async_proofs_worker_priority in
-  x
-  end
-
 (* Feedback received in the init stage, this is different as the STM
    will not be generally be initialized, thus stateid, etc... may be
    bogus. For now we just print to the console too *)
 let coqtop_init_feed = Coqloop.coqloop_feed
 let drop_last_doc = ref None
-let measure_time = ref false
 
 (* Default toplevel loop *)
-let console_toploop_run doc =
+let console_toploop_run opts doc =
   (* We initialize the console only if we run the toploop_run *)
   let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in
   if Dumpglob.dump () then begin
     Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
     Dumpglob.noglob ()
   end;
-  let doc = Coqloop.loop ~time:!measure_time doc in
+  let doc = Coqloop.loop ~time:opts.time doc in
   (* Initialise and launch the Ocaml toplevel *)
   drop_last_doc := Some doc;
   Coqinit.init_ocaml_path();
@@ -100,10 +54,7 @@ let console_toploop_run doc =
 
 let toploop_run = ref console_toploop_run
 
-let output_context = ref false
-
 let memory_stat = ref false
-
 let print_memory_stat () =
   begin (* -m|--memory from the command-line *)
     if !memory_stat then
@@ -124,133 +75,87 @@ let print_memory_stat () =
 let _ = at_exit print_memory_stat
 
 (******************************************************************************)
-(* Engagement                                                                 *)
-(******************************************************************************)
-let impredicative_set = ref Declarations.PredicativeSet
-let set_impredicative_set c = impredicative_set := Declarations.ImpredicativeSet
-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 engage () =
-  Global.set_engagement !impredicative_set
-
-(******************************************************************************)
-(* Interactive toplevel name                                                  *)
-(******************************************************************************)
-let toplevel_default_name = Names.(DirPath.make [Id.of_string "Top"])
-let toplevel_name = ref toplevel_default_name
-let set_toplevel_name dir =
-  if Names.DirPath.is_empty dir then user_err Pp.(str "Need a non empty toplevel module name");
-  toplevel_name := dir
-
-(******************************************************************************)
 (* Input/Output State                                                         *)
 (******************************************************************************)
-let warn_deprecated_inputstate =
-  CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
-         (fun () -> strbrk "The inputstate option is deprecated and discouraged.")
-
-let inputstate = ref ""
-let set_inputstate s =
-  warn_deprecated_inputstate ();
-  inputstate:=s
-let inputstate () =
-  if not (CString.is_empty !inputstate) then
-    let fname = Loadpath.locate_file (CUnix.make_suffix !inputstate ".coq") in
-    States.intern_state fname
-
-let warn_deprecated_outputstate =
-  CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated"
-         (fun () ->
-          strbrk "The outputstate option is deprecated and discouraged.")
-
-let outputstate = ref ""
-let set_outputstate s =
-  warn_deprecated_outputstate ();
-  outputstate:=s
-let outputstate () =
-  if not (CString.is_empty !outputstate) then
-    let fname = CUnix.make_suffix !outputstate ".coq" in
-    States.extern_state fname
+let inputstate opts =
+  Option.iter (fun istate_file ->
+    let fname = Loadpath.locate_file (CUnix.make_suffix istate_file ".coq") in
+    States.intern_state fname) opts.inputstate
+
+let outputstate opts =
+  Option.iter (fun ostate_file ->
+    let fname = CUnix.make_suffix ostate_file ".coq" in
+    States.extern_state fname) opts.outputstate
 
 (******************************************************************************)
 (* Interactive Load File Simulation                                           *)
 (******************************************************************************)
-let load_vernacular_list = ref ([] : (string * bool) list)
-
-let add_load_vernacular verb s =
-  load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list
-
-let load_vernacular ~time doc sid =
+let load_vernacular opts doc sid =
   List.fold_left
     (fun (doc,sid) (f_in, verbosely) ->
       let s = Loadpath.locate_file f_in in
       if !Flags.beautify then
-        Flags.with_option Flags.beautify_file (Vernac.load_vernac ~time ~verbosely ~interactive:false ~check:true doc sid) f_in
+        Flags.with_option Flags.beautify_file (Vernac.load_vernac ~time:opts.time ~verbosely ~interactive:false ~check:true doc sid) f_in
       else
-        Vernac.load_vernac ~time ~verbosely ~interactive:false ~check:true doc sid s)
-    (doc, sid) (List.rev !load_vernacular_list)
-
-let load_init_vernaculars ~time doc sid =
-  let doc, sid = Coqinit.load_rcfile ~time doc sid in
-  load_vernacular ~time doc sid
+        Vernac.load_vernac ~time:opts.time ~verbosely ~interactive:false ~check:true doc sid s)
+    (doc, sid) (List.rev opts.load_vernacular_list)
+
+let load_init_vernaculars opts doc sid =
+  let doc, sid = if opts.load_rcfile then
+      Coqinit.load_rcfile ~rcfile:opts.rcfile ~time:opts.time doc sid
+    else begin
+      Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.");
+      doc,sid
+    end in
+  load_vernacular opts doc sid
 
 (******************************************************************************)
-(* Required Modules                                                           *)
+(* Startup LoadPath and Modules                                               *)
 (******************************************************************************)
-let set_include d p implicit =
-  let p = dirpath_of_string p in
-  Coqinit.push_include d p implicit
+(* prelude_data == From Coq Require Export Prelude. *)
+let prelude_data = "Prelude", Some "Coq", Some true
 
-(* None = No Import; Some false = Import; Some true = Export *)
-let require_list = ref ([] : (string * string option * bool option) list)
-let add_require s = require_list := s :: !require_list
+let require_libs opts =
+  if opts.load_init then prelude_data :: opts.vo_requires else opts.vo_requires
 
-let load_init = ref true
+let cmdline_load_path opts =
+  let open Mltop in
+  (* loadpaths given by options -Q and -R *)
+  List.map
+    (fun (unix_path, coq_path, implicit) ->
+       { recursive = true;
+         path_spec = VoPath { unix_path; coq_path; has_ml = Mltop.AddNoML; implicit } })
+      (List.rev opts.vo_includes) @
 
-(* From Coq Require Import Prelude. *)
-let prelude_data = "Prelude", Some "Coq", Some true
+  (* additional ml directories, given with option -I *)
+  List.map (fun s -> {recursive = false; path_spec = MlPath s}) (List.rev opts.ml_includes)
 
-let require_libs () =
-  if !load_init then prelude_data :: !require_list else !require_list
-
-let add_compat_require v =
-  match v with
-  | Flags.V8_5 -> add_require ("Coq.Compat.Coq85", None, Some false)
-  | Flags.V8_6 -> add_require ("Coq.Compat.Coq86", None, Some false)
-  | Flags.V8_7 -> add_require ("Coq.Compat.Coq87", None, Some false)
-  | Flags.VOld | Flags.Current -> ()
+let build_load_path opts =
+  Coqinit.libs_init_load_path ~load_init:opts.load_init @
+  cmdline_load_path opts
 
 (******************************************************************************)
-(* File Compilation                                                           *)
+(* Fatal Errors                                                               *)
 (******************************************************************************)
 
-let glob_opt = ref false
-
-let compile_list = ref ([] : (bool * string) list)
-
-type compilation_mode = BuildVo | BuildVio | Vio2Vo
-let compilation_mode = ref BuildVo
-let compilation_output_name = ref None
-
-let batch_mode = ref false
-let set_batch_mode () =
-  System.trust_file_cache := false;
-  batch_mode := true
-
-let add_compile verbose s =
-  set_batch_mode ();
-  Flags.quiet := true;
-  if not !glob_opt then Dumpglob.dump_to_dotglob ();
-  (** make the file name explicit; needed not to break up Coq loadpath stuff. *)
-  let s =
-    let open Filename in
-    if is_implicit s
-    then concat current_dir_name s
-    else s
+(** Prints info which is either an error or an anomaly and then exits
+    with the appropriate error code *)
+let fatal_error msg =
+  Topfmt.std_logger Feedback.Error msg;
+  flush_all ();
+  exit 1
+
+let fatal_error_exn ?extra exn =
+  Topfmt.print_err_exn ?extra exn;
+  flush_all ();
+  let exit_code =
+    if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1
   in
-  compile_list := (verbose,s) :: !compile_list
+  exit exit_code
 
+(******************************************************************************)
+(* File Compilation                                                           *)
+(******************************************************************************)
 let warn_file_no_extension =
   CWarnings.create ~name:"file-no-extension" ~category:"filesystem"
          (fun (f,ext) ->
@@ -268,16 +173,11 @@ let ensure_ext ext f =
 let chop_extension f =
   try Filename.chop_extension f with _ -> f
 
-let compile_error msg =
-  Topfmt.std_logger Feedback.Error msg;
-  flush_all ();
-  exit 1
-
 let ensure_bname src tgt =
   let src, tgt = Filename.basename src, Filename.basename tgt in
   let src, tgt = chop_extension src, chop_extension tgt in
   if src <> tgt then
-    compile_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++
+    fatal_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++
                    str "Source: " ++ str src                                                ++ fnl () ++
                    str "Target: " ++ str tgt)
 
@@ -289,25 +189,23 @@ let ensure_vio v vio = ensure ".vio" v vio
 
 let ensure_exists f =
   if not (Sys.file_exists f) then
-    compile_error (hov 0 (str "Can't find file" ++ spc () ++ str f))
-
-let top_stm_options = ref Stm.AsyncOpts.default_opts
+    fatal_error (hov 0 (str "Can't find file" ++ spc () ++ str f))
 
 (* Compile a vernac file *)
-let compile ~time ~verbosely ~f_in ~f_out =
+let compile opts ~verbosely ~f_in ~f_out =
   let check_pending_proofs () =
     let pfs = Proof_global.get_all_proof_names () in
     if not (CList.is_empty pfs) then
-      compile_error (str "There are pending proofs: "
+      fatal_error (str "There are pending proofs: "
                     ++ (pfs
                         |> List.rev
                         |> prlist_with_sep pr_comma Names.Id.print)
                     ++ str ".")
   in
-  let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in
-  let require_libs = require_libs () in
-  let stm_options = !top_stm_options in
-  match !compilation_mode with
+  let iload_path = build_load_path opts in
+  let require_libs = require_libs opts in
+  let stm_options = opts.stm_flags in
+  match opts.compilation_mode with
   | BuildVo ->
       Flags.record_aux_file := true;
       let long_f_dot_v = ensure_v f_in in
@@ -319,12 +217,10 @@ let compile ~time ~verbosely ~f_in ~f_out =
 
       let doc, sid = Stm.(new_doc
           { doc_type = VoDoc long_f_dot_vo;
-            iload_path;
-            require_libs;
-            stm_options;
+            iload_path; require_libs; stm_options;
           }) in
 
-      let doc, sid = load_init_vernaculars ~time doc sid in
+      let doc, sid = load_init_vernaculars opts doc sid in
       let ldir = Stm.get_ldir ~doc in
       Aux_file.(start_aux_file
         ~aux_file:(aux_file_name_for long_f_dot_vo)
@@ -332,7 +228,7 @@ let compile ~time ~verbosely ~f_in ~f_out =
       Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
       let wall_clock1 = Unix.gettimeofday () in
-      let doc, _ = Vernac.load_vernac ~time ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
+      let doc, _ = Vernac.load_vernac ~time:opts.time ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
       let _doc = Stm.join ~doc in
       let wall_clock2 = Unix.gettimeofday () in
       check_pending_proofs ();
@@ -367,15 +263,13 @@ let compile ~time ~verbosely ~f_in ~f_out =
 
       let doc, sid = Stm.(new_doc
           { doc_type = VioDoc long_f_dot_vio;
-            iload_path;
-            require_libs;
-            stm_options;
+            iload_path; require_libs; stm_options;
           }) in
 
-      let doc, sid = load_init_vernaculars ~time doc sid in
+      let doc, sid = load_init_vernaculars opts doc sid in
 
       let ldir = Stm.get_ldir ~doc in
-      let doc, _ = Vernac.load_vernac ~time ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
+      let doc, _ = Vernac.load_vernac ~time:opts.time ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
       let doc = Stm.finish ~doc in
       check_pending_proofs ();
       let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in
@@ -390,91 +284,96 @@ let compile ~time ~verbosely ~f_in ~f_out =
       let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
       Library.save_library_raw lfdv sum lib univs proofs
 
-let compile ~time ~verbosely ~f_in ~f_out =
+let compile opts ~verbosely ~f_in ~f_out =
   ignore(CoqworkmgrApi.get 1);
-  compile ~time ~verbosely ~f_in ~f_out;
+  compile opts ~verbosely ~f_in ~f_out;
   CoqworkmgrApi.giveback 1
 
-let compile_file (verbosely,f_in) =
+let compile_file opts (f_in, verbosely) =
   if !Flags.beautify then
     Flags.with_option Flags.beautify_file
-      (fun f_in -> compile ~verbosely ~f_in ~f_out:None) f_in
+      (fun f_in -> compile opts ~verbosely ~f_in ~f_out:None) f_in
   else
-    compile ~verbosely ~f_in ~f_out:None
+    compile opts ~verbosely ~f_in ~f_out:None
 
-let compile_files ~time =
-  if !compile_list == [] then ()
-  else List.iter (compile_file ~time) (List.rev !compile_list)
+let compile_files opts =
+  let compile_list = List.rev opts.compile_list in
+  List.iter (compile_file opts) compile_list
 
 (******************************************************************************)
 (* VIO Dispatching                                                            *)
 (******************************************************************************)
-
-let vio_tasks = ref []
-let add_vio_task f =
-  set_batch_mode ();
-  Flags.quiet := true;
-  vio_tasks := f :: !vio_tasks
-
-let check_vio_tasks () =
+let check_vio_tasks opts =
   let rc =
     List.fold_left (fun acc t -> Vio_checking.check_vio t && acc)
-      true (List.rev !vio_tasks) in
-  if not rc then exit 1
+      true (List.rev opts.vio_tasks) in
+  if not rc then fatal_error Pp.(str "VIO Task Check failed")
 
 (* vio files *)
-let vio_files = ref []
-let vio_files_j = ref 0
-let vio_checking = ref false
-let add_vio_file f =
-  set_batch_mode ();
-  Flags.quiet := true;
-  vio_files := f :: !vio_files
-
-let set_vio_checking_j opt j =
-  try vio_files_j := int_of_string j
-  with Failure _ ->
-    prerr_endline ("The first argument of " ^ opt ^ " must the number");
-    prerr_endline "of concurrent workers to be used (a positive integer).";
-    prerr_endline "Makefiles generated by coq_makefile should be called";
-    prerr_endline "setting the J variable like in 'make vio2vo J=3'";
-    exit 1
-
-let schedule_vio () =
+let schedule_vio opts =
   (* We must add update the loadpath here as the scheduling process
      happens outside of the STM *)
-  let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in
+  let iload_path = build_load_path opts in
   List.iter Mltop.add_coq_path iload_path;
 
-  if !vio_checking then
-    Vio_checking.schedule_vio_checking !vio_files_j !vio_files
+  if opts.vio_checking then
+    Vio_checking.schedule_vio_checking opts.vio_files_j opts.vio_files
   else
-    Vio_checking.schedule_vio_compilation !vio_files_j !vio_files
+    Vio_checking.schedule_vio_compilation opts.vio_files_j opts.vio_files
 
 (******************************************************************************)
-(* UI Options                                                                 *)
+(* Color Options                                                              *)
 (******************************************************************************)
-(** Options for proof general *)
-
-let set_emacs () =
-  if not (Option.is_empty !toploop) then
-    user_err Pp.(str "Flag -emacs is incompatible with a custom toplevel loop");
-  Coqloop.print_emacs := true;
-  Printer.enable_goal_tags_printing := true;
-  color := `OFF
-
-(** Options for CoqIDE *)
-
-let set_ideslave () =
-  if !Coqloop.print_emacs then user_err Pp.(str "Flags -ideslave and -emacs are incompatible");
-  toploop := Some "coqidetop";
-  Flags.ide_slave := true
+let init_color color_mode =
+  let has_color = match color_mode with
+  | `OFF -> false
+  | `ON -> true
+  | `AUTO ->
+    Terminal.has_style Unix.stdout &&
+    Terminal.has_style Unix.stderr &&
+    (* emacs compilation buffer does not support colors by default,
+       its TERM variable is set to "dumb". *)
+    try Sys.getenv "TERM" <> "dumb" with Not_found -> false
+  in
+  if has_color then begin
+    let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in
+    match colors with
+    | None ->
+      (** Default colors *)
+      Topfmt.init_terminal_output ~color:true
+    | Some "" ->
+      (** No color output *)
+      Topfmt.init_terminal_output ~color:false
+    | Some s ->
+      (** Overwrite all colors *)
+      Topfmt.clear_styles ();
+      Topfmt.parse_color_config s;
+      Topfmt.init_terminal_output ~color:true
+  end
+  else
+    Topfmt.init_terminal_output ~color:false
 
-(** Options for slaves *)
+let toploop_init = ref begin fun opts x ->
+  let () = init_color opts.color in
+  let () = CoqworkmgrApi.init !WorkerLoop.async_proofs_worker_priority in
+  x
+  end
 
-let set_toploop name =
-  if !Coqloop.print_emacs then user_err Pp.(str "Flags -toploop and -emacs are incompatible");
-  toploop := Some name
+let print_style_tags opts =
+  let () = init_color opts.color in
+  let tags = Topfmt.dump_tags () in
+  let iter (t, st) =
+    let opt = Terminal.eval st ^ t ^ Terminal.reset ^ "\n" in
+    print_string opt
+  in
+  let make (t, st) =
+    let tags = List.map string_of_int (Terminal.repr st) in
+    (t ^ "=" ^ String.concat ";" tags)
+  in
+  let repr = List.map make tags in
+  let () = Printf.printf "COQ_COLORS=\"%s\"\n" (String.concat ":" repr) in
+  let () = List.iter iter tags in
+  flush_all ()
 
 (** GC tweaking *)
 
@@ -501,339 +400,37 @@ let init_gc () =
              Gc.minor_heap_size = 33554432; (** 4M *)
              Gc.space_overhead = 120}
 
-(*s Parsing of the command line.
-    We no longer use [Arg.parse], in order to use share [Usage.print_usage]
-    between coqtop and coqc. *)
-
-let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesystem"
-    (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned")
-
-exception NoCoqLib
-
-let usage batch =
-  begin
-    try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib)
-    with NoCoqLib -> usage_no_coqlib ()
-  end;
-  let lp = Coqinit.toplevel_init_load_path () in
-  (* Necessary for finding the toplevels below *)
-  List.iter Mltop.add_coq_path lp;
-  if batch then Usage.print_usage_coqc ()
-  else begin
-    Mltop.load_ml_objects_raw_rex
-      (Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$"));
-    Usage.print_usage_coqtop ()
-  end
-
-let print_style_tags () =
-  let () = init_color () in
-  let tags = Topfmt.dump_tags () in
-  let iter (t, st) =
-    let opt = Terminal.eval st ^ t ^ Terminal.reset ^ "\n" in
-    print_string opt
-  in
-  let make (t, st) =
-    let tags = List.map string_of_int (Terminal.repr st) in
-    (t ^ "=" ^ String.concat ";" tags)
-  in
-  let repr = List.map make tags in
-  let () = Printf.printf "COQ_COLORS=\"%s\"\n" (String.concat ":" repr) in
-  let () = List.iter iter tags in
-  flush_all ()
-
-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
-
-let filter_opts = ref false
-let exitcode () = if !filter_opts then 2 else 0
-
-let print_where = ref false
-let print_config = ref false
-let print_tags = ref false
-
-let get_priority opt s =
-  try CoqworkmgrApi.priority_of_string s
-  with Invalid_argument _ ->
-    prerr_endline ("Error: low/high expected after "^opt); exit 1
-
-let get_async_proofs_mode opt = let open Stm.AsyncOpts in function
-  | "no" | "off" -> APoff
-  | "yes" | "on" -> APon
-  | "lazy" -> APonLazy
-  | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1
-
-let get_cache opt = function
-  | "force" -> Some Stm.AsyncOpts.Force
-  | _ -> prerr_endline ("Error: force expected after "^opt); exit 1
-
-
-let set_worker_id opt s =
-  assert (s <> "master");
-  Flags.async_proofs_worker_id := s
-
-let get_bool opt = function
-  | "yes" | "on" -> true
-  | "no" | "off" -> false
-  | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1
-
-let get_int opt n =
-  try int_of_string n
-  with Failure _ ->
-    prerr_endline ("Error: integer expected after option "^opt); exit 1
-
-let get_float opt n =
-  try float_of_string n
-  with Failure _ ->
-    prerr_endline ("Error: float expected after option "^opt); exit 1
-
-let get_host_port opt s =
-  match CString.split ':' s with
-  | [host; portr; portw] ->
-       Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
-  | ["stdfds"] -> Some Spawned.AnonPipe
-  | _ ->
-     prerr_endline ("Error: host:portr:portw or stdfds expected after option "^opt);
-     exit 1
-
-let get_error_resilience opt = function
-  | "on" | "all" | "yes" -> `All
-  | "off" | "no" -> `None
-  | s -> `Only (CString.split ',' s)
-
-let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
-
-let is_not_dash_option = function
-  | Some f when String.length f > 0 && f.[0] <> '-' -> true
-  | _ -> false
-
-let get_native_name s =
-  (* We ignore even critical errors because this mode has to be super silent *)
-  try
-    String.concat "/" [Filename.dirname s;
-      Nativelib.output_dir; Library.native_name_from_filename s]
-  with _ -> ""
-
-(** Prints info which is either an error or an anomaly and then exits
-    with the appropriate error code *)
-let fatal_error ?extra exn =
-  Topfmt.print_err_exn ?extra exn;
-  let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in
-  exit exit_code
-
-let parse_args arglist =
-  let args = ref arglist in
-  let extras = ref [] in
-  let rec parse () = match !args with
-  | [] -> List.rev !extras
-  | opt :: rem ->
-    args := rem;
-    let next () = match !args with
-      | x::rem -> args := rem; x
-      | [] -> error_missing_arg opt
-    in
-    let peek_next () = match !args with
-      | x::_ -> Some x
-      | [] -> None
-    in
-    begin match opt with
-
-    (* Complex options with many args *)
-    |"-I"|"-include" ->
-      begin match rem with
-      | d :: rem -> Coqinit.push_ml_include d; args := rem
-      | [] -> error_missing_arg opt
-      end
-    |"-Q" ->
-      begin match rem with
-      | d :: p :: rem -> set_include d p false; args := rem
-      | _ -> error_missing_arg opt
-      end
-    |"-R" ->
-      begin match rem with
-      | d :: p :: rem -> set_include d p true; args := rem
-      | _ -> error_missing_arg opt
-      end
-
-    (* Options with two arg *)
-    |"-check-vio-tasks" ->
-        let tno = get_task_list (next ()) in
-        let tfile = next () in
-        add_vio_task (tno,tfile)
-    |"-schedule-vio-checking" ->
-        vio_checking := true;
-        set_vio_checking_j opt (next ());
-        add_vio_file (next ());
-        while is_not_dash_option (peek_next ()) do add_vio_file (next ()); done
-    |"-schedule-vio2vo" ->
-        set_vio_checking_j opt (next ());
-        add_vio_file (next ());
-        while is_not_dash_option (peek_next ()) do add_vio_file (next ()); done
-
-    (* Options with one arg *)
-    |"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ())
-    |"-async-proofs" ->
-      top_stm_options :=
-        { !top_stm_options with
-          Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next())
-        }
-    |"-async-proofs-j" ->
-      top_stm_options :=
-        { !top_stm_options with
-          Stm.AsyncOpts.async_proofs_n_workers = (get_int opt (next ()))
-        }
-    |"-async-proofs-cache" ->
-      top_stm_options :=
-        { !top_stm_options with
-          Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ())
-        }
-    |"-async-proofs-tac-j" ->
-      top_stm_options :=
-        { !top_stm_options with
-          Stm.AsyncOpts.async_proofs_n_tacworkers = (get_int opt (next ()))
-        }
-    |"-async-proofs-worker-priority" ->
-        WorkerLoop.async_proofs_worker_priority := get_priority opt (next ())
-    |"-async-proofs-private-flags" ->
-      top_stm_options :=
-        { !top_stm_options with
-          Stm.AsyncOpts.async_proofs_private_flags = Some (next ());
-        }
-    |"-async-proofs-tactic-error-resilience" ->
-      top_stm_options :=
-        { !top_stm_options with
-          Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ());
-        }
-    |"-async-proofs-command-error-resilience" ->
-      top_stm_options :=
-        { !top_stm_options with
-          Stm.AsyncOpts.async_proofs_cmd_error_resilience = get_bool opt (next ())
-        }
-    |"-async-proofs-delegation-threshold" ->
-      top_stm_options :=
-        { !top_stm_options with
-          Stm.AsyncOpts.async_proofs_delegation_threshold = get_float opt (next ())
-        }
-    |"-worker-id" -> set_worker_id opt (next ())
-    |"-compat" ->
-        let v = G_vernac.parse_compat_version ~allow_old:false (next ()) in
-        Flags.compat_version := v; add_compat_require v
-    |"-compile" -> add_compile false (next ())
-    |"-compile-verbose" -> add_compile true (next ())
-    |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true
-    |"-feedback-glob" -> Dumpglob.feedback_glob ()
-    |"-exclude-dir" -> System.exclude_directory (next ())
-    |"-init-file" -> Coqinit.set_rcfile (next ())
-    |"-inputstate"|"-is" -> set_inputstate (next ())
-    |"-load-ml-object" -> Mltop.dir_ml_load (next ())
-    |"-load-ml-source" -> Mltop.dir_ml_use (next ())
-    |"-load-vernac-object" -> add_require (next (), None, None)
-    |"-load-vernac-source"|"-l" -> add_load_vernacular false (next ())
-    |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ())
-    |"-outputstate" -> set_outputstate (next ())
-    |"-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 ())
-    |"-require" -> add_require (next (), None, Some false)
-    |"-top" -> set_toplevel_name (dirpath_of_string (next ()))
-    |"-main-channel" -> Spawned.main_channel := get_host_port opt (next())
-    |"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
-    |"-vio2vo" ->
-      add_compile false (next ());
-      compilation_mode := Vio2Vo
-    |"-toploop" -> set_toploop (next ())
-    |"-w" | "-W" ->
-      let w = next () in
-      if w = "none" then CWarnings.set_flags w
-      else
-        let w = CWarnings.get_flags () ^ "," ^ w in
-        CWarnings.set_flags (CWarnings.normalize_flags_string w)
-    |"-o" -> compilation_output_name := Some (next())
-
-    (* Options with zero arg *)
-    |"-async-queries-always-delegate"
-    |"-async-proofs-always-delegate"
-    |"-async-proofs-full" ->
-      top_stm_options :=
-        { !top_stm_options with
-          Stm.AsyncOpts.async_proofs_full = true;
-        }
-    |"-async-proofs-never-reopen-branch" ->
-      top_stm_options :=
-        { !top_stm_options with
-          Stm.AsyncOpts.async_proofs_never_reopen_branch = true;
-        }
-    |"-batch" -> set_batch_mode ()
-    |"-test-mode" -> Flags.test_mode := true
-    |"-beautify" -> Flags.beautify := true
-    |"-boot" -> Flags.boot := true; Coqinit.no_load_rc ()
-    |"-bt" -> Backtrace.record_backtrace true
-    |"-color" -> set_color (next ())
-    |"-config"|"--config" -> print_config := true
-    |"-debug" -> Coqinit.set_debug ()
-    |"-stm-debug" -> Stm.stm_debug := true
-    |"-emacs" -> set_emacs ()
-    |"-filteropts" -> filter_opts := true
-    |"-h"|"-H"|"-?"|"-help"|"--help" -> usage !batch_mode
-    |"-ideslave" -> set_ideslave ()
-    |"-impredicative-set" -> set_impredicative_set ()
-    |"-indices-matter" -> Indtypes.enforce_indices_matter ()
-    |"-m"|"--memory" -> memory_stat := true
-    |"-noinit"|"-nois" -> load_init := false
-    |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
-    |"-native-compiler" ->
-      if not Coq_config.native_compiler then
-        warning "Native compilation was disabled at configure time."
-      else Flags.output_native_objects := true
-    |"-output-context" -> output_context := true
-    |"-profile-ltac" -> Flags.profile_ltac := true
-    |"-q" -> Coqinit.no_load_rc ()
-    |"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false
-    |"-quick" -> compilation_mode := BuildVio
-    |"-list-tags" -> print_tags := true
-    |"-time" -> measure_time := true
-    |"-type-in-type" -> set_type_in_type ()
-    |"-unicode" -> add_require ("Utf8_core", None, Some false)
-    |"-v"|"--version" -> Usage.version (exitcode ())
-    |"-print-version"|"--print-version" -> Usage.machine_readable_version (exitcode ())
-    |"-where" -> print_where := true
-
-    (* Unknown option *)
-    | s -> extras := s :: !extras
-    end;
-    parse ()
-  in
-  try
-    parse ()
-  with any -> fatal_error any
-
+(** Main init routine *)
 let init_toplevel arglist =
   (* Coq's init process, phase 1:
-     - OCaml parameters, and basic structures and IO
+     OCaml parameters, basic structures, and IO
    *)
   CProfile.init_profile ();
   init_gc ();
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
   let init_feeder = Feedback.add_feeder coqtop_init_feed in
   Lib.init();
+
   (* Coq's init process, phase 2:
-     - Basic Coq environment, load-path, plugins.
+     Basic Coq environment, load-path, plugins.
    *)
   let res = begin
     try
-      let extras = parse_args arglist in
+      let opts,extras = parse_args arglist in
+      memory_stat := opts.memory_stat;
+
       (* If we have been spawned by the Spawn module, this has to be done
        * early since the master waits us to connect back *)
       Spawned.init_channels ();
       Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
-      if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ()));
-      if !print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode ()));
-      if !print_tags then (print_style_tags (); exit (exitcode ()));
-      if !filter_opts then (print_string (String.concat "\n" extras); exit 0);
+      if opts.print_where then (print_endline(Envars.coqlib ()); exit(exitcode opts));
+      if opts.print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode opts));
+      if opts.print_tags then (print_style_tags opts; exit (exitcode opts));
+      if opts.filter_opts then (print_string (String.concat "\n" extras); exit 0);
       let top_lp = Coqinit.toplevel_init_load_path () in
       List.iter Mltop.add_coq_path top_lp;
-      Option.iter Mltop.load_ml_object_raw !toploop;
-      let extras = !toploop_init extras in
+      Option.iter Mltop.load_ml_object_raw opts.toploop;
+      let extras = !toploop_init 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";
@@ -841,10 +438,10 @@ let init_toplevel arglist =
       end;
       Flags.if_verbose print_header ();
       Mltop.init_known_plugins ();
-      engage ();
+      Global.set_engagement opts.impredicative_set;
 
       (* Allow the user to load an arbitrary state here *)
-      inputstate ();
+      inputstate opts;
 
       (* This state will be shared by all the documents *)
       Stm.init_core ();
@@ -853,9 +450,7 @@ let init_toplevel arglist =
 
          It is essential that the module system is in a consistent
          state before we take the first snapshot. This was not
-         guaranteed in the past. In particular, we want to be sure we
-         have called start_library before loading the prelude and rest
-         of required files.
+         guaranteed in the past, but now is thanks to the STM API.
 
          We split the codepath here depending whether coqtop is called
          in interactive mode or not.  *)
@@ -863,39 +458,37 @@ let init_toplevel arglist =
       (* The condition for starting the interactive mode is a bit
          convoluted, we should really refactor batch/compilation_mode
          more. *)
-      if (not !batch_mode
-          || CList.(is_empty !compile_list && is_empty !vio_files && is_empty !vio_tasks))
+      if (not opts.batch_mode
+          || CList.(is_empty opts.compile_list && is_empty opts.vio_files && is_empty opts.vio_tasks))
       (* Interactive *)
       then begin
-        let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in
-        let require_libs = require_libs () in
-        let stm_options = !top_stm_options in
-        try
-          let doc, sid = Stm.(new_doc
-                                { doc_type = Interactive !toplevel_name;
-                                  iload_path;
-                                  require_libs;
-                                  stm_options;
-                                }) in
-          Some (load_init_vernaculars ~time:!measure_time doc sid)
-        with any -> flush_all(); fatal_error any
-      (* Non interactive *)
+        let iload_path = build_load_path opts in
+        let require_libs = require_libs opts in
+        let stm_options = opts.stm_flags in
+        try let doc, sid =
+              Stm.(new_doc
+                     { doc_type = Interactive opts.toplevel_name;
+                       iload_path; require_libs; stm_options;
+                     }) in
+          Some (load_init_vernaculars opts doc sid), opts
+        with any -> flush_all(); fatal_error_exn any
+      (* Non interactive: we perform a sequence of compilation steps *)
       end else begin
         try
-          compile_files ~time:!measure_time;
+          compile_files opts;
           (* Vio compile pass *)
-          if !vio_files <> [] then schedule_vio ();
+          if opts.vio_files <> [] then schedule_vio opts;
           (* Vio task pass *)
-          check_vio_tasks ();
+          check_vio_tasks opts;
           (* Allow the user to output an arbitrary state *)
-          outputstate ();
-          None
-        with any -> flush_all(); fatal_error any
+          outputstate opts;
+          None, opts
+        with any -> flush_all(); fatal_error_exn any
       end;
     with any ->
       flush_all();
       let extra = Some (str "Error during initialization: ") in
-      fatal_error ?extra any
+      fatal_error_exn ?extra any
   end in
   Feedback.del_feeder init_feeder;
   res
@@ -903,12 +496,12 @@ let init_toplevel arglist =
 let start () =
   match init_toplevel (List.tl (Array.to_list Sys.argv)) with
   (* Batch mode *)
-  | Some (doc, sid) when not !batch_mode ->
-    !toploop_run doc;
+  | Some (doc, sid), opts when not opts.batch_mode ->
+    !toploop_run opts doc;
     exit 1
-  | _ ->
+  | _ , opts ->
     flush_all();
-    if !output_context then begin
+    if opts.output_context then begin
       let sigma, env = Pfedit.get_current_context () in
       Feedback.msg_notice (Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ())
     end;
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 5b9494eaa..4d625a03d 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -11,7 +11,7 @@
    state, load the files given on the command line, load the resource file,
    produce the output state if any, and finally will launch [Coqloop.loop]. *)
 
-val init_toplevel : string list -> (Stm.doc * Stateid.t) option
+val init_toplevel : string list -> (Stm.doc * Stateid.t) option * Coqargs.coq_cmdopts
 
 val start : unit -> unit
 
@@ -19,6 +19,6 @@ val start : unit -> unit
 val drop_last_doc : Stm.doc option ref
 
 (* For other toploops *)
-val toploop_init : (string list -> string list) ref
-val toploop_run : (Stm.doc -> unit) ref
+val toploop_init : (Coqargs.coq_cmdopts -> string list -> string list) ref
+val toploop_run : (Coqargs.coq_cmdopts -> Stm.doc -> unit) ref
 
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 10bf48647..9fb2e33d7 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -2,4 +2,5 @@ Vernac
 Usage
 Coqloop
 Coqinit
+Coqargs
 Coqtop