From c6e2e57b8211dfc5bdaaa02592f8ae8bbad1d770 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 8 May 2019 12:53:04 +0200 Subject: Toplevel: structuring source code. --- toplevel/ccompile.ml | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index e6255a947e..605db74836 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -20,6 +20,16 @@ let fatal_error msg = (******************************************************************************) (* Interactive Load File Simulation *) (******************************************************************************) + +let load_init_file opts ~state = + if opts.load_rcfile then + Topfmt.(in_phase ~phase:LoadingRcFile) (fun () -> + Coqinit.load_rcfile ~rcfile:opts.rcfile ~state) () + else begin + Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); + state + end + let load_vernacular opts ~state = List.fold_left (fun state (f_in, echo) -> @@ -32,16 +42,9 @@ let load_vernacular opts ~state = ) state (List.rev opts.load_vernacular_list) let load_init_vernaculars opts ~state = - let state = - if opts.load_rcfile then - Topfmt.(in_phase ~phase:LoadingRcFile) (fun () -> - Coqinit.load_rcfile ~rcfile:opts.rcfile ~state) () - else begin - Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); - state - end in - - load_vernacular opts ~state + let state = load_init_file opts ~state in + let state = load_vernacular opts ~state in + state (******************************************************************************) (* File Compilation *) -- cgit v1.2.3 From 5f3777e9ca29493a242b66f92ba803fa5760a634 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 8 May 2019 13:02:56 +0200 Subject: Toplevel: structuring init_toplevel. --- toplevel/coqtop.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index e43e6a8da4..170959f2e2 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -257,8 +257,7 @@ type custom_toplevel = ; opts : Coqargs.t } - -let init_toploop opts = +let init_document opts = let iload_path = build_load_path opts in let require_libs = require_libs opts in let stm_options = opts.stm_flags in @@ -268,8 +267,12 @@ let init_toploop opts = { doc_type = Interactive opts.toplevel_name; iload_path; require_libs; stm_options; }) in - let state = { doc; sid; proof = None; time = opts.time } in - Ccompile.load_init_vernaculars opts ~state, opts + { doc; sid; proof = None; time = opts.time } + +let init_toploop opts = + let state = init_document opts in + let state = Ccompile.load_init_vernaculars opts ~state in + state let coqtop_init ~opts extra = init_color opts; @@ -297,7 +300,7 @@ let start_coq custom = prerr_endline "See -help for the list of supported options"; exit 1 end; - init_toploop opts + init_toploop opts, opts with any -> flush_all(); fatal_error_exn any in -- cgit v1.2.3 From fe5389542af2d9b6e8d964bbc2c10e997af409fe Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 8 May 2019 13:22:34 +0200 Subject: A classification of command line options. A few semantic changes: - several queries (-where, -config, ...) are accepted - queries are exclusive of other arguments - option -filterops is exclusive of other arguments if it contains another query (this allows to get rid of the "exitcode" hack) --- toplevel/ccompile.ml | 14 +-- toplevel/coqargs.ml | 297 ++++++++++++++++++++++++++++++--------------------- toplevel/coqargs.mli | 75 ++++++++----- toplevel/coqc.ml | 6 +- toplevel/coqloop.ml | 2 +- toplevel/coqtop.ml | 102 ++++++++++-------- toplevel/coqtop.mli | 2 +- toplevel/usage.ml | 11 +- toplevel/usage.mli | 6 +- 9 files changed, 297 insertions(+), 218 deletions(-) diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 605db74836..d8a3dbb4bb 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -22,9 +22,9 @@ let fatal_error msg = (******************************************************************************) let load_init_file opts ~state = - if opts.load_rcfile then + if opts.pre.load_rcfile then Topfmt.(in_phase ~phase:LoadingRcFile) (fun () -> - Coqinit.load_rcfile ~rcfile:opts.rcfile ~state) () + Coqinit.load_rcfile ~rcfile:opts.config.rcfile ~state) () else begin Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); state @@ -39,7 +39,7 @@ let load_vernacular opts ~state = if !Flags.beautify then Flags.with_option Flags.beautify_file load_vernac f_in else load_vernac s - ) state (List.rev opts.load_vernacular_list) + ) state (List.rev opts.pre.load_vernacular_list) let load_init_vernaculars opts ~state = let state = load_init_file opts ~state in @@ -102,8 +102,8 @@ let compile opts copts ~echo ~f_in ~f_out = in let iload_path = build_load_path opts in let require_libs = require_libs opts in - let stm_options = opts.stm_flags in - let output_native_objects = match opts.native_compiler with + let stm_options = opts.config.stm_flags in + let output_native_objects = match opts.config.native_compiler with | NativeOff -> false | NativeOn {ondemand} -> not ondemand in match copts.compilation_mode with @@ -118,7 +118,7 @@ let compile opts copts ~echo ~f_in ~f_out = Stm.{ doc_type = VoDoc long_f_dot_vo; iload_path; require_libs; stm_options; } in - let state = { doc; sid; proof = None; time = opts.time } in + let state = { doc; sid; proof = None; time = opts.config.time } in let state = load_init_vernaculars opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in Aux_file.(start_aux_file @@ -164,7 +164,7 @@ let compile opts copts ~echo ~f_in ~f_out = iload_path; require_libs; stm_options; } in - let state = { doc; sid; proof = None; time = opts.time } in + let state = { doc; sid; proof = None; time = opts.config.time } in let state = load_init_vernaculars opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 7e3759f177..e47fbf2921 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -40,52 +40,70 @@ type native_compiler = NativeOff | NativeOn of { ondemand : bool } type option_command = OptionSet of string option | OptionUnset -type t = { +type coqargs_logic_config = { + impredicative_set : Declarations.set_predicativity; + indices_matter : bool; + toplevel_name : Stm.interactive_top; + allow_sprop : bool; + cumulative_sprop : bool; +} +type coqargs_config = { + logic : coqargs_logic_config; + rcfile : string option; + coqlib : string option; + color : color; + enable_VM : bool; + native_compiler : native_compiler; + stm_flags : Stm.AsyncOpts.stm_opt; + debug : bool; + diffs_set : bool; + time : bool; + glob_opt : bool; + print_emacs : bool; + set_options : (Goptions.option_name * option_command) list; +} + +type coqargs_pre = { load_init : bool; load_rcfile : bool; - rcfile : string option; ml_includes : Loadpath.coq_path list; vo_includes : Loadpath.coq_path list; vo_requires : (string * string option * bool option) list; (* None = No Import; Some false = Import; Some true = Export *) - toplevel_name : Stm.interactive_top; - load_vernacular_list : (string * bool) list; - batch : bool; - color : color; + inputstate : string option; +} - impredicative_set : Declarations.set_predicativity; - indices_matter : bool; - enable_VM : bool; - native_compiler : native_compiler; - allow_sprop : bool; - cumulative_sprop : bool; +type coqargs_base_query = + | PrintTags | PrintWhere | PrintConfig + | PrintVersion | PrintMachineReadableVersion + | PrintHelp of (unit -> unit) - set_options : (Goptions.option_name * option_command) list; - - stm_flags : Stm.AsyncOpts.stm_opt; - debug : bool; - diffs_set : bool; - time : bool; +type coqargs_queries = { + queries : coqargs_base_query list; + filteropts : bool; +} - filter_opts : bool; +type coqargs_interactive = Interactive | Batch - glob_opt : bool; +type coqargs_main = + | Queries of coqargs_queries + | Run of coqargs_interactive +type coqargs_post = { memory_stat : bool; - print_tags : bool; - print_where : bool; - print_config: bool; output_context : bool; +} - print_emacs : bool; - - inputstate : string option; - +type t = { + config : coqargs_config; + pre : coqargs_pre; + main : coqargs_main; + post : coqargs_post; } let default_toplevel = Names.(DirPath.make [Id.of_string "Top"]) @@ -95,69 +113,77 @@ let default_native = then NativeOn {ondemand=true} else NativeOff -let default = { - - load_init = true; - load_rcfile = true; - rcfile = None; - - ml_includes = []; - vo_includes = []; - vo_requires = []; - - toplevel_name = Stm.TopLogical default_toplevel; - - load_vernacular_list = []; - batch = false; - - color = `AUTO; - +let default_logic_config = { impredicative_set = Declarations.PredicativeSet; indices_matter = false; - enable_VM = true; - native_compiler = default_native; + toplevel_name = Stm.TopLogical default_toplevel; allow_sprop = false; cumulative_sprop = false; +} - set_options = []; - +let default_config = { + logic = default_logic_config; + rcfile = None; + coqlib = None; + color = `AUTO; + enable_VM = true; + native_compiler = default_native; stm_flags = Stm.AsyncOpts.default_opts; debug = false; diffs_set = false; time = false; + glob_opt = false; + print_emacs = false; + set_options = []; + + (* Quiet / verbosity options should be here *) +} - filter_opts = false; +let default_pre = { + load_init = true; + load_rcfile = true; + ml_includes = []; + vo_includes = []; + vo_requires = []; + load_vernacular_list = []; + inputstate = None; +} - glob_opt = false; +let default_queries = { + queries = []; + filteropts = false; +} +let default_main = + Run Interactive + +let default_post = { memory_stat = false; - print_tags = false; - print_where = false; - print_config = false; output_context = false; +} - print_emacs = false; - - (* Quiet / verbosity options should be here *) - - inputstate = None; +let default = { + config = default_config; + pre = default_pre; + main = default_main; + post = default_post; } (******************************************************************************) (* Functional arguments *) (******************************************************************************) let add_ml_include opts s = - Loadpath.{ opts with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.ml_includes } + Loadpath.{ opts with pre = { opts.pre with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.pre.ml_includes }} let add_vo_include opts unix_path coq_path implicit = let open Loadpath in let coq_path = Libnames.dirpath_of_string coq_path in - { opts with vo_includes = { + { opts with pre = { opts.pre with vo_includes = { recursive = true; - path_spec = VoPath { unix_path; coq_path; has_ml = AddNoML; implicit } } :: opts.vo_includes } + path_spec = VoPath { unix_path; coq_path; has_ml = AddNoML; implicit } } :: opts.pre.vo_includes }} let add_vo_require opts d p export = - { opts with vo_requires = (d, p, export) :: opts.vo_requires } + { opts with pre = { opts.pre with vo_requires = (d, p, export) :: opts.pre.vo_requires }} let add_compat_require opts v = match v with @@ -166,19 +192,45 @@ let add_compat_require opts v = | Flags.Current -> add_vo_require opts "Coq.Compat.Coq810" None (Some false) let add_load_vernacular opts verb s = - { opts with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.load_vernacular_list } + { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }} (** Options for proof general *) let set_emacs opts = Printer.enable_goal_tags_printing := true; - { opts with color = `EMACS; print_emacs = true } + { opts with config = { opts.config with color = `OFF; print_emacs = true }} + +let set_logic f oval = + { oval with config = { oval.config with logic = f oval.config.logic }} let set_color opts = function -| "yes" | "on" -> { opts with color = `ON } -| "no" | "off" -> { opts with color = `OFF } -| "auto" -> { opts with color = `AUTO } -| _ -> - error_wrong_arg ("Error: on/off/auto expected after option color") + | "yes" | "on" -> { opts with config = { opts.config with color = `ON }} + | "no" | "off" -> { opts with config = { opts.config with color = `OFF }} + | "auto" -> { opts with config = { opts.config with color = `AUTO }} + | _ -> + error_wrong_arg ("Error: on/off/auto expected after option color") + +let set_batch opts = + { opts with main = match opts.main with + | Run _ -> Run Batch + | Queries _ as x -> x } + +let add_query { queries; filteropts } q = + { queries = queries@[q]; filteropts } + +let set_query opts q = + { opts with main = match opts.main with + | Run _ -> Queries (add_query default_queries q) + | Queries queries -> Queries (add_query queries q) + } + +let add_filteropts { queries } = + { queries; filteropts = true } + +let set_filteropts opts = + { opts with main = match opts.main with + | Run _ -> Queries (add_filteropts default_queries) + | Queries queries -> Queries (add_filteropts queries) + } let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" @@ -190,9 +242,7 @@ let warn_deprecated_simple_require = let set_inputstate opts s = warn_deprecated_inputstate (); - { opts with inputstate = Some s } - -let exitcode opts = if opts.filter_opts then 2 else 0 + { opts with pre = { opts.pre with inputstate = Some s }} (******************************************************************************) (* Parsing helpers *) @@ -320,54 +370,54 @@ let parse_args ~help ~init arglist : t * string list = (* Options with one arg *) |"-coqlib" -> - Envars.set_user_coqlib (next ()); - oval + { oval with config = { oval.config with coqlib = Some (next ()) + }} |"-async-proofs" -> - { oval with stm_flags = { oval.stm_flags with + { oval with config = { oval.config with stm_flags = { oval.config.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 + { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with Stm.AsyncOpts.async_proofs_n_workers = (get_int opt (next ())) - }} + }}} |"-async-proofs-cache" -> - { oval with stm_flags = { oval.stm_flags with + { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ()) - }} + }}} |"-async-proofs-tac-j" -> let j = get_int opt (next ()) in if j <= 0 then begin error_wrong_arg ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1") end; - { oval with stm_flags = { oval.stm_flags with + { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with Stm.AsyncOpts.async_proofs_n_tacworkers = j - }} + }}} |"-async-proofs-worker-priority" -> CoqworkmgrApi.async_proofs_worker_priority := get_priority opt (next ()); oval |"-async-proofs-private-flags" -> - { oval with stm_flags = { oval.stm_flags with + { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with Stm.AsyncOpts.async_proofs_private_flags = Some (next ()); - }} + }}} |"-async-proofs-tactic-error-resilience" -> - { oval with stm_flags = { oval.stm_flags with + { oval with config = { oval.config with stm_flags = { oval.config.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 + { oval with config = { oval.config with stm_flags = { oval.config.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 + { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with Stm.AsyncOpts.async_proofs_delegation_threshold = get_float opt (next ()) - }} + }}} |"-worker-id" -> set_worker_id opt (next ()); oval @@ -378,7 +428,7 @@ let parse_args ~help ~init arglist : t * string list = |"-dump-glob" -> Dumpglob.dump_into_file (next ()); - { oval with glob_opt = true } + { oval with config = { oval.config with glob_opt = true }} |"-feedback-glob" -> Dumpglob.feedback_glob (); oval @@ -387,7 +437,7 @@ let parse_args ~help ~init arglist : t * string list = System.exclude_directory (next ()); oval |"-init-file" -> - { oval with rcfile = Some (next ()); } + { oval with config = { oval.config with rcfile = Some (next ()); }} |"-inputstate"|"-is" -> set_inputstate oval (next ()) @@ -441,10 +491,10 @@ let parse_args ~help ~init arglist : t * string list = 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 = Stm.TopLogical topname } + { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = Stm.TopLogical topname }}} |"-topfile" -> - { oval with toplevel_name = Stm.TopPhysical (next()) } + { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = Stm.TopPhysical (next()) }}} |"-main-channel" -> Spawned.main_channel := get_host_port opt (next()); oval @@ -462,7 +512,7 @@ let parse_args ~help ~init arglist : t * string list = oval |"-bytecode-compiler" -> - { oval with enable_VM = get_bool opt (next ()) } + { oval with config = { oval.config with enable_VM = get_bool opt (next ()) }} |"-native-compiler" -> @@ -479,68 +529,67 @@ let parse_args ~help ~init arglist : t * string list = | _ -> error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") in - { oval with native_compiler } + { oval with config = { oval.config with native_compiler }} | "-set" -> let opt = next() in let opt, v = parse_option_set opt in - { oval with set_options = (opt, OptionSet v) :: oval.set_options } + { oval with config = { oval.config with set_options = (opt, OptionSet v) :: oval.config.set_options }} | "-unset" -> let opt = next() in let opt = to_opt_key opt in - { oval with set_options = (opt, OptionUnset) :: oval.set_options } + { oval with config = { oval.config with set_options = (opt, OptionUnset) :: oval.config.set_options }} (* Options with zero arg *) |"-async-queries-always-delegate" |"-async-proofs-always-delegate" |"-async-proofs-never-reopen-branch" -> - { oval with stm_flags = { oval.stm_flags with + { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with Stm.AsyncOpts.async_proofs_never_reopen_branch = true - }} + }}} |"-batch" -> Flags.quiet := true; - { oval with batch = true } + set_batch oval |"-test-mode" -> Vernacentries.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval |"-bt" -> Backtrace.record_backtrace true; oval |"-color" -> set_color oval (next ()) - |"-config"|"--config" -> { oval with print_config = true } + |"-config"|"--config" -> set_query oval PrintConfig |"-debug" -> Coqinit.set_debug (); oval |"-diffs" -> let opt = next () in if List.exists (fun x -> opt = x) ["off"; "on"; "removed"] then Proof_diffs.write_diffs_option opt else error_wrong_arg "Error: on|off|removed expected after -diffs"; - { oval with diffs_set = true } + { oval with config = { oval.config with diffs_set = true }} |"-stm-debug" -> Stm.stm_debug := true; oval |"-emacs" -> set_emacs oval - |"-filteropts" -> { oval with filter_opts = true } + |"-filteropts" -> set_filteropts oval |"-impredicative-set" -> - { oval with impredicative_set = Declarations.ImpredicativeSet } - |"-allow-sprop" -> { oval with allow_sprop = true } - |"-disallow-sprop" -> { oval with allow_sprop = false } - |"-sprop-cumulative" -> { oval with cumulative_sprop = true } - |"-indices-matter" -> { oval with indices_matter = true } - |"-m"|"--memory" -> { oval with memory_stat = true } - |"-noinit"|"-nois" -> { oval with load_init = false } - |"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with glob_opt = true } - |"-output-context" -> { oval with output_context = true } + set_logic (fun o -> { o with impredicative_set = Declarations.ImpredicativeSet }) oval + |"-allow-sprop" -> set_logic (fun o -> { o with allow_sprop = true }) oval + |"-disallow-sprop" -> set_logic (fun o -> { o with allow_sprop = false }) oval + |"-sprop-cumulative" -> set_logic (fun o -> { o with cumulative_sprop = true }) oval + |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval + |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }} + |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }} + |"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with config = { oval.config with glob_opt = true }} + |"-output-context" -> { oval with post = { oval.post with output_context = true }} |"-profile-ltac" -> Flags.profile_ltac := true; oval - |"-q" -> { oval with load_rcfile = false; } + |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }} |"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false; oval - |"-list-tags" -> { oval with print_tags = true } - |"-time" -> { oval with time = true } + |"-list-tags" -> set_query oval PrintTags + |"-time" -> { oval with config = { oval.config with time = true }} |"-type-in-type" -> set_type_in_type (); oval |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) - |"-where" -> { oval with print_where = true } - |"-h"|"-H"|"-?"|"-help"|"--help" -> usage help; oval - |"-v"|"--version" -> Usage.version (exitcode oval) - |"-print-version"|"--print-version" -> - Usage.machine_readable_version (exitcode oval) + |"-where" -> set_query oval PrintWhere + |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp (fun () -> usage help)) + |"-v"|"--version" -> set_query oval PrintVersion + |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion (* Unknown option *) | s -> @@ -560,11 +609,11 @@ let parse_args ~help ~init arglist : t * string list = let prelude_data = "Prelude", Some "Coq", Some false let require_libs opts = - if opts.load_init then prelude_data :: opts.vo_requires else opts.vo_requires + if opts.pre.load_init then prelude_data :: opts.pre.vo_requires else opts.pre.vo_requires let cmdline_load_path opts = - List.rev opts.vo_includes @ List.(rev opts.ml_includes) + List.rev opts.pre.vo_includes @ List.(rev opts.pre.ml_includes) let build_load_path opts = - Coqinit.libs_init_load_path ~load_init:opts.load_init @ + Coqinit.libs_init_load_path ~load_init:opts.pre.load_init @ cmdline_load_path opts diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index 81f8983e98..897885997c 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -16,57 +16,76 @@ type native_compiler = NativeOff | NativeOn of { ondemand : bool } type option_command = OptionSet of string option | OptionUnset -type t = { +type coqargs_logic_config = { + impredicative_set : Declarations.set_predicativity; + indices_matter : bool; + toplevel_name : Stm.interactive_top; + allow_sprop : bool; + cumulative_sprop : bool; +} +type coqargs_config = { + logic : coqargs_logic_config; + rcfile : string option; + coqlib : string option; + color : color; + enable_VM : bool; + native_compiler : native_compiler; + stm_flags : Stm.AsyncOpts.stm_opt; + debug : bool; + diffs_set : bool; + time : bool; + glob_opt : bool; + print_emacs : bool; + set_options : (Goptions.option_name * option_command) list; +} + +type coqargs_pre = { load_init : bool; load_rcfile : bool; - rcfile : string option; ml_includes : Loadpath.coq_path list; vo_includes : Loadpath.coq_path list; vo_requires : (string * string option * bool option) list; - - toplevel_name : Stm.interactive_top; + (* None = No Import; Some false = Import; Some true = Export *) load_vernacular_list : (string * bool) list; - batch : bool; - - color : color; + inputstate : string option; +} - impredicative_set : Declarations.set_predicativity; - indices_matter : bool; - enable_VM : bool; - native_compiler : native_compiler; - allow_sprop : bool; - cumulative_sprop : bool; +type coqargs_base_query = + | PrintTags | PrintWhere | PrintConfig + | PrintVersion | PrintMachineReadableVersion + | PrintHelp of (unit -> unit) - set_options : (Goptions.option_name * option_command) list; - - stm_flags : Stm.AsyncOpts.stm_opt; - debug : bool; - diffs_set : bool; - time : bool; +type coqargs_queries = { + queries : coqargs_base_query list; + filteropts : bool; +} - filter_opts : bool; +type coqargs_interactive = Interactive | Batch - glob_opt : bool; +type coqargs_main = + | Queries of coqargs_queries + | Run of coqargs_interactive +type coqargs_post = { memory_stat : bool; - print_tags : bool; - print_where : bool; - print_config: bool; output_context : bool; +} - print_emacs : bool; - - inputstate : string option; +type t = { + config : coqargs_config; + pre : coqargs_pre; + main : coqargs_main; + post : coqargs_post; } (* Default options *) val default : t val parse_args : help:(unit -> unit) -> init:t -> string list -> t * string list -val exitcode : t -> int +val error_wrong_arg : string -> unit val require_libs : t -> (string * string option * bool option) list val build_load_path : t -> Loadpath.coq_path list diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index a04552e8db..7c4aded5bb 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -28,11 +28,11 @@ let coqc_main () = in let opts, extras = Topfmt.(in_phase ~phase:Initialization) - Coqtop.(init_toplevel ~help:Usage.print_usage_coqc ~init:Coqargs.default coqc_init) List.(tl (Array.to_list Sys.argv)) in + Coqtop.(init_batch_toplevel ~help:Usage.print_usage_coqc ~init:Coqargs.default coqc_init) List.(tl (Array.to_list Sys.argv)) in let copts = Coqcargs.parse extras in - if not opts.Coqargs.glob_opt then Dumpglob.dump_to_dotglob (); + if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob (); Topfmt.(in_phase ~phase:CompilationPhase) Ccompile.compile_files opts copts; @@ -47,7 +47,7 @@ let coqc_main () = flush_all(); - if opts.Coqargs.output_context then begin + if opts.Coqargs.post.Coqargs.output_context then begin let sigma, env = let e = Global.env () in Evd.from_env e, e in Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) end; diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 4bcde566e3..f6211102e6 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -444,7 +444,7 @@ let drop_args = ref None let loop ~opts ~state = drop_args := Some opts; let open Coqargs in - print_emacs := opts.print_emacs; + print_emacs := opts.config.print_emacs; (* We initialize the console only if we run the toploop_run *) let tl_feed = Feedback.add_feeder coqloop_feed in if Dumpglob.dump () then begin diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 170959f2e2..22d293129e 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -48,8 +48,6 @@ let print_memory_stat () = with _ -> () end -let _ = at_exit print_memory_stat - let interp_set_option opt v old = let open Goptions in let err expect = @@ -159,6 +157,22 @@ let print_style_tags opts = let () = List.iter iter tags in flush_all () + +let print_queries opts extras q = + let print_query = function + | PrintVersion -> Usage.version () + | PrintMachineReadableVersion -> Usage.machine_readable_version () + | PrintWhere -> print_endline (Envars.coqlib ()) + | PrintHelp f -> f () + | PrintConfig -> Envars.print_config stdout Coq_config.all_src_dirs + | PrintTags -> print_style_tags opts.config in + List.iter print_query q.queries; + if q.filteropts then + if q.queries <> [] && extras <> [] then + error_wrong_arg "Queries are exclusive of other arguments" + else + print_string (String.concat "\n" extras) + (** GC tweaking *) (** Coq is a heavy user of persistent data structures and symbolic ASTs, so the @@ -184,6 +198,10 @@ let init_gc () = Gc.minor_heap_size = 33554432; (* 4M *) Gc.space_overhead = 120} +let init_setup = function + | None -> Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); + | Some s -> Envars.set_user_coqlib s + (** Main init routine *) let init_toplevel ~help ~init custom_init arglist = (* Coq's init process, phase 1: @@ -199,58 +217,44 @@ let init_toplevel ~help ~init custom_init arglist = Basic Coq environment, load-path, plugins. *) let opts, extras = parse_args ~help ~init arglist in - memory_stat := opts.memory_stat; + if opts.post.memory_stat then at_exit print_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 opts.print_where then begin - print_endline (Envars.coqlib ()); - exit (exitcode opts) - end; - if opts.print_config then begin - Envars.print_config stdout Coq_config.all_src_dirs; - exit (exitcode opts) - end; - if opts.print_tags then begin - print_style_tags opts; - exit (exitcode opts) - end; - if opts.filter_opts then begin - print_string (String.concat "\n" extras); - exit 0; - end; + init_setup opts.config.coqlib; + (* Querying or running? *) + match opts.main with + | Queries q -> print_queries opts extras q; exit 0 + | Run batch -> + (* Initialization *) let top_lp = Coqinit.toplevel_init_load_path () in List.iter Loadpath.add_coq_path top_lp; let opts, extras = custom_init ~opts extras in Mltop.init_known_plugins (); + (* Configuration *) + Global.set_engagement opts.config.logic.impredicative_set; + Global.set_indices_matter opts.config.logic.indices_matter; + Global.set_VM opts.config.enable_VM; + Global.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true); + Global.set_allow_sprop opts.config.logic.allow_sprop; + if opts.config.logic.cumulative_sprop then Global.make_sprop_cumulative (); - Global.set_engagement opts.impredicative_set; - Global.set_indices_matter opts.indices_matter; - Global.set_VM opts.enable_VM; - Global.set_native_compiler (match opts.native_compiler with NativeOff -> false | NativeOn _ -> true); - Global.set_allow_sprop opts.allow_sprop; - if opts.cumulative_sprop then Global.make_sprop_cumulative (); - - set_options opts.set_options; + set_options opts.config.set_options; (* Allow the user to load an arbitrary state here *) - inputstate opts; + inputstate opts.pre; (* This state will be shared by all the documents *) Stm.init_core (); + batch, opts, extras - (* Coq init process, phase 3: Stm initialization, backtracking state. +type init_fn = opts:Coqargs.t -> string list -> Coqargs.t * string list - 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, but now is thanks to the STM API. - *) +let init_batch_toplevel ~help ~init custom_init args = + let run_mode, opts, extras = init_toplevel ~help ~init custom_init args in opts, extras -type init_fn = opts:Coqargs.t -> string list -> Coqargs.t * string list - type custom_toplevel = { init : init_fn ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit @@ -258,16 +262,22 @@ type custom_toplevel = } let init_document opts = + (* Coq init process, phase 3: Stm initialization, backtracking state. + + 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, but now is thanks to the STM API. + *) let iload_path = build_load_path opts in let require_libs = require_libs opts in - let stm_options = opts.stm_flags in + let stm_options = opts.config.stm_flags in let open Vernac.State in let doc, sid = Stm.(new_doc - { doc_type = Interactive opts.toplevel_name; + { doc_type = Interactive opts.config.logic.toplevel_name; iload_path; require_libs; stm_options; }) in - { doc; sid; proof = None; time = opts.time } + { doc; sid; proof = None; time = opts.config.time } let init_toploop opts = let state = init_document opts in @@ -275,7 +285,7 @@ let init_toploop opts = state let coqtop_init ~opts extra = - init_color opts; + init_color opts.config; CoqworkmgrApi.(init !async_proofs_worker_priority); Flags.if_verbose print_header (); opts, extra @@ -289,9 +299,9 @@ let coqtop_toplevel = let start_coq custom = let init_feeder = Feedback.add_feeder Coqloop.coqloop_feed in (* Init phase *) - let state, opts = + let run_mode, state, opts = try - let opts, extras = + let run_mode, opts, extras = init_toplevel ~help:Usage.print_usage_coqtop ~init:default custom.init (List.tl (Array.to_list Sys.argv)) in @@ -300,10 +310,12 @@ let start_coq custom = prerr_endline "See -help for the list of supported options"; exit 1 end; - init_toploop opts, opts + let state = init_toploop opts in + run_mode, state, opts with any -> flush_all(); fatal_error_exn any in Feedback.del_feeder init_feeder; - if not opts.batch then custom.run ~opts ~state; - exit 0 + match run_mode with + | Interactive -> custom.run ~opts ~state; + | Batch -> exit 0 diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 40f569a1c8..d1f0f78355 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -23,7 +23,7 @@ type custom_toplevel = (** [init_toplevel ~help ~init custom_init arg_list] Common Coq initialization and argument parsing *) -val init_toplevel +val init_batch_toplevel : help:(unit -> unit) -> init:Coqargs.t -> init_fn diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 91b3c32126..011cc34987 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -8,15 +8,14 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -let version ret = +let version () = Printf.printf "The Coq Proof Assistant, version %s (%s)\n" Coq_config.version Coq_config.date; - Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version; - exit ret -let machine_readable_version ret = + Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version + +let machine_readable_version () = Printf.printf "%s %s\n" - Coq_config.version Coq_config.caml_version; - exit ret + Coq_config.version Coq_config.caml_version (* print the usage of coqtop (or coqc) on channel co *) diff --git a/toplevel/usage.mli b/toplevel/usage.mli index 1f257a5896..7d658579fd 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -8,10 +8,10 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** {6 Prints the version number on the standard output and exits (with 0). } *) +(** {6 Prints the version number on the standard output. } *) -val version : int -> 'a -val machine_readable_version : int -> 'a +val version : unit -> unit +val machine_readable_version : unit -> unit (** {6 Enable toploop plugins to insert some text in the usage message. } *) val add_to_usage : string -> string -> unit -- cgit v1.2.3 From 26b7e819746a6b36d0e22181f64549c503fe0481 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 8 May 2019 13:01:39 +0200 Subject: Function print_memory_stat: getting rid of a mutable. --- toplevel/coqtop.ml | 27 +++++++++++---------------- 1 file changed, 11 insertions(+), 16 deletions(-) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 22d293129e..2f2cebe074 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -30,23 +30,18 @@ let print_header () = Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); flush_all () -let memory_stat = ref false let print_memory_stat () = - begin (* -m|--memory from the command-line *) - if !memory_stat then - Feedback.msg_notice - (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ()); - end; - begin - (* operf-macro interface: - https://github.com/OCamlPro/operf-macro *) - try - let fn = Sys.getenv "OCAML_GC_STATS" in - let oc = open_out fn in - Gc.print_stat oc; - close_out oc - with _ -> () - end + (* -m|--memory from the command-line *) + Feedback.msg_notice + (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ()); + (* operf-macro interface: + https://github.com/OCamlPro/operf-macro *) + try + let fn = Sys.getenv "OCAML_GC_STATS" in + let oc = open_out fn in + Gc.print_stat oc; + close_out oc + with _ -> () let interp_set_option opt v old = let open Goptions in -- cgit v1.2.3 From dd15e030be5e55d3770d27fbbc2fe0f5384f0166 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 8 May 2019 19:42:08 +0200 Subject: Adding methods help and parse_extra to custom toplevels data. In particular, method init does not do parsing any more. This allows for instance to let coqidetop treats itself the "-filteropts" option. --- ide/coq.ml | 2 +- ide/idetop.ml | 23 ++++++++++++++++++----- toplevel/coqc.ml | 16 ++++++++++------ toplevel/coqtop.ml | 24 +++++++++++++++--------- toplevel/coqtop.mli | 18 ++++++++++-------- toplevel/workerLoop.ml | 13 ++++++++----- 6 files changed, 62 insertions(+), 34 deletions(-) diff --git a/ide/coq.ml b/ide/coq.ml index 92c24b3b85..889cc3be36 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -102,7 +102,7 @@ let display_coqtop_answer cmd lines = let rec filter_coq_opts args = let argstr = String.concat " " (List.map Filename.quote args) in - let cmd = Filename.quote (coqtop_path ()) ^" -nois -filteropts " ^ argstr in + let cmd = Filename.quote (coqtop_path ()) ^" -nois -batch " ^ argstr in let cmd = requote cmd in let filtered_args = ref [] in let errlines = ref [] in diff --git a/ide/idetop.ml b/ide/idetop.ml index c6a8fdaa55..c7638343b0 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -553,12 +553,25 @@ let () = Usage.add_to_usage "coqidetop" " --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\ \n --help-XML-protocol print documentation of the Coq XML protocol\n" -let islave_init ~opts extra_args = - let args = parse extra_args in - CoqworkmgrApi.(init High); - opts, args +let islave_parse ~opts extra_args = + let open Coqtop in + let run_mode, extra_args = coqtop_toplevel.parse_extra ~opts extra_args in + let extra_args = parse extra_args in + (* One of the role of coqidetop is to find the name of buffers to open *) + (* in the command line; Coqide is waiting these names on stdout *) + (* (see filter_coq_opts in coq.ml), so we send them now *) + print_string (String.concat "\n" extra_args); + run_mode, [] + +let islave_init ~opts = + CoqworkmgrApi.(init High) let () = let open Coqtop in - let custom = { init = islave_init; run = loop; opts = Coqargs.default } in + let custom = { + parse_extra = islave_parse ; + help = (fun _ -> output_string stderr "Same options as coqtop"); + init = islave_init; + run = loop; + opts = Coqargs.default } in start_coq custom diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 7c4aded5bb..e58b2eec3c 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -21,16 +21,20 @@ let coqc_main () = (* Careful because init_toplevel will call Summary.init_summaries, thus options such as `quiet` have to be set after the main initialisation is run. *) - let coqc_init ~opts args = + let coqc_init ~opts = set_noninteractive_mode (); - let opts, args = Coqtop.(coqtop_toplevel.init) ~opts args in - opts, args - in + Coqtop.(coqtop_toplevel.init) ~opts in + let custom_coqc = Coqtop.{ + coqtop_toplevel with + help = Usage.print_usage_coqc; + init = coqc_init; + parse_extra = (fun ~opts extras -> Coqcargs.parse extras, []); + } in let opts, extras = Topfmt.(in_phase ~phase:Initialization) - Coqtop.(init_batch_toplevel ~help:Usage.print_usage_coqc ~init:Coqargs.default coqc_init) List.(tl (Array.to_list Sys.argv)) in + Coqtop.(init_batch_toplevel ~help:Usage.print_usage_coqc ~init:Coqargs.default (fun ~opts extras -> coqc_init ~opts; (opts, extras))) List.(tl (Array.to_list Sys.argv)) in - let copts = Coqcargs.parse extras in + let copts, extras = custom_coqc.Coqtop.parse_extra ~opts extras in if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob (); diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 2f2cebe074..58dd994dcd 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -244,14 +244,16 @@ let init_toplevel ~help ~init custom_init arglist = Stm.init_core (); batch, opts, extras -type init_fn = opts:Coqargs.t -> string list -> Coqargs.t * string list - let init_batch_toplevel ~help ~init custom_init args = let run_mode, opts, extras = init_toplevel ~help ~init custom_init args in opts, extras -type custom_toplevel = - { init : init_fn +type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list + +type 'a custom_toplevel = + { parse_extra : 'a extra_args_fn + ; help : unit -> unit + ; init : opts:Coqargs.t -> unit ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit ; opts : Coqargs.t } @@ -279,14 +281,18 @@ let init_toploop opts = let state = Ccompile.load_init_vernaculars opts ~state in state -let coqtop_init ~opts extra = +let coqtop_init ~opts = init_color opts.config; CoqworkmgrApi.(init !async_proofs_worker_priority); - Flags.if_verbose print_header (); - opts, extra + Flags.if_verbose print_header () + +let coqtop_parse_extra ~opts extras = + opts, extras let coqtop_toplevel = - { init = coqtop_init + { parse_extra = coqtop_parse_extra + ; help = Usage.print_usage_coqtop + ; init = coqtop_init ; run = Coqloop.loop ; opts = Coqargs.default } @@ -298,7 +304,7 @@ let start_coq custom = try let run_mode, opts, extras = init_toplevel - ~help:Usage.print_usage_coqtop ~init:default custom.init + ~help:Usage.print_usage_coqtop ~init:default (fun ~opts extras -> let opts, extras = custom.parse_extra ~opts extras in custom.init ~opts; (opts, extras)) (List.tl (Array.to_list Sys.argv)) in if not (CList.is_empty extras) then begin prerr_endline ("Don't know what to do with "^String.concat " " extras); diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index d1f0f78355..3f2d458407 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -13,24 +13,26 @@ [run] launches a custom toplevel. *) -type init_fn = opts:Coqargs.t -> string list -> Coqargs.t * string list +type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list -type custom_toplevel = - { init : init_fn +type 'a custom_toplevel = + { parse_extra : 'a extra_args_fn + ; help : unit -> unit + ; init : opts:Coqargs.t -> unit ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit ; opts : Coqargs.t } -(** [init_toplevel ~help ~init custom_init arg_list] - Common Coq initialization and argument parsing *) +(** [init_toplevel custom] + Customized Coq initialization and argument parsing *) val init_batch_toplevel : help:(unit -> unit) -> init:Coqargs.t - -> init_fn + -> Coqargs.t extra_args_fn -> string list -> Coqargs.t * string list -val coqtop_toplevel : custom_toplevel +val coqtop_toplevel : Coqargs.t custom_toplevel (** The Coq main module. [start custom] will parse the command line, print the banner, initialize the load path, load the input state, @@ -38,4 +40,4 @@ val coqtop_toplevel : custom_toplevel produce the output state if any, and finally will launch [custom.run]. *) -val start_coq : custom_toplevel -> unit +val start_coq : Coqargs.t custom_toplevel -> unit diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index d362f9db22..6d147ac308 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -13,18 +13,21 @@ let rec parse = function | x :: rest -> x :: parse rest | [] -> [] -let arg_init init ~opts extra_args = - let extra_args = parse extra_args in +let worker_parse_extra ~opts extra_args = + opts, parse extra_args + +let worker_init init ~opts = Flags.quiet := true; init (); - CoqworkmgrApi.(init !async_proofs_worker_priority); - opts, extra_args + CoqworkmgrApi.(init !async_proofs_worker_priority) let start ~init ~loop = let open Coqtop in let custom = { + parse_extra = worker_parse_extra; + help = (fun _ -> output_string stderr "Same options as coqtop"); opts = Coqargs.default; - init = arg_init init; + init = worker_init init; run = (fun ~opts:_ ~state:_ -> loop ()); } in start_coq custom -- cgit v1.2.3 From e55ba2f04578738ec72c4ca64daf23b9ea51ec06 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 9 May 2019 00:36:49 +0200 Subject: An attempt to reorganize further coqtop initialization into semantic units. Incidentally moving parsing of "-batch" to the coqtop binary. --- stm/asyncTaskQueue.ml | 2 +- toplevel/coqargs.ml | 27 ++++-------- toplevel/coqargs.mli | 6 +-- toplevel/coqc.ml | 6 +-- toplevel/coqtop.ml | 110 ++++++++++++++++++++++++++++--------------------- toplevel/coqtop.mli | 15 +++---- toplevel/workerLoop.ml | 2 +- 7 files changed, 81 insertions(+), 87 deletions(-) diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 044ac29e92..dadf5f9f3e 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -125,7 +125,7 @@ module Make(T : Task) () = struct "-async-proofs-worker-priority"; CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)] (* Options to discard: 0 arguments *) - | ("-emacs"|"-batch")::tl -> + | "-emacs"::tl -> set_slave_opt tl (* Options to discard: 1 argument *) | ( "-async-proofs" | "-vio2vo" | "-o" diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index e47fbf2921..b1f823cd1a 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -85,14 +85,12 @@ type coqargs_base_query = type coqargs_queries = { queries : coqargs_base_query list; - filteropts : bool; + filteropts : string list option; } -type coqargs_interactive = Interactive | Batch - type coqargs_main = | Queries of coqargs_queries - | Run of coqargs_interactive + | Run type coqargs_post = { memory_stat : bool; @@ -151,12 +149,9 @@ let default_pre = { let default_queries = { queries = []; - filteropts = false; + filteropts = None; } -let default_main = - Run Interactive - let default_post = { memory_stat = false; output_context = false; @@ -165,7 +160,7 @@ let default_post = { let default = { config = default_config; pre = default_pre; - main = default_main; + main = Run; post = default_post; } @@ -209,26 +204,21 @@ let set_color opts = function | _ -> error_wrong_arg ("Error: on/off/auto expected after option color") -let set_batch opts = - { opts with main = match opts.main with - | Run _ -> Run Batch - | Queries _ as x -> x } - let add_query { queries; filteropts } q = { queries = queries@[q]; filteropts } let set_query opts q = { opts with main = match opts.main with - | Run _ -> Queries (add_query default_queries q) + | Run -> Queries (add_query default_queries q) | Queries queries -> Queries (add_query queries q) } let add_filteropts { queries } = - { queries; filteropts = true } + { queries; filteropts = Some [] } let set_filteropts opts = { opts with main = match opts.main with - | Run _ -> Queries (add_filteropts default_queries) + | Run -> Queries (add_filteropts default_queries) | Queries queries -> Queries (add_filteropts queries) } @@ -548,9 +538,6 @@ let parse_args ~help ~init arglist : t * string list = { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with Stm.AsyncOpts.async_proofs_never_reopen_branch = true }}} - |"-batch" -> - Flags.quiet := true; - set_batch oval |"-test-mode" -> Vernacentries.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval |"-bt" -> Backtrace.record_backtrace true; oval diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index 897885997c..3cbb0b109f 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -60,14 +60,12 @@ type coqargs_base_query = type coqargs_queries = { queries : coqargs_base_query list; - filteropts : bool; + filteropts : string list option; } -type coqargs_interactive = Interactive | Batch - type coqargs_main = | Queries of coqargs_queries - | Run of coqargs_interactive + | Run type coqargs_post = { memory_stat : bool; diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index e58b2eec3c..603d4118b5 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -30,11 +30,9 @@ let coqc_main () = init = coqc_init; parse_extra = (fun ~opts extras -> Coqcargs.parse extras, []); } in - let opts, extras = + let opts, copts = Topfmt.(in_phase ~phase:Initialization) - Coqtop.(init_batch_toplevel ~help:Usage.print_usage_coqc ~init:Coqargs.default (fun ~opts extras -> coqc_init ~opts; (opts, extras))) List.(tl (Array.to_list Sys.argv)) in - - let copts, extras = custom_coqc.Coqtop.parse_extra ~opts extras in + Coqtop.init_toplevel custom_coqc in if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob (); diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 58dd994dcd..79b9d5d501 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -11,6 +11,9 @@ open Pp open Coqargs +(** This file provides generic support for Coq executables + specific + support for the coqtop executable *) + let () = at_exit flush_all let ( / ) = Filename.concat @@ -152,8 +155,7 @@ let print_style_tags opts = let () = List.iter iter tags in flush_all () - -let print_queries opts extras q = +let print_queries opts q = let print_query = function | PrintVersion -> Usage.version () | PrintMachineReadableVersion -> Usage.machine_readable_version () @@ -162,11 +164,13 @@ let print_queries opts extras q = | PrintConfig -> Envars.print_config stdout Coq_config.all_src_dirs | PrintTags -> print_style_tags opts.config in List.iter print_query q.queries; - if q.filteropts then + match q.filteropts with + | Some extras -> if q.queries <> [] && extras <> [] then error_wrong_arg "Queries are exclusive of other arguments" else print_string (String.concat "\n" extras) + | None -> () (** GC tweaking *) @@ -197,35 +201,38 @@ let init_setup = function | None -> Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); | Some s -> Envars.set_user_coqlib s -(** Main init routine *) -let init_toplevel ~help ~init custom_init arglist = +let init_process () = (* Coq's init process, phase 1: OCaml parameters, basic structures, and IO *) CProfile.init_profile (); init_gc (); Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) - - Lib.init(); - + Lib.init () + +let init_parse parse_extra help init_opts = + let opts, extras = + parse_args ~help:help ~init:init_opts + (List.tl (Array.to_list Sys.argv)) in + let customopts, extras = parse_extra ~opts extras in + if not (CList.is_empty extras) then begin + prerr_endline ("Don't know what to do with "^String.concat " " extras); + prerr_endline "See -help for the list of supported options"; + exit 1 + end; + opts, customopts + +let init_execution opts custom_init = (* Coq's init process, phase 2: Basic Coq environment, load-path, plugins. *) - let opts, extras = parse_args ~help ~init arglist in - if opts.post.memory_stat then at_exit print_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 (); - init_setup opts.config.coqlib; - (* Querying or running? *) - match opts.main with - | Queries q -> print_queries opts extras q; exit 0 - | Run batch -> - (* Initialization *) + if opts.post.memory_stat then at_exit print_memory_stat; let top_lp = Coqinit.toplevel_init_load_path () in List.iter Loadpath.add_coq_path top_lp; - let opts, extras = custom_init ~opts extras in + custom_init ~opts; Mltop.init_known_plugins (); (* Configuration *) Global.set_engagement opts.config.logic.impredicative_set; @@ -241,12 +248,7 @@ let init_toplevel ~help ~init custom_init arglist = inputstate opts.pre; (* This state will be shared by all the documents *) - Stm.init_core (); - batch, opts, extras - -let init_batch_toplevel ~help ~init custom_init args = - let run_mode, opts, extras = init_toplevel ~help ~init custom_init args in - opts, extras + Stm.init_core () type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list @@ -258,6 +260,18 @@ type 'a custom_toplevel = ; opts : Coqargs.t } +(** Main init routine *) +let init_toplevel custom = + let () = init_process () in + let opts, customopts = init_parse custom.parse_extra custom.help custom.opts in + let () = init_setup opts.config.coqlib in + (* Querying or running? *) + match opts.main with + | Queries q -> print_queries opts q; exit 0 + | Run -> + let () = init_execution opts custom.init in + opts, customopts + let init_document opts = (* Coq init process, phase 3: Stm initialization, backtracking state. @@ -281,36 +295,14 @@ let init_toploop opts = let state = Ccompile.load_init_vernaculars opts ~state in state -let coqtop_init ~opts = - init_color opts.config; - CoqworkmgrApi.(init !async_proofs_worker_priority); - Flags.if_verbose print_header () - -let coqtop_parse_extra ~opts extras = - opts, extras - -let coqtop_toplevel = - { parse_extra = coqtop_parse_extra - ; help = Usage.print_usage_coqtop - ; init = coqtop_init - ; run = Coqloop.loop - ; opts = Coqargs.default - } +type run_mode = Interactive | Batch let start_coq custom = let init_feeder = Feedback.add_feeder Coqloop.coqloop_feed in (* Init phase *) let run_mode, state, opts = try - let run_mode, opts, extras = - init_toplevel - ~help:Usage.print_usage_coqtop ~init:default (fun ~opts extras -> let opts, extras = custom.parse_extra ~opts extras in custom.init ~opts; (opts, extras)) - (List.tl (Array.to_list Sys.argv)) in - if not (CList.is_empty extras) then begin - prerr_endline ("Don't know what to do with "^String.concat " " extras); - prerr_endline "See -help for the list of supported options"; - exit 1 - end; + let opts, run_mode = init_toplevel custom in let state = init_toploop opts in run_mode, state, opts with any -> @@ -320,3 +312,25 @@ let start_coq custom = match run_mode with | Interactive -> custom.run ~opts ~state; | Batch -> exit 0 + +let coqtop_init ~opts = + init_color opts.config; + CoqworkmgrApi.(init !async_proofs_worker_priority); + Flags.if_verbose print_header () + +let coqtop_parse_extra ~opts extras = + let rec parse_extra run_mode = function + | "-batch" :: rest -> parse_extra Batch rest + | x :: rest -> + let run_mode, rest = parse_extra run_mode rest in run_mode, x :: rest + | [] -> run_mode, [] in + let run_mode, extras = parse_extra Interactive extras in + run_mode, extras + +let coqtop_toplevel = + { parse_extra = coqtop_parse_extra + ; help = Usage.print_usage_coqtop + ; init = coqtop_init + ; run = Coqloop.loop + ; opts = Coqargs.default + } diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 3f2d458407..4a86dc1b5a 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -25,19 +25,16 @@ type 'a custom_toplevel = (** [init_toplevel custom] Customized Coq initialization and argument parsing *) -val init_batch_toplevel - : help:(unit -> unit) - -> init:Coqargs.t - -> Coqargs.t extra_args_fn - -> string list - -> Coqargs.t * string list +val init_toplevel : 'a custom_toplevel -> Coqargs.t * 'a -val coqtop_toplevel : Coqargs.t custom_toplevel +type run_mode = Interactive | Batch -(** The Coq main module. [start custom] will parse the command line, +(** The generic Coq main module. [start custom] will parse the command line, print the banner, initialize the load path, load the input state, load the files given on the command line, load the resource file, produce the output state if any, and finally will launch [custom.run]. *) +val start_coq : run_mode custom_toplevel -> unit -val start_coq : Coqargs.t custom_toplevel -> unit +(** The specific characterization of the coqtop_toplevel *) +val coqtop_toplevel : run_mode custom_toplevel diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index 6d147ac308..1fcc106348 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -14,7 +14,7 @@ let rec parse = function | [] -> [] let worker_parse_extra ~opts extra_args = - opts, parse extra_args + Coqtop.Interactive, parse extra_args let worker_init init ~opts = Flags.quiet := true; -- cgit v1.2.3 From c41f747f7df49bc26983d41096519672f05b793a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 10 May 2019 11:25:09 +0200 Subject: Layout/documentation updates. --- stm/asyncTaskQueue.ml | 4 ++-- stm/asyncTaskQueue.mli | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index dadf5f9f3e..fa6044fe88 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -155,8 +155,8 @@ module Make(T : Task) () = struct let args = Array.of_list (set_slave_opt (List.tl (Array.to_list Sys.argv))) in let env = Array.append (T.extra_env ()) (Unix.environment ()) in - let worker_name = System.get_toplevel_path ("coq" ^ !T.name) in - Worker.spawn ~env worker_name args in + let worker_name = System.get_toplevel_path ("coq" ^ !T.name) in + Worker.spawn ~env worker_name args in name, proc, CThread.prepare_in_channel_for_thread_friendly_io ic, oc let manager cpanel (id, proc, ic, oc) = diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli index a9a215acc8..ea438f3f76 100644 --- a/stm/asyncTaskQueue.mli +++ b/stm/asyncTaskQueue.mli @@ -68,10 +68,10 @@ module type Task = sig type request type response - (** UID of the task kind, for -toploop *) + (** UID of the task kind *) val name : string ref - (** Extra arguments of the task kind, for -toploop *) + (** Extra arguments of the task kind *) val extra_env : unit -> string array (** {5 Master API, it is run by the master, on a thread} *) -- cgit v1.2.3 From 2bdfddc39d1fd6200042ddb95ded98b44e14b8e5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 10 May 2019 11:24:51 +0200 Subject: Passing command-line option async_proofs_worker_priority functionally. We lose track of it at some time in "known_state" and assume that the reference cur_opt has not been modified in between the time it was set (in "new_doc") and "known_state". --- ide/idetop.ml | 11 ++++++++--- stm/asyncTaskQueue.ml | 12 ++++++------ stm/asyncTaskQueue.mli | 12 ++++++------ stm/coqworkmgrApi.ml | 3 ++- stm/coqworkmgrApi.mli | 2 +- stm/stm.ml | 29 +++++++++++++++++------------ stm/stm.mli | 2 ++ stm/workerPool.ml | 16 ++++++++-------- stm/workerPool.mli | 5 +++-- toplevel/coqargs.ml | 5 +++-- toplevel/coqtop.ml | 2 +- toplevel/workerLoop.ml | 3 +-- 12 files changed, 58 insertions(+), 44 deletions(-) diff --git a/ide/idetop.ml b/ide/idetop.ml index c7638343b0..f39c59f5d8 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -563,8 +563,13 @@ let islave_parse ~opts extra_args = print_string (String.concat "\n" extra_args); run_mode, [] -let islave_init ~opts = - CoqworkmgrApi.(init High) +let islave_init ~opts = () + +let islave_default_opts = + Coqargs.{ default with + config = { default.config with + stm_flags = { default.config.stm_flags with + Stm.AsyncOpts.async_proofs_worker_priority = CoqworkmgrApi.High }}} let () = let open Coqtop in @@ -573,5 +578,5 @@ let () = help = (fun _ -> output_string stderr "Same options as coqtop"); init = islave_init; run = loop; - opts = Coqargs.default } in + opts = islave_default_opts } in start_coq custom diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index fa6044fe88..909804d0c9 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -115,7 +115,7 @@ module Make(T : Task) () = struct type process = Worker.process type extra = (T.task * cancel_switch) TQueue.t - let spawn id = + let spawn id priority = let name = Printf.sprintf "%s:%d" !T.name id in let proc, ic, oc = (* Filter arguments for slaves. *) @@ -123,7 +123,7 @@ module Make(T : Task) () = struct | [] -> !async_proofs_flags_for_workers @ ["-worker-id"; name; "-async-proofs-worker-priority"; - CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)] + CoqworkmgrApi.(string_of_priority priority)] (* Options to discard: 0 arguments *) | "-emacs"::tl -> set_slave_opt tl @@ -262,7 +262,7 @@ module Make(T : Task) () = struct cleaner : Thread.t option; } - let create size = + let create size priority = let cleaner queue = while true do try ignore(TQueue.pop ~picky:(fun (_,cancelled) -> !cancelled) queue) @@ -270,7 +270,7 @@ module Make(T : Task) () = struct done in let queue = TQueue.create () in { - active = Pool.create queue ~size; + active = Pool.create queue ~size priority; queue; cleaner = if size > 0 then Some (CThread.create cleaner queue) else None; } @@ -369,8 +369,8 @@ module Make(T : Task) () = struct (TQueue.wait_until_n_are_waiting_then_snapshot (Pool.n_workers active) queue) - let with_n_workers n f = - let q = create n in + let with_n_workers n priority f = + let q = create n priority in try let rc = f q in destroy q; rc with e -> let e = CErrors.push e in destroy q; iraise e diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli index ea438f3f76..e6cf6343c8 100644 --- a/stm/asyncTaskQueue.mli +++ b/stm/asyncTaskQueue.mli @@ -144,10 +144,10 @@ module MakeQueue(T : Task) () : sig (** [queue] is the abstract queue type. *) type queue - (** [create n] will initialize the queue with [n] workers. If [n] is - 0, the queue won't spawn any process, working in a lazy local - manner. [not imposed by the this API] *) - val create : int -> queue + (** [create n pri] will initialize the queue with [n] workers having + priority [pri]. If [n] is 0, the queue won't spawn any process, + working in a lazy local manner. [not imposed by the this API] *) + val create : int -> CoqworkmgrApi.priority -> queue (** [destroy q] Deallocates [q], cancelling all pending tasks. *) val destroy : queue -> unit @@ -203,9 +203,9 @@ module MakeQueue(T : Task) () : sig (** [clear q] Clears [q], only if the worker prool is empty *) val clear : queue -> unit - (** [with_n_workers n f] create a queue, run the function, destroy + (** [with_n_workers n pri f] creates a queue, runs the function, destroys the queue. The user should call join *) - val with_n_workers : int -> (queue -> 'a) -> 'a + val with_n_workers : int -> CoqworkmgrApi.priority -> (queue -> 'a) -> 'a end diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml index c21f057742..92dc77172f 100644 --- a/stm/coqworkmgrApi.ml +++ b/stm/coqworkmgrApi.ml @@ -13,7 +13,8 @@ let debug = false type priority = Low | High (* Default priority *) -let async_proofs_worker_priority = ref Low + +let default_async_proofs_worker_priority = Low let string_of_priority = function Low -> "low" | High -> "high" let priority_of_string = function diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli index d53af84071..29eba5bc91 100644 --- a/stm/coqworkmgrApi.mli +++ b/stm/coqworkmgrApi.mli @@ -15,7 +15,7 @@ val string_of_priority : priority -> string val priority_of_string : string -> priority (* Default priority *) -val async_proofs_worker_priority : priority ref +val default_async_proofs_worker_priority : priority (* Connects to a work manager if any. If no worker manager, then -async-proofs-j and -async-proofs-tac-j are used *) diff --git a/stm/stm.ml b/stm/stm.ml index ceb62582cd..4db4579e38 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -51,6 +51,8 @@ module AsyncOpts = struct async_proofs_tac_error_resilience : tac_error_filter; async_proofs_cmd_error_resilience : bool; async_proofs_delegation_threshold : float; + + async_proofs_worker_priority : CoqworkmgrApi.priority; } let default_opts = { @@ -67,6 +69,8 @@ module AsyncOpts = struct async_proofs_tac_error_resilience = `Only [ "curly" ]; async_proofs_cmd_error_resilience = true; async_proofs_delegation_threshold = 0.03; + + async_proofs_worker_priority = CoqworkmgrApi.Low; } let cur_opt = ref default_opts @@ -1636,7 +1640,7 @@ and Slaves : sig val wait_all_done : unit -> unit (* initialize the whole machinery (optional) *) - val init : unit -> unit + val init : CoqworkmgrApi.priority -> unit type 'a tasks = (('a,VCS.vcs) Stateid.request * bool) list val dump_snapshot : unit -> Future.UUID.t tasks @@ -1658,11 +1662,11 @@ end = struct (* {{{ *) module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask) () let queue = ref None - let init () = + let init priority = if async_proofs_is_master !cur_opt then - queue := Some (TaskQueue.create !cur_opt.async_proofs_n_workers) + queue := Some (TaskQueue.create !cur_opt.async_proofs_n_workers priority) else - queue := Some (TaskQueue.create 0) + queue := Some (TaskQueue.create 0 priority) let check_task_aux extra name l i = let { Stateid.stop; document; loc; name = r_name }, drop = List.nth l i in @@ -1978,7 +1982,7 @@ and Partac : sig val vernac_interp : solve:bool -> abstract:bool -> cancel_switch:AsyncTaskQueue.cancel_switch -> - int -> Stateid.t -> Stateid.t -> aast -> unit + int -> CoqworkmgrApi.priority -> Stateid.t -> Stateid.t -> aast -> unit end = struct (* {{{ *) @@ -1990,7 +1994,7 @@ end = struct (* {{{ *) else f () - let vernac_interp ~solve ~abstract ~cancel_switch nworkers safe_id id + let vernac_interp ~solve ~abstract ~cancel_switch nworkers priority safe_id id { indentation; verbose; expr = e; strlen } : unit = let e, time, batch, fail = @@ -2003,7 +2007,7 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_fail ~st fail (fun () -> (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () -> - TaskQueue.with_n_workers nworkers (fun queue -> + TaskQueue.with_n_workers nworkers priority (fun queue -> PG_compat.map_proof (fun p -> let Proof.{goals} = Proof.data p in let open TacTask in @@ -2118,7 +2122,7 @@ end (* }}} *) and Query : sig - val init : unit -> unit + val init : CoqworkmgrApi.priority -> unit val vernac_interp : cancel_switch:AsyncTaskQueue.cancel_switch -> Stateid.t -> Stateid.t -> aast -> unit end = struct (* {{{ *) @@ -2132,7 +2136,7 @@ end = struct (* {{{ *) TaskQueue.enqueue_task (Option.get !queue) QueryTask.({ t_where = prev; t_for = id; t_what = q }) ~cancel_switch - let init () = queue := Some (TaskQueue.create 0) + let init priority = queue := Some (TaskQueue.create 0 priority) end (* }}} *) @@ -2410,7 +2414,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = resilient_tactic id cblock (fun () -> reach ~cache:true view.next; Partac.vernac_interp ~solve ~abstract ~cancel_switch - !cur_opt.async_proofs_n_tacworkers view.next id x) + !cur_opt.async_proofs_n_tacworkers + !cur_opt.async_proofs_worker_priority view.next id x) ), cache, true | `Cmd { cast = x; cqueue = `QueryQueue cancel_switch } when async_proofs_is_master !cur_opt -> (fun () -> @@ -2679,10 +2684,10 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = (* We record the state at this point! *) State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial; Backtrack.record (); - Slaves.init (); + Slaves.init stm_options.async_proofs_worker_priority; if async_proofs_is_master !cur_opt then begin stm_prerr_endline (fun () -> "Initializing workers"); - Query.init (); + Query.init stm_options.async_proofs_worker_priority; let opts = match !cur_opt.async_proofs_private_flags with | None -> [] | Some s -> Str.split_delim (Str.regexp ",") s in diff --git a/stm/stm.mli b/stm/stm.mli index 92a782d965..29e4b02e3f 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -34,6 +34,8 @@ module AsyncOpts : sig async_proofs_tac_error_resilience : tac_error_filter; async_proofs_cmd_error_resilience : bool; async_proofs_delegation_threshold : float; + + async_proofs_worker_priority : CoqworkmgrApi.priority; } val default_opts : stm_opt diff --git a/stm/workerPool.ml b/stm/workerPool.ml index 15c6510f7c..f77ced2f3a 100644 --- a/stm/workerPool.ml +++ b/stm/workerPool.ml @@ -19,7 +19,7 @@ type 'a cpanel = { module type PoolModel = sig (* this shall come from a Spawn.* model *) type process - val spawn : int -> worker_id * process * CThread.thread_ic * out_channel + val spawn : int -> CoqworkmgrApi.priority -> worker_id * process * CThread.thread_ic * out_channel (* this defines the main loop of the manager *) type extra @@ -79,20 +79,20 @@ let locking { lock; pool = p } f = x with e -> Mutex.unlock lock; raise e -let rec create_worker extra pool id = +let rec create_worker extra pool priority id = let cancel = ref false in - let name, process, ic, oc as worker = Model.spawn id in + let name, process, ic, oc as worker = Model.spawn id priority in master_handshake name ic oc; - let exit () = cancel := true; cleanup pool; Thread.exit () in + let exit () = cancel := true; cleanup pool priority; Thread.exit () in let cancelled () = !cancel in let cpanel = { exit; cancelled; extra } in let manager = CThread.create (Model.manager cpanel) worker in { name; cancel; manager; process } -and cleanup x = locking x begin fun { workers; count; extra_arg } -> +and cleanup x priority = locking x begin fun { workers; count; extra_arg } -> workers := List.map (function | { cancel } as w when !cancel = false -> w - | _ -> let n = !count in incr count; create_worker extra_arg x n) + | _ -> let n = !count in incr count; create_worker extra_arg x priority n) !workers end @@ -102,7 +102,7 @@ end let is_empty x = locking x begin fun { workers } -> !workers = [] end -let create extra_arg ~size = let x = { +let create extra_arg ~size priority = let x = { lock = Mutex.create (); pool = { extra_arg; @@ -110,7 +110,7 @@ let create extra_arg ~size = let x = { count = ref size; }} in locking x begin fun { workers } -> - workers := CList.init size (create_worker extra_arg x) + workers := CList.init size (create_worker extra_arg x priority) end; x diff --git a/stm/workerPool.mli b/stm/workerPool.mli index 5a6c968993..5468a24959 100644 --- a/stm/workerPool.mli +++ b/stm/workerPool.mli @@ -19,7 +19,8 @@ type 'a cpanel = { module type PoolModel = sig (* this shall come from a Spawn.* model *) type process - val spawn : int -> worker_id * process * CThread.thread_ic * out_channel + val spawn : int -> CoqworkmgrApi.priority -> + worker_id * process * CThread.thread_ic * out_channel (* this defines the main loop of the manager *) type extra @@ -31,7 +32,7 @@ module Make(Model : PoolModel) : sig type pool - val create : Model.extra -> size:int -> pool + val create : Model.extra -> size:int -> CoqworkmgrApi.priority -> pool val is_empty : pool -> bool val n_workers : pool -> int diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index b1f823cd1a..d05bf6378a 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -386,8 +386,9 @@ let parse_args ~help ~init arglist : t * string list = }}} |"-async-proofs-worker-priority" -> - CoqworkmgrApi.async_proofs_worker_priority := get_priority opt (next ()); - oval + { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with + Stm.AsyncOpts.async_proofs_worker_priority = get_priority opt (next ()) + }}} |"-async-proofs-private-flags" -> { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 79b9d5d501..560ba35a42 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -233,6 +233,7 @@ let init_execution opts custom_init = let top_lp = Coqinit.toplevel_init_load_path () in List.iter Loadpath.add_coq_path top_lp; custom_init ~opts; + CoqworkmgrApi.(init opts.config.stm_flags.Stm.AsyncOpts.async_proofs_worker_priority); Mltop.init_known_plugins (); (* Configuration *) Global.set_engagement opts.config.logic.impredicative_set; @@ -315,7 +316,6 @@ let start_coq custom = let coqtop_init ~opts = init_color opts.config; - CoqworkmgrApi.(init !async_proofs_worker_priority); Flags.if_verbose print_header () let coqtop_parse_extra ~opts extras = diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index 1fcc106348..c2bd8213b0 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -18,8 +18,7 @@ let worker_parse_extra ~opts extra_args = let worker_init init ~opts = Flags.quiet := true; - init (); - CoqworkmgrApi.(init !async_proofs_worker_priority) + init () let start ~init ~loop = let open Coqtop in -- cgit v1.2.3 From 01c965e1989cbc528d46b1751d8c2c708542da4e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 10 May 2019 20:26:30 +0200 Subject: Some common points between coqc and other coq binaries. - Binding coqc execution to the generic support for Coq binaries (i.e. to start_coq). - Moving init_toploop to the init part of coq executables so that coqc can avoid to call it. By the way, it is unclear what workerloop should do with it. Also, it is unclear how much the -l option should be considered an coqidetop or coq*worker option. In any case, it should be disallowed in coqc, I guess? - Moving the custom init part at the end of the initialization phase. Seems ok, despites the few involved side effects. --- ide/idetop.ml | 9 ++++++-- toplevel/coqc.ml | 43 +++++++++++++++++--------------------- toplevel/coqtop.ml | 56 ++++++++++++++++++++++++++++---------------------- toplevel/coqtop.mli | 27 ++++++++++++++---------- toplevel/workerLoop.ml | 9 ++++---- 5 files changed, 78 insertions(+), 66 deletions(-) diff --git a/ide/idetop.ml b/ide/idetop.ml index f39c59f5d8..f79ad5deab 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -496,7 +496,10 @@ let msg_format = ref (fun () -> (* The loop ignores the command line arguments as the current model delegates its handing to the toplevel container. *) -let loop ~opts:_ ~state = +let loop run_mode ~opts:_ state = + match run_mode with + | Coqtop.Batch -> exit 0 + | Coqtop.Interactive -> let open Vernac.State in set_doc state.doc; init_signal_handler (); @@ -563,7 +566,9 @@ let islave_parse ~opts extra_args = print_string (String.concat "\n" extra_args); run_mode, [] -let islave_init ~opts = () +let islave_init run_mode ~opts = + if run_mode = Coqtop.Batch then Flags.quiet := true; + Coqtop.init_toploop opts let islave_default_opts = Coqargs.{ default with diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 603d4118b5..fd275fdb1b 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -8,34 +8,18 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -let set_noninteractive_mode () = - Flags.quiet := true; - System.trust_file_cache := true - let outputstate opts = Option.iter (fun ostate_file -> let fname = CUnix.make_suffix ostate_file ".coq" in States.extern_state fname) opts.Coqcargs.outputstate -let coqc_main () = - (* Careful because init_toplevel will call Summary.init_summaries, - thus options such as `quiet` have to be set after the main - initialisation is run. *) - let coqc_init ~opts = - set_noninteractive_mode (); - Coqtop.(coqtop_toplevel.init) ~opts in - let custom_coqc = Coqtop.{ - coqtop_toplevel with - help = Usage.print_usage_coqc; - init = coqc_init; - parse_extra = (fun ~opts extras -> Coqcargs.parse extras, []); - } in - let opts, copts = - Topfmt.(in_phase ~phase:Initialization) - Coqtop.init_toplevel custom_coqc in - - if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob (); +let coqc_init _copts ~opts = + Flags.quiet := true; + System.trust_file_cache := true; + Coqtop.init_color opts.Coqargs.config; + if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob () +let coqc_main copts ~opts = Topfmt.(in_phase ~phase:CompilationPhase) Ccompile.compile_files opts copts; @@ -55,10 +39,10 @@ let coqc_main () = end; CProfile.print_profile () -let main () = +let coqc_run copts ~opts () = let _feeder = Feedback.add_feeder Coqloop.coqloop_feed in try - coqc_main (); + coqc_main ~opts copts; exit 0 with exn -> flush_all(); @@ -66,3 +50,14 @@ let main () = flush_all(); let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in exit exit_code + +let custom_coqc = Coqtop.{ + parse_extra = (fun ~opts extras -> Coqcargs.parse extras, []); + help = Usage.print_usage_coqc; + init = coqc_init; + run = coqc_run; + opts = Coqargs.default; +} + +let main () = + Coqtop.start_coq custom_coqc diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 560ba35a42..770698bee8 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -232,7 +232,6 @@ let init_execution opts custom_init = if opts.post.memory_stat then at_exit print_memory_stat; let top_lp = Coqinit.toplevel_init_load_path () in List.iter Loadpath.add_coq_path top_lp; - custom_init ~opts; CoqworkmgrApi.(init opts.config.stm_flags.Stm.AsyncOpts.async_proofs_worker_priority); Mltop.init_known_plugins (); (* Configuration *) @@ -249,15 +248,16 @@ let init_execution opts custom_init = inputstate opts.pre; (* This state will be shared by all the documents *) - Stm.init_core () + Stm.init_core (); + custom_init ~opts type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list -type 'a custom_toplevel = +type ('a,'b) custom_toplevel = { parse_extra : 'a extra_args_fn ; help : unit -> unit - ; init : opts:Coqargs.t -> unit - ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit + ; init : 'a -> opts:Coqargs.t -> 'b + ; run : 'a -> opts:Coqargs.t -> 'b -> unit ; opts : Coqargs.t } @@ -270,8 +270,8 @@ let init_toplevel custom = match opts.main with | Queries q -> print_queries opts q; exit 0 | Run -> - let () = init_execution opts custom.init in - opts, customopts + let customstate = init_execution opts (custom.init customopts) in + opts, customopts, customstate let init_document opts = (* Coq init process, phase 3: Stm initialization, backtracking state. @@ -291,32 +291,33 @@ let init_document opts = }) in { doc; sid; proof = None; time = opts.config.time } -let init_toploop opts = - let state = init_document opts in - let state = Ccompile.load_init_vernaculars opts ~state in - state - -type run_mode = Interactive | Batch - let start_coq custom = let init_feeder = Feedback.add_feeder Coqloop.coqloop_feed in (* Init phase *) - let run_mode, state, opts = - try - let opts, run_mode = init_toplevel custom in - let state = init_toploop opts in - run_mode, state, opts + let opts, custom_opts, state = + try init_toplevel custom with any -> flush_all(); fatal_error_exn any in Feedback.del_feeder init_feeder; - match run_mode with - | Interactive -> custom.run ~opts ~state; - | Batch -> exit 0 + (* Run phase *) + custom.run ~opts custom_opts state + +(** ****************************************) +(** Specific support for coqtop executable *) -let coqtop_init ~opts = +type run_mode = Interactive | Batch + +let init_toploop opts = + let state = init_document opts in + let state = Ccompile.load_init_vernaculars opts ~state in + state + +let coqtop_init run_mode ~opts = + if run_mode = Batch then Flags.quiet := true; init_color opts.config; - Flags.if_verbose print_header () + Flags.if_verbose print_header (); + init_toploop opts let coqtop_parse_extra ~opts extras = let rec parse_extra run_mode = function @@ -327,10 +328,15 @@ let coqtop_parse_extra ~opts extras = let run_mode, extras = parse_extra Interactive extras in run_mode, extras +let coqtop_run run_mode ~opts state = + match run_mode with + | Interactive -> Coqloop.loop ~opts ~state; + | Batch -> exit 0 + let coqtop_toplevel = { parse_extra = coqtop_parse_extra ; help = Usage.print_usage_coqtop ; init = coqtop_init - ; run = Coqloop.loop + ; run = coqtop_run ; opts = Coqargs.default } diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 4a86dc1b5a..e2339afbde 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -15,26 +15,31 @@ type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list -type 'a custom_toplevel = +type ('a,'b) custom_toplevel = { parse_extra : 'a extra_args_fn ; help : unit -> unit - ; init : opts:Coqargs.t -> unit - ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit + ; init : 'a -> opts:Coqargs.t -> 'b + ; run : 'a -> opts:Coqargs.t -> 'b -> unit ; opts : Coqargs.t } -(** [init_toplevel custom] - Customized Coq initialization and argument parsing *) -val init_toplevel : 'a custom_toplevel -> Coqargs.t * 'a - -type run_mode = Interactive | Batch - (** The generic Coq main module. [start custom] will parse the command line, print the banner, initialize the load path, load the input state, load the files given on the command line, load the resource file, produce the output state if any, and finally will launch [custom.run]. *) -val start_coq : run_mode custom_toplevel -> unit +val start_coq : ('a,'b) custom_toplevel -> unit + +(** Initializer color for output *) + +val init_color : Coqargs.coqargs_config -> unit + +(** Prepare state for interactive loop *) + +val init_toploop : Coqargs.t -> Vernac.State.t (** The specific characterization of the coqtop_toplevel *) -val coqtop_toplevel : run_mode custom_toplevel + +type run_mode = Interactive | Batch + +val coqtop_toplevel : (run_mode,Vernac.State.t) custom_toplevel diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index c2bd8213b0..0087e4833c 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -14,11 +14,12 @@ let rec parse = function | [] -> [] let worker_parse_extra ~opts extra_args = - Coqtop.Interactive, parse extra_args + (), parse extra_args -let worker_init init ~opts = +let worker_init init () ~opts = Flags.quiet := true; - init () + init (); + Coqtop.init_toploop opts let start ~init ~loop = let open Coqtop in @@ -27,6 +28,6 @@ let start ~init ~loop = help = (fun _ -> output_string stderr "Same options as coqtop"); opts = Coqargs.default; init = worker_init init; - run = (fun ~opts:_ ~state:_ -> loop ()); + run = (fun () ~opts:_ _state (* why is state not used *) -> loop ()); } in start_coq custom -- cgit v1.2.3 From cc9a10182255527959fc10bd86f18a7b40ef5a2a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 8 May 2019 21:26:37 +0200 Subject: Removing -filterops "hack" from coqtop. This is now the "coqidetop" binary which specifically know how to collect extra arguments. --- toplevel/coqargs.ml | 31 +++++-------------------------- toplevel/coqargs.mli | 9 ++------- toplevel/coqtop.ml | 25 ++++++++----------------- 3 files changed, 15 insertions(+), 50 deletions(-) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index d05bf6378a..5e3a82dcb9 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -78,18 +78,13 @@ type coqargs_pre = { inputstate : string option; } -type coqargs_base_query = +type coqargs_query = | PrintTags | PrintWhere | PrintConfig | PrintVersion | PrintMachineReadableVersion | PrintHelp of (unit -> unit) -type coqargs_queries = { - queries : coqargs_base_query list; - filteropts : string list option; -} - type coqargs_main = - | Queries of coqargs_queries + | Queries of coqargs_query list | Run type coqargs_post = { @@ -147,10 +142,7 @@ let default_pre = { inputstate = None; } -let default_queries = { - queries = []; - filteropts = None; -} +let default_queries = [] let default_post = { memory_stat = false; @@ -204,22 +196,10 @@ let set_color opts = function | _ -> error_wrong_arg ("Error: on/off/auto expected after option color") -let add_query { queries; filteropts } q = - { queries = queries@[q]; filteropts } - let set_query opts q = { opts with main = match opts.main with - | Run -> Queries (add_query default_queries q) - | Queries queries -> Queries (add_query queries q) - } - -let add_filteropts { queries } = - { queries; filteropts = Some [] } - -let set_filteropts opts = - { opts with main = match opts.main with - | Run -> Queries (add_filteropts default_queries) - | Queries queries -> Queries (add_filteropts queries) + | Run -> Queries (default_queries@[q]) + | Queries queries -> Queries (queries@[q]) } let warn_deprecated_inputstate = @@ -553,7 +533,6 @@ let parse_args ~help ~init arglist : t * string list = { oval with config = { oval.config with diffs_set = true }} |"-stm-debug" -> Stm.stm_debug := true; oval |"-emacs" -> set_emacs oval - |"-filteropts" -> set_filteropts oval |"-impredicative-set" -> set_logic (fun o -> { o with impredicative_set = Declarations.ImpredicativeSet }) oval |"-allow-sprop" -> set_logic (fun o -> { o with allow_sprop = true }) oval diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index 3cbb0b109f..d1873bcb58 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -53,18 +53,13 @@ type coqargs_pre = { inputstate : string option; } -type coqargs_base_query = +type coqargs_query = | PrintTags | PrintWhere | PrintConfig | PrintVersion | PrintMachineReadableVersion | PrintHelp of (unit -> unit) -type coqargs_queries = { - queries : coqargs_base_query list; - filteropts : string list option; -} - type coqargs_main = - | Queries of coqargs_queries + | Queries of coqargs_query list | Run type coqargs_post = { diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 770698bee8..95f9d9ef77 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -155,22 +155,13 @@ let print_style_tags opts = let () = List.iter iter tags in flush_all () -let print_queries opts q = - let print_query = function - | PrintVersion -> Usage.version () - | PrintMachineReadableVersion -> Usage.machine_readable_version () - | PrintWhere -> print_endline (Envars.coqlib ()) - | PrintHelp f -> f () - | PrintConfig -> Envars.print_config stdout Coq_config.all_src_dirs - | PrintTags -> print_style_tags opts.config in - List.iter print_query q.queries; - match q.filteropts with - | Some extras -> - if q.queries <> [] && extras <> [] then - error_wrong_arg "Queries are exclusive of other arguments" - else - print_string (String.concat "\n" extras) - | None -> () +let print_query opts = function + | PrintVersion -> Usage.version () + | PrintMachineReadableVersion -> Usage.machine_readable_version () + | PrintWhere -> print_endline (Envars.coqlib ()) + | PrintHelp f -> f () + | PrintConfig -> Envars.print_config stdout Coq_config.all_src_dirs + | PrintTags -> print_style_tags opts.config (** GC tweaking *) @@ -268,7 +259,7 @@ let init_toplevel custom = let () = init_setup opts.config.coqlib in (* Querying or running? *) match opts.main with - | Queries q -> print_queries opts q; exit 0 + | Queries q -> List.iter (print_query opts) q; exit 0 | Run -> let customstate = init_execution opts (custom.init customopts) in opts, customopts, customstate -- cgit v1.2.3 From fe487e8eaae3186803ec657c517d0ebebab3bafd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 8 May 2019 22:42:48 +0200 Subject: An even more uniform treatment of the -help option across executables. Incidentally fix some missing newline in coqc help, and give proper help for coqidetop and the "coq*worker"s. --- ide/idetop.ml | 8 +++++--- topbin/coqproofworker_bin.ml | 2 +- topbin/coqqueryworker_bin.ml | 2 +- topbin/coqtacticworker_bin.ml | 2 +- toplevel/coqargs.ml | 8 +++++--- toplevel/coqargs.mli | 4 ++-- toplevel/coqc.ml | 17 ++++++++++++++- toplevel/coqtop.ml | 11 +++++++--- toplevel/coqtop.mli | 2 +- toplevel/usage.ml | 48 +++++++++---------------------------------- toplevel/usage.mli | 8 ++++---- toplevel/workerLoop.ml | 6 ++++-- toplevel/workerLoop.mli | 4 ++-- 13 files changed, 60 insertions(+), 62 deletions(-) diff --git a/ide/idetop.ml b/ide/idetop.ml index f79ad5deab..eb76951b44 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -552,8 +552,10 @@ let rec parse = function x :: parse rest | [] -> [] -let () = Usage.add_to_usage "coqidetop" -" --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\ +let () = Usage.add_to_usage "coqidetop" "" "\n\ +coqidetop specific options:\n\ +\n --xml_formatinclude dir (idem)\ +\n --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\ \n --help-XML-protocol print documentation of the Coq XML protocol\n" let islave_parse ~opts extra_args = @@ -580,7 +582,7 @@ let () = let open Coqtop in let custom = { parse_extra = islave_parse ; - help = (fun _ -> output_string stderr "Same options as coqtop"); + help = Usage.print_usage "coqidetop"; init = islave_init; run = loop; opts = islave_default_opts } in diff --git a/topbin/coqproofworker_bin.ml b/topbin/coqproofworker_bin.ml index baf76582ac..2715406b13 100644 --- a/topbin/coqproofworker_bin.ml +++ b/topbin/coqproofworker_bin.ml @@ -11,4 +11,4 @@ module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) () let () = - WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop + WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop "coqproofworker" diff --git a/topbin/coqqueryworker_bin.ml b/topbin/coqqueryworker_bin.ml index 0f7005e422..225158e064 100644 --- a/topbin/coqqueryworker_bin.ml +++ b/topbin/coqqueryworker_bin.ml @@ -10,4 +10,4 @@ module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) () -let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop +let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop "coqqueryworker" diff --git a/topbin/coqtacticworker_bin.ml b/topbin/coqtacticworker_bin.ml index 19a8cde88a..962028e0e7 100644 --- a/topbin/coqtacticworker_bin.ml +++ b/topbin/coqtacticworker_bin.ml @@ -10,4 +10,4 @@ module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) () -let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop +let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop "coqtacticworker" diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 5e3a82dcb9..b07639511c 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -81,7 +81,7 @@ type coqargs_pre = { type coqargs_query = | PrintTags | PrintWhere | PrintConfig | PrintVersion | PrintMachineReadableVersion - | PrintHelp of (unit -> unit) + | PrintHelp of (out_channel -> unit) type coqargs_main = | Queries of coqargs_query list @@ -290,6 +290,7 @@ let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesy exception NoCoqLib +(* Is this still useful for displaying help? *) let usage help = begin try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib) @@ -298,7 +299,7 @@ let usage help = let lp = Coqinit.toplevel_init_load_path () in (* Necessary for finding the toplevels below *) List.iter Loadpath.add_coq_path lp; - help () + help (* Main parsing routine *) let parse_args ~help ~init arglist : t * string list = @@ -554,7 +555,8 @@ let parse_args ~help ~init arglist : t * string list = |"-type-in-type" -> set_type_in_type (); oval |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) |"-where" -> set_query oval PrintWhere - |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp (fun () -> usage help)) + |"-h"|"-H"|"-?"|"-help"|"--help" -> + set_query oval (PrintHelp (fun co -> usage (help co))) |"-v"|"--version" -> set_query oval PrintVersion |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index d1873bcb58..46220cd1d8 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -56,7 +56,7 @@ type coqargs_pre = { type coqargs_query = | PrintTags | PrintWhere | PrintConfig | PrintVersion | PrintMachineReadableVersion - | PrintHelp of (unit -> unit) + | PrintHelp of (out_channel -> unit) type coqargs_main = | Queries of coqargs_query list @@ -77,7 +77,7 @@ type t = { (* Default options *) val default : t -val parse_args : help:(unit -> unit) -> init:t -> string list -> t * string list +val parse_args : help:(out_channel -> unit) -> init:t -> string list -> t * string list val error_wrong_arg : string -> unit val require_libs : t -> (string * string option * bool option) list diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index fd275fdb1b..c905eff646 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -19,6 +19,21 @@ let coqc_init _copts ~opts = Coqtop.init_color opts.Coqargs.config; if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob () +let () = Usage.add_to_usage "coqc" "file..." "\n\ +coqc specific options:\ +\n -o f.vo use f.vo as the output file name\ +\n -verbose compile and output the input file\ +\n -quick quickly compile .v files to .vio files (skip proofs)\ +\n -schedule-vio2vo j f1..fn run up to j instances of Coq to turn each fi.vio\ +\n into fi.vo\ +\n -schedule-vio-checking j f1..fn run up to j instances of Coq to check all\ +\n proofs in each fi.vio\ +\n\ +\nUndocumented:\ +\n -vio2vo [see manual]\ +\n -check-vio-tasks [see manual]\ +\n" + let coqc_main copts ~opts = Topfmt.(in_phase ~phase:CompilationPhase) Ccompile.compile_files opts copts; @@ -53,7 +68,7 @@ let coqc_run copts ~opts () = let custom_coqc = Coqtop.{ parse_extra = (fun ~opts extras -> Coqcargs.parse extras, []); - help = Usage.print_usage_coqc; + help = Usage.print_usage "coqc"; init = coqc_init; run = coqc_run; opts = Coqargs.default; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 95f9d9ef77..5194c7a128 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -159,7 +159,7 @@ let print_query opts = function | PrintVersion -> Usage.version () | PrintMachineReadableVersion -> Usage.machine_readable_version () | PrintWhere -> print_endline (Envars.coqlib ()) - | PrintHelp f -> f () + | PrintHelp f -> f stderr | PrintConfig -> Envars.print_config stdout Coq_config.all_src_dirs | PrintTags -> print_style_tags opts.config @@ -246,7 +246,7 @@ type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list type ('a,'b) custom_toplevel = { parse_extra : 'a extra_args_fn - ; help : unit -> unit + ; help : out_channel -> unit ; init : 'a -> opts:Coqargs.t -> 'b ; run : 'a -> opts:Coqargs.t -> 'b -> unit ; opts : Coqargs.t @@ -324,9 +324,14 @@ let coqtop_run run_mode ~opts state = | Interactive -> Coqloop.loop ~opts ~state; | Batch -> exit 0 +let () = Usage.add_to_usage "coqtop" "" "\n\ +coqtop specific options:\n\ +\n -batch batch mode (exits after interpretation of command line)\ +\n" + let coqtop_toplevel = { parse_extra = coqtop_parse_extra - ; help = Usage.print_usage_coqtop + ; help = Usage.print_usage "coqtop" ; init = coqtop_init ; run = coqtop_run ; opts = Coqargs.default diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index e2339afbde..af1890bee5 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -17,7 +17,7 @@ type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list type ('a,'b) custom_toplevel = { parse_extra : 'a extra_args_fn - ; help : unit -> unit + ; help : out_channel -> unit ; init : 'a -> opts:Coqargs.t -> 'b ; run : 'a -> opts:Coqargs.t -> 'b -> unit ; opts : Coqargs.t diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 011cc34987..636d4f8d5d 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -20,7 +20,8 @@ let machine_readable_version () = (* print the usage of coqtop (or coqc) on channel co *) let extra_usage = ref [] -let add_to_usage name text = extra_usage := (name,text) :: !extra_usage +let add_to_usage name extra text = + extra_usage := (name,(extra,text)) :: !extra_usage let print_usage_common co command = output_string co command; @@ -98,42 +99,13 @@ let print_usage_common co command = \n -bytecode-compiler (yes|no) enable the vm_compute reduction machine\ \n -native-compiler (yes|no|ondemand) enable the native_compute reduction machine\ \n -h, -help, --help print this list of options\ -\n"; - List.iter (fun (name, text) -> - output_string co - ("\nWith the flag '-toploop "^name^ - "' these extra option are also available:\n"^ - text^"\n")) - !extra_usage +\n" -(* print the usage on standard error *) +(* print the usage *) -let print_usage_coqtop () = - print_usage_common stderr "Usage: coqtop \n\n"; - output_string stderr "\n\ -coqtop specific options:\ -\n\ -\n -batch batch mode (exits just after argument parsing)\ -\n"; - flush stderr ; - exit 1 - -let print_usage_coqc () = - print_usage_common stderr "Usage: coqc file...\n\n"; - output_string stderr "\n\ -coqc specific options:\ -\n\ -\n -o f.vo use f.vo as the output file name\ -\n -verbose compile and output the input file\ -\n -quick quickly compile .v files to .vio files (skip proofs)\ -\n -schedule-vio2vo j f1..fn run up to j instances of Coq to turn each fi.vio\ -\n into fi.vo\ -\n -schedule-vio-checking j f1..fn run up to j instances of Coq to check all\ -\n proofs in each fi.vio\ -\n\ -\nUndocumented:\ -\n -vio2vo [see manual]\ -\n -check-vio-tasks [see manual]\ -\n"; - flush stderr ; - exit 1 +let print_usage binfile co = + let extra, text = + try List.assoc binfile !extra_usage + with Not_found -> ("","") in + print_usage_common co ("Usage: " ^ binfile ^ " " ^ extra ^ "\n\n"); + output_string co text diff --git a/toplevel/usage.mli b/toplevel/usage.mli index 7d658579fd..7d80598b7e 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -13,10 +13,10 @@ val version : unit -> unit val machine_readable_version : unit -> unit -(** {6 Enable toploop plugins to insert some text in the usage message. } *) -val add_to_usage : string -> string -> unit +(** {6 [add_to_usage name extra_args extra_options] tell what extra + arguments or options to print when asking usage for command [name]. } *) +val add_to_usage : string -> string -> string -> unit (** {6 Prints the usage on the error output. } *) -val print_usage_coqtop : unit -> unit -val print_usage_coqc : unit -> unit +val print_usage : string -> out_channel -> unit diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index 0087e4833c..3af48bad99 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -21,11 +21,13 @@ let worker_init init () ~opts = init (); Coqtop.init_toploop opts -let start ~init ~loop = +let start ~init ~loop name = + let _ = Usage.add_to_usage name "" ("\n" ^ name ^ " specific options:\ +\n --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\n") in let open Coqtop in let custom = { parse_extra = worker_parse_extra; - help = (fun _ -> output_string stderr "Same options as coqtop"); + help = Usage.print_usage name; opts = Coqargs.default; init = worker_init init; run = (fun () ~opts:_ _state (* why is state not used *) -> loop ()); diff --git a/toplevel/workerLoop.mli b/toplevel/workerLoop.mli index 685a10f6f3..8d6f0b1988 100644 --- a/toplevel/workerLoop.mli +++ b/toplevel/workerLoop.mli @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(* Register a STM worker *) +(* Register a STM worker of a given executable name *) val start : init:(unit -> unit) -> - loop:(unit -> unit) -> unit + loop:(unit -> unit) -> string -> unit -- cgit v1.2.3 From f2779d48d3b7735687444e22b16cdb7cb8f7ce60 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 10 May 2019 09:36:57 +0200 Subject: Usage: bypassing a useless detour via a reference. --- ide/idetop.ml | 8 ++++++-- toplevel/coqargs.ml | 27 ++++----------------------- toplevel/coqargs.mli | 4 ++-- toplevel/coqc.ml | 8 ++++++-- toplevel/coqtop.ml | 12 ++++++++---- toplevel/coqtop.mli | 2 +- toplevel/usage.ml | 19 +++++++++---------- toplevel/usage.mli | 17 ++++++++++++----- toplevel/workerLoop.ml | 11 ++++++++--- 9 files changed, 56 insertions(+), 52 deletions(-) diff --git a/ide/idetop.ml b/ide/idetop.ml index eb76951b44..02682e2ee9 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -552,11 +552,15 @@ let rec parse = function x :: parse rest | [] -> [] -let () = Usage.add_to_usage "coqidetop" "" "\n\ +let coqidetop_specific_usage = Usage.{ + executable_name = "coqidetop"; + extra_args = ""; + extra_options = "\n\ coqidetop specific options:\n\ \n --xml_formatinclude dir (idem)\ \n --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\ \n --help-XML-protocol print documentation of the Coq XML protocol\n" +} let islave_parse ~opts extra_args = let open Coqtop in @@ -582,7 +586,7 @@ let () = let open Coqtop in let custom = { parse_extra = islave_parse ; - help = Usage.print_usage "coqidetop"; + help = coqidetop_specific_usage; init = islave_init; run = loop; opts = islave_default_opts } in diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index b07639511c..eb0331d95e 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -81,7 +81,7 @@ type coqargs_pre = { type coqargs_query = | PrintTags | PrintWhere | PrintConfig | PrintVersion | PrintMachineReadableVersion - | PrintHelp of (out_channel -> unit) + | PrintHelp of Usage.specific_usage type coqargs_main = | Queries of coqargs_query list @@ -281,27 +281,9 @@ let parse_option_set opt = let v = String.sub opt (eqi+1) (len - eqi - 1) in to_opt_key (String.sub opt 0 eqi), Some v -(*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 - -(* Is this still useful for displaying help? *) -let usage help = - 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 Loadpath.add_coq_path lp; - help - (* Main parsing routine *) +(*s Parsing of the command line *) + let parse_args ~help ~init arglist : t * string list = let args = ref arglist in let extras = ref [] in @@ -555,8 +537,7 @@ let parse_args ~help ~init arglist : t * string list = |"-type-in-type" -> set_type_in_type (); oval |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) |"-where" -> set_query oval PrintWhere - |"-h"|"-H"|"-?"|"-help"|"--help" -> - set_query oval (PrintHelp (fun co -> usage (help co))) + |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp help) |"-v"|"--version" -> set_query oval PrintVersion |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index 46220cd1d8..e414888861 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -56,7 +56,7 @@ type coqargs_pre = { type coqargs_query = | PrintTags | PrintWhere | PrintConfig | PrintVersion | PrintMachineReadableVersion - | PrintHelp of (out_channel -> unit) + | PrintHelp of Usage.specific_usage type coqargs_main = | Queries of coqargs_query list @@ -77,7 +77,7 @@ type t = { (* Default options *) val default : t -val parse_args : help:(out_channel -> unit) -> init:t -> string list -> t * string list +val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * string list val error_wrong_arg : string -> unit val require_libs : t -> (string * string option * bool option) list diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index c905eff646..5678acb2b1 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -19,7 +19,10 @@ let coqc_init _copts ~opts = Coqtop.init_color opts.Coqargs.config; if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob () -let () = Usage.add_to_usage "coqc" "file..." "\n\ +let coqc_specific_usage = Usage.{ + executable_name = "coqc"; + extra_args = "file..."; + extra_options = "\n\ coqc specific options:\ \n -o f.vo use f.vo as the output file name\ \n -verbose compile and output the input file\ @@ -33,6 +36,7 @@ coqc specific options:\ \n -vio2vo [see manual]\ \n -check-vio-tasks [see manual]\ \n" +} let coqc_main copts ~opts = Topfmt.(in_phase ~phase:CompilationPhase) @@ -68,7 +72,7 @@ let coqc_run copts ~opts () = let custom_coqc = Coqtop.{ parse_extra = (fun ~opts extras -> Coqcargs.parse extras, []); - help = Usage.print_usage "coqc"; + help = coqc_specific_usage; init = coqc_init; run = coqc_run; opts = Coqargs.default; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 5194c7a128..f09d202edf 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -159,7 +159,7 @@ let print_query opts = function | PrintVersion -> Usage.version () | PrintMachineReadableVersion -> Usage.machine_readable_version () | PrintWhere -> print_endline (Envars.coqlib ()) - | PrintHelp f -> f stderr + | PrintHelp h -> Usage.print_usage stderr h | PrintConfig -> Envars.print_config stdout Coq_config.all_src_dirs | PrintTags -> print_style_tags opts.config @@ -246,7 +246,7 @@ type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list type ('a,'b) custom_toplevel = { parse_extra : 'a extra_args_fn - ; help : out_channel -> unit + ; help : Usage.specific_usage ; init : 'a -> opts:Coqargs.t -> 'b ; run : 'a -> opts:Coqargs.t -> 'b -> unit ; opts : Coqargs.t @@ -324,14 +324,18 @@ let coqtop_run run_mode ~opts state = | Interactive -> Coqloop.loop ~opts ~state; | Batch -> exit 0 -let () = Usage.add_to_usage "coqtop" "" "\n\ +let coqtop_specific_usage = Usage.{ + executable_name = "coqtop"; + extra_args = ""; + extra_options = "\n\ coqtop specific options:\n\ \n -batch batch mode (exits after interpretation of command line)\ \n" +} let coqtop_toplevel = { parse_extra = coqtop_parse_extra - ; help = Usage.print_usage "coqtop" + ; help = coqtop_specific_usage ; init = coqtop_init ; run = coqtop_run ; opts = Coqargs.default diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index af1890bee5..4fe7d538a8 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -17,7 +17,7 @@ type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list type ('a,'b) custom_toplevel = { parse_extra : 'a extra_args_fn - ; help : out_channel -> unit + ; help : Usage.specific_usage ; init : 'a -> opts:Coqargs.t -> 'b ; run : 'a -> opts:Coqargs.t -> 'b -> unit ; opts : Coqargs.t diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 636d4f8d5d..cdb2e36fbd 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -19,10 +19,6 @@ let machine_readable_version () = (* print the usage of coqtop (or coqc) on channel co *) -let extra_usage = ref [] -let add_to_usage name extra text = - extra_usage := (name,(extra,text)) :: !extra_usage - let print_usage_common co command = output_string co command; output_string co "Coq options are:\n"; @@ -103,9 +99,12 @@ let print_usage_common co command = (* print the usage *) -let print_usage binfile co = - let extra, text = - try List.assoc binfile !extra_usage - with Not_found -> ("","") in - print_usage_common co ("Usage: " ^ binfile ^ " " ^ extra ^ "\n\n"); - output_string co text +type specific_usage = { + executable_name : string; + extra_args : string; + extra_options : string; +} + +let print_usage co { executable_name; extra_args; extra_options } = + print_usage_common co ("Usage: " ^ executable_name ^ " " ^ extra_args ^ "\n\n"); + output_string co extra_options diff --git a/toplevel/usage.mli b/toplevel/usage.mli index 7d80598b7e..536cbdc6b2 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -13,10 +13,17 @@ val version : unit -> unit val machine_readable_version : unit -> unit -(** {6 [add_to_usage name extra_args extra_options] tell what extra - arguments or options to print when asking usage for command [name]. } *) -val add_to_usage : string -> string -> string -> unit +(** {6 extra arguments or options to print when asking usage for a + given executable. } *) -(** {6 Prints the usage on the error output. } *) -val print_usage : string -> out_channel -> unit +type specific_usage = { + executable_name : string; + extra_args : string; + extra_options : string; +} + +(** {6 Prints the generic part and specific part of usage for a + given executable. } *) + +val print_usage : out_channel -> specific_usage -> unit diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index 3af48bad99..5f80ac475c 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -21,13 +21,18 @@ let worker_init init () ~opts = init (); Coqtop.init_toploop opts +let worker_specific_usage name = Usage.{ + executable_name = name; + extra_args = ""; + extra_options = ("\n" ^ name ^ " specific options:\ +\n --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\n"); +} + let start ~init ~loop name = - let _ = Usage.add_to_usage name "" ("\n" ^ name ^ " specific options:\ -\n --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\n") in let open Coqtop in let custom = { parse_extra = worker_parse_extra; - help = Usage.print_usage name; + help = worker_specific_usage name; opts = Coqargs.default; init = worker_init init; run = (fun () ~opts:_ _state (* why is state not used *) -> loop ()); -- cgit v1.2.3