[toplevel] Refactor command line argument handling.

We mostly separate command line argument parsing from interpretation,
some (minor) imperative actions are still done at argument parsing
time. This tidies up the code quite a bit and allows to better follow
the complicated command line handling code.

To this effect, we group the key actions to be performed by the
toplevel into a new record type. There is still room to improve.

1 files changed, 575 insertions, 0 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