diff options
Diffstat (limited to 'toplevel/coqargs.ml')
| -rw-r--r-- | toplevel/coqargs.ml | 154 |
1 files changed, 14 insertions, 140 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index f822c68843..74c016101a 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -31,10 +31,9 @@ let set_type_in_type () = (******************************************************************************) -type compilation_mode = BuildVo | BuildVio | Vio2Vo type color = [`ON | `AUTO | `OFF] -type coq_cmdopts = { +type t = { load_init : bool; load_rcfile : bool; @@ -45,21 +44,10 @@ type coq_cmdopts = { 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 : Stm.interactive_top; - 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; + batch : bool; color : color; @@ -67,6 +55,7 @@ type coq_cmdopts = { indices_matter : bool; enable_VM : bool; enable_native_compiler : bool; + stm_flags : Stm.AsyncOpts.stm_opt; debug : bool; diffs_set : bool; @@ -85,13 +74,12 @@ type coq_cmdopts = { print_emacs : bool; inputstate : string option; - outputstate : string option; } let default_toplevel = Names.(DirPath.make [Id.of_string "Top"]) -let default_opts = { +let default = { load_init = true; load_rcfile = true; @@ -101,20 +89,10 @@ let default_opts = { vo_includes = []; vo_requires = []; - batch_mode = false; - compilation_mode = BuildVo; - toplevel_name = Stm.TopLogical default_toplevel; - compile_list = []; - compilation_output_name = None; - load_vernacular_list = []; - - vio_checking = false; - vio_tasks = []; - vio_files = []; - vio_files_j = 0; + batch = false; color = `AUTO; @@ -142,7 +120,6 @@ let default_opts = { (* Quiet / verbosity options should be here *) inputstate = None; - outputstate = None; } (******************************************************************************) @@ -168,44 +145,9 @@ let add_compat_require opts v = | Flags.V8_9 -> add_vo_require opts "Coq.Compat.Coq89" None (Some false) | Flags.Current -> add_vo_require opts "Coq.Compat.Coq810" None (Some false) -let set_batch_mode opts = - (* XXX: This should be in the argument record *) - Flags.quiet := true; - System.trust_file_cache := true; - { 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 = Printer.enable_goal_tags_printing := true; @@ -225,22 +167,11 @@ 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 @@ -285,16 +216,6 @@ 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 @@ -311,7 +232,7 @@ let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesy exception NoCoqLib -let usage batch = +let usage help = begin try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib) with NoCoqLib -> usage_no_coqlib () @@ -319,18 +240,10 @@ let usage batch = 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 Usage.print_usage_coqtop () - -let deprecated_coqc_warning = CWarnings.(create - ~name:"deprecate-compile-arg" - ~category:"toplevel" - ~default:Enabled - (fun opt_name -> Pp.(seq [str "The option "; str opt_name; str" is deprecated, please use coqc."]))) + help () (* Main parsing routine *) -let parse_args init_opts arglist : coq_cmdopts * string list = +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 @@ -342,10 +255,6 @@ let parse_args init_opts arglist : coq_cmdopts * string list = | 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 *) @@ -371,23 +280,6 @@ let parse_args init_opts arglist : coq_cmdopts * string list = | _ -> 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" -> Envars.set_user_coqlib (next ()); @@ -442,14 +334,6 @@ let parse_args init_opts arglist : coq_cmdopts * string list = Flags.compat_version := v; add_compat_require oval v - |"-compile" as opt -> - deprecated_coqc_warning opt; - add_compile oval false (next ()) - - |"-compile-verbose" as opt -> - deprecated_coqc_warning opt; - add_compile oval true (next ()) - |"-dump-glob" -> Dumpglob.dump_into_file (next ()); { oval with glob_opt = true } @@ -466,9 +350,6 @@ let parse_args init_opts arglist : coq_cmdopts * string list = |"-inputstate"|"-is" -> set_inputstate oval (next ()) - |"-outputstate" -> - set_outputstate oval (next ()) - |"-load-ml-object" -> Mltop.dir_ml_load (next ()); oval @@ -514,10 +395,6 @@ let parse_args init_opts arglist : coq_cmdopts * string list = |"-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 } - |"-w" | "-W" -> let w = next () in if w = "none" then @@ -527,10 +404,6 @@ let parse_args init_opts arglist : coq_cmdopts * string list = CWarnings.set_flags (CWarnings.normalize_flags_string w); oval - |"-o" as opt -> - deprecated_coqc_warning opt; - { oval with compilation_output_name = Some (next()) } - |"-bytecode-compiler" -> { oval with enable_VM = get_bool opt (next ()) } @@ -558,7 +431,9 @@ let parse_args init_opts arglist : coq_cmdopts * string list = { oval with stm_flags = { oval.stm_flags with Stm.AsyncOpts.async_proofs_never_reopen_branch = true }} - |"-batch" -> set_batch_mode oval + |"-batch" -> + Flags.quiet := true; + { oval with batch = true } |"-test-mode" -> Flags.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval |"-boot" -> Flags.boot := true; { oval with load_rcfile = false; } @@ -588,13 +463,12 @@ let parse_args init_opts arglist : coq_cmdopts * string list = 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 + |"-h"|"-H"|"-?"|"-help"|"--help" -> usage help; oval |"-v"|"--version" -> Usage.version (exitcode oval) |"-print-version"|"--print-version" -> Usage.machine_readable_version (exitcode oval) @@ -607,13 +481,13 @@ let parse_args init_opts arglist : coq_cmdopts * string list = parse noval in try - parse init_opts + parse init with any -> fatal_error any (******************************************************************************) (* Startup LoadPath and Modules *) (******************************************************************************) -(* prelude_data == From Coq Require Export Prelude. *) +(* prelude_data == From Coq Require Import Prelude. *) let prelude_data = "Prelude", Some "Coq", Some false let require_libs opts = |