From 4264aec518d5407f345c58e18e014e15e9ae96af Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 5 Jan 2021 11:34:35 +0100 Subject: [sysinit] new component for system initialization This component holds the code for initializing Coq: - parsing arguments not specific to the toplevel - initializing all components from vernac downwards (no stm) This commit moves stm specific arguments parsing to stm/stmargs.ml --- META.coq.in | 17 +- Makefile.common | 4 +- Makefile.dev | 3 +- dev/base_include | 1 - dev/dune | 1 + dev/tools/update-compat.py | 2 +- ide/coqide/idetop.ml | 16 +- stm/dune | 2 +- stm/stm.ml | 71 +----- stm/stm.mli | 29 +-- stm/stm.mllib | 1 + stm/stmargs.ml | 140 +++++++++++ stm/stmargs.mli | 13 + sysinit/coqargs.ml | 515 ++++++++++++++++++++++++++++++++++++++++ sysinit/coqargs.mli | 107 +++++++++ sysinit/coqloadpath.ml | 73 ++++++ sysinit/coqloadpath.mli | 16 ++ sysinit/dune | 8 + sysinit/sysinit.mllib | 3 + sysinit/usage.ml | 112 +++++++++ sysinit/usage.mli | 28 +++ toplevel/ccompile.ml | 19 +- toplevel/ccompile.mli | 2 +- toplevel/coqargs.ml | 580 --------------------------------------------- toplevel/coqargs.mli | 81 ------- toplevel/coqc.ml | 11 +- toplevel/coqinit.ml | 111 --------- toplevel/coqinit.mli | 22 -- toplevel/coqrc.ml | 45 ++++ toplevel/coqrc.mli | 11 + toplevel/coqtop.ml | 21 +- toplevel/coqtop.mli | 6 +- toplevel/toplevel.mllib | 4 +- toplevel/usage.ml | 113 --------- toplevel/usage.mli | 29 --- toplevel/workerLoop.ml | 7 +- 36 files changed, 1151 insertions(+), 1073 deletions(-) create mode 100644 stm/stmargs.ml create mode 100644 stm/stmargs.mli create mode 100644 sysinit/coqargs.ml create mode 100644 sysinit/coqargs.mli create mode 100644 sysinit/coqloadpath.ml create mode 100644 sysinit/coqloadpath.mli create mode 100644 sysinit/dune create mode 100644 sysinit/sysinit.mllib create mode 100644 sysinit/usage.ml create mode 100644 sysinit/usage.mli delete mode 100644 toplevel/coqargs.ml delete mode 100644 toplevel/coqargs.mli delete mode 100644 toplevel/coqinit.ml delete mode 100644 toplevel/coqinit.mli create mode 100644 toplevel/coqrc.ml create mode 100644 toplevel/coqrc.mli delete mode 100644 toplevel/usage.ml delete mode 100644 toplevel/usage.mli diff --git a/META.coq.in b/META.coq.in index 68ab0733ee..7a9818da08 100644 --- a/META.coq.in +++ b/META.coq.in @@ -207,10 +207,10 @@ package "vernac" ( package "stm" ( - description = "Coq State Transactional Machine" + description = "Coq State Transaction Machine" version = "8.14" - requires = "coq.vernac" + requires = "coq.sysinit" directory = "stm" archive(byte) = "stm.cma" @@ -218,6 +218,19 @@ package "stm" ( ) +package "sysinit" ( + + description = "Coq initialization" + version = "8.14" + + requires = "coq.vernac" + directory = "sysinit" + + archive(byte) = "sysinit.cma" + archive(native) = "sysinit.cmxa" + +) + package "toplevel" ( description = "Coq Toplevel" diff --git a/Makefile.common b/Makefile.common index 82d9b89c4f..415454df79 100644 --- a/Makefile.common +++ b/Makefile.common @@ -99,7 +99,7 @@ CORESRCDIRS:=\ coqpp \ config clib lib kernel kernel/byterun library \ engine pretyping interp proofs gramlib/.pack parsing printing \ - tactics vernac stm toplevel + tactics vernac stm sysinit toplevel PLUGINDIRS:=\ omega micromega \ @@ -132,7 +132,7 @@ CORECMA:=config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma library/l engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ gramlib/.pack/gramlib.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \ - stm/stm.cma toplevel/toplevel.cma + sysinit/sysinit.cma stm/stm.cma toplevel/toplevel.cma ########################################################################### # plugins object files diff --git a/Makefile.dev b/Makefile.dev index 5825a884c2..cfb02b6d80 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -91,10 +91,11 @@ interp: interp/interp.cma parsing: parsing/parsing.cma pretyping: pretyping/pretyping.cma stm: stm/stm.cma +sysinit: sysinit/sysinit.cma toplevel: toplevel/toplevel.cma .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping -.PHONY: engine stm toplevel +.PHONY: engine stm sysinit toplevel ###################### ### 3) theories files diff --git a/dev/base_include b/dev/base_include index daee2d97c5..f375a867bc 100644 --- a/dev/base_include +++ b/dev/base_include @@ -134,7 +134,6 @@ open ComDefinition open Indschemes open Ind_tables open Auto_ind_decl -open Coqinit open Coqtop open Himsg open Metasyntax diff --git a/dev/dune b/dev/dune index a6d88c94d2..ae801f9e83 100644 --- a/dev/dune +++ b/dev/dune @@ -34,6 +34,7 @@ %{lib:coq.tactics:tactics.cma} %{lib:coq.vernac:vernac.cma} %{lib:coq.stm:stm.cma} + %{lib:coq.sysinit:sysinit.cma} %{lib:coq.toplevel:toplevel.cma} %{lib:coq.plugins.ltac:ltac_plugin.cma} %{lib:coq.top_printers:top_printers.cmi} diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py index 666fb6cc91..a14b98c73c 100755 --- a/dev/tools/update-compat.py +++ b/dev/tools/update-compat.py @@ -64,7 +64,7 @@ DEFAULT_NUMBER_OF_OLD_VERSIONS = 2 RELEASE_NUMBER_OF_OLD_VERSIONS = 2 MASTER_NUMBER_OF_OLD_VERSIONS = 3 EXTRA_HEADER = '\n(** Compatibility file for making Coq act similar to Coq v%s *)\n' -COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml') +COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'sysinit', 'coqargs.ml') DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template') TEST_SUITE_RUN_PATH = os.path.join(ROOT_PATH, 'test-suite', 'tools', 'update-compat', 'run.sh') TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i) diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index 528e2a756b..ed0eb8f34b 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -513,7 +513,7 @@ 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 run_mode ~opts:_ state = +let loop (run_mode,_) ~opts:_ state = match run_mode with | Coqtop.Batch -> exit 0 | Coqtop.Interactive -> @@ -582,23 +582,19 @@ coqidetop specific options:\n\ let islave_parse ~opts extra_args = let open Coqtop in - let run_mode, extra_args = coqtop_toplevel.parse_extra ~opts extra_args in + let (run_mode, stm_opts), 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, [] + (run_mode, stm_opts), [] -let islave_init run_mode ~opts = +let islave_init (run_mode, stm_opts) ~opts = if run_mode = Coqtop.Batch then Flags.quiet := true; - Coqtop.init_toploop opts + Coqtop.init_toploop opts stm_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 islave_default_opts = Coqargs.default let () = let open Coqtop in diff --git a/stm/dune b/stm/dune index c369bd00fb..27d561334e 100644 --- a/stm/dune +++ b/stm/dune @@ -3,4 +3,4 @@ (synopsis "Coq's Document Manager and Proof Checking Scheduler") (public_name coq.stm) (wrapped false) - (libraries vernac)) + (libraries sysinit)) diff --git a/stm/stm.ml b/stm/stm.ml index 27f2b6fc5c..f4e370e7bc 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -297,13 +297,11 @@ end (* }}} *) (*************************** THE DOCUMENT *************************************) (******************************************************************************) -type interactive_top = TopLogical of DirPath.t | TopPhysical of string - (* The main document type associated to a VCS *) type stm_doc_type = | VoDoc of string | VioDoc of string - | Interactive of interactive_top + | Interactive of Coqargs.interactive_top (* Dummy until we land the functional interp patch + fixed start_library *) type doc = int @@ -517,7 +515,7 @@ end = struct (* {{{ *) type vcs = (branch_type, transaction, vcs state_info, box) t let vcs : vcs ref = ref (empty Stateid.dummy) - let doc_type = ref (Interactive (TopLogical (Names.DirPath.make []))) + let doc_type = ref (Interactive (Coqargs.TopLogical (Names.DirPath.make []))) let ldir = ref Names.DirPath.empty let init dt id ps = @@ -2308,23 +2306,6 @@ end (* }}} *) (** STM initialization options: *) -type option_command = - | OptionSet of string option - | OptionAppend of string - | OptionUnset - -type injection_command = - | OptionInjection of (Goptions.option_name * option_command) - (** Set flags or options before the initial state is ready. *) - | RequireInjection of (string * string option * bool option) - (** Require libraries before the initial state is - ready. Parameters follow [Library], that is to say, - [lib,prefix,import_export] means require library [lib] from - optional [prefix] and [import_export] if [Some false/Some true] - is used. *) - (* -load-vernac-source interleaving is not supported yet *) - (* | LoadInjection of (string * bool) *) - type stm_init_options = { doc_type : stm_doc_type (** The STM does set some internal flags differently depending on @@ -2338,7 +2319,7 @@ type stm_init_options = (** [vo] load paths for the document. Usually extracted from -R options / _CoqProject *) - ; injections : injection_command list + ; injections : Coqargs.injection_command list (** Injects Require and Set/Unset commands before the initial state is ready *) @@ -2355,6 +2336,10 @@ let doc_type_module_name (std : stm_doc_type) = | Interactive mn -> Names.DirPath.to_string mn *) +let init_process stm_flags = + Spawned.init_channels (); + CoqworkmgrApi.(init stm_flags.AsyncOpts.async_proofs_worker_priority) + let init_core () = if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true; if !Flags.async_proofs_worker_id = "master" then Partac.enable_par ~nworkers:!cur_opt.async_proofs_n_tacworkers; @@ -2379,44 +2364,10 @@ let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } = let mfrom = Option.map Libnames.qualid_of_string from in Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in - let interp_set_option opt v old = - let open Goptions in - let err expect = - let opt = String.concat " " opt in - let got = v in (* avoid colliding with Pp.v *) - CErrors.user_err - Pp.(str "-set: " ++ str opt ++ - str" expects " ++ str expect ++ - str" but got " ++ str got) - in - match old with - | BoolValue _ -> - let v = match String.trim v with - | "true" -> true - | "false" | "" -> false - | _ -> err "a boolean" - in - BoolValue v - | IntValue _ -> - let v = String.trim v in - let v = match int_of_string_opt v with - | Some _ as v -> v - | None -> if v = "" then None else err "an int" - in - IntValue v - | StringValue _ -> StringValue v - | StringOptValue _ -> StringOptValue (Some v) in - - let set_option = let open Goptions in function - | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt - | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true - | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v - | opt, OptionAppend v -> set_string_option_append_value_gen ~locality:OptLocal opt v in - let handle_injection = function - | RequireInjection r -> require_file r + | Coqargs.RequireInjection r -> require_file r (* | LoadInjection l -> *) - | OptionInjection o -> set_option o in + | Coqargs.OptionInjection o -> Coqargs.set_option o in (* Set the options from the new documents *) AsyncOpts.cur_opt := stm_options; @@ -2437,8 +2388,8 @@ let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } = begin match doc_type with | Interactive ln -> let dp = match ln with - | TopLogical dp -> dp - | TopPhysical f -> dirpath_of_file f + | Coqargs.TopLogical dp -> dp + | Coqargs.TopPhysical f -> dirpath_of_file f in Declaremods.start_library dp diff --git a/stm/stm.mli b/stm/stm.mli index e0c33a309b..dddd63cb52 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -42,32 +42,13 @@ module AsyncOpts : sig end -type interactive_top = TopLogical of DirPath.t | TopPhysical of string - (** The STM document type [stm_doc_type] determines some properties such as what uncompleted proofs are allowed and what gets recorded to aux files. *) type stm_doc_type = | VoDoc of string (* file path *) | VioDoc of string (* file path *) - | Interactive of interactive_top (* module path *) - -type option_command = - | OptionSet of string option - | OptionAppend of string - | OptionUnset - -type injection_command = - | OptionInjection of (Goptions.option_name * option_command) - (** Set flags or options before the initial state is ready. *) - | RequireInjection of (string * string option * bool option) - (** Require libraries before the initial state is - ready. Parameters follow [Library], that is to say, - [lib,prefix,import_export] means require library [lib] from - optional [prefix] and [import_export] if [Some false/Some true] - is used. *) - (* -load-vernac-source interleaving is not supported yet *) - (* | LoadInjection of (string * bool) *) + | Interactive of Coqargs.interactive_top (* module path *) (** STM initialization options: *) type stm_init_options = @@ -83,7 +64,7 @@ type stm_init_options = (** [vo] load paths for the document. Usually extracted from -R options / _CoqProject *) - ; injections : injection_command list + ; injections : Coqargs.injection_command list (** Injects Require and Set/Unset commands before the initial state is ready *) @@ -94,8 +75,10 @@ type stm_init_options = (** The type of a STM document *) type doc -(** [init_core] performs some low-level initialization; should go away - in future releases. *) +(** [init_process] performs some low-level initialization, call early *) +val init_process : AsyncOpts.stm_opt -> unit + +(** [init_core] snapshorts the initial system state *) val init_core : unit -> unit (** [new_doc opt] Creates a new document with options [opt] *) diff --git a/stm/stm.mllib b/stm/stm.mllib index 49e7195e27..a77e0c79e7 100644 --- a/stm/stm.mllib +++ b/stm/stm.mllib @@ -7,5 +7,6 @@ CoqworkmgrApi AsyncTaskQueue Partac Stm +Stmargs ProofBlockDelimiter Vio_checking diff --git a/stm/stmargs.ml b/stm/stmargs.ml new file mode 100644 index 0000000000..609d4f42e9 --- /dev/null +++ b/stm/stmargs.ml @@ -0,0 +1,140 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* "master"); + Flags.async_proofs_worker_id := s + +let get_host_port opt s = + match String.split_on_char ':' s with + | [host; portr; portw] -> + Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) + | ["stdfds"] -> Some Spawned.AnonPipe + | _ -> + Coqargs.error_wrong_arg ("Error: host:portr:portw or stdfds expected after option "^opt) + +let get_error_resilience opt = function + | "on" | "all" | "yes" -> `All + | "off" | "no" -> `None + | s -> `Only (String.split_on_char ',' s) + +let get_priority opt s = + try CoqworkmgrApi.priority_of_string s + with Invalid_argument _ -> + Coqargs.error_wrong_arg ("Error: low/high expected after "^opt) + +let get_async_proofs_mode opt = let open Stm.AsyncOpts in function + | "no" | "off" -> APoff + | "yes" | "on" -> APon + | "lazy" -> APonLazy + | _ -> + Coqargs.error_wrong_arg ("Error: on/off/lazy expected after "^opt) + +let get_cache opt = function + | "force" -> Some Stm.AsyncOpts.Force + | _ -> + Coqargs.error_wrong_arg ("Error: force expected after "^opt) + +let parse_args ~init arglist : Stm.AsyncOpts.stm_opt * string list = + let args = ref arglist in + let extras = ref [] in + let rec parse oval = match !args with + | [] -> + (oval, List.rev !extras) + | opt :: rem -> + args := rem; + let next () = match !args with + | x::rem -> args := rem; x + | [] -> Coqargs.error_missing_arg opt + in + let noval = begin match opt with + + |"-async-proofs" -> + { oval with + Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next()) + } + |"-async-proofs-j" -> + { oval with + Stm.AsyncOpts.async_proofs_n_workers = (Coqargs.get_int ~opt (next ())) + } + |"-async-proofs-cache" -> + { oval with + Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ()) + } + + |"-async-proofs-tac-j" -> + let j = Coqargs.get_int ~opt (next ()) in + if j <= 0 then begin + Coqargs.error_wrong_arg ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1") + end; + { oval with + Stm.AsyncOpts.async_proofs_n_tacworkers = j + } + + |"-async-proofs-worker-priority" -> + { oval with + Stm.AsyncOpts.async_proofs_worker_priority = get_priority opt (next ()) + } + + |"-async-proofs-private-flags" -> + { oval with + Stm.AsyncOpts.async_proofs_private_flags = Some (next ()); + } + + |"-async-proofs-tactic-error-resilience" -> + { oval with + Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ()) + } + + |"-async-proofs-command-error-resilience" -> + { oval with + Stm.AsyncOpts.async_proofs_cmd_error_resilience = Coqargs.get_bool ~opt (next ()) + } + + |"-async-proofs-delegation-threshold" -> + { oval with + Stm.AsyncOpts.async_proofs_delegation_threshold = Coqargs.get_float ~opt (next ()) + } + + |"-worker-id" -> set_worker_id opt (next ()); oval + + |"-main-channel" -> + Spawned.main_channel := get_host_port opt (next()); oval + + |"-control-channel" -> + Spawned.control_channel := get_host_port opt (next()); oval + + (* Options with zero arg *) + |"-async-queries-always-delegate" + |"-async-proofs-always-delegate" + |"-async-proofs-never-reopen-branch" -> + { oval with + Stm.AsyncOpts.async_proofs_never_reopen_branch = true + } + |"-stm-debug" -> Stm.stm_debug := true; oval + (* Unknown option *) + | s -> + extras := s :: !extras; + oval + end in + parse noval + in + try + parse init + with any -> fatal_error any + +let usage = "\ +\n -stm-debug STM debug mode (will trace every transaction)\ +" \ No newline at end of file diff --git a/stm/stmargs.mli b/stm/stmargs.mli new file mode 100644 index 0000000000..f760afdc98 --- /dev/null +++ b/stm/stmargs.mli @@ -0,0 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* string list -> Stm.AsyncOpts.stm_opt * string list + +val usage : string diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml new file mode 100644 index 0000000000..930c3b135f --- /dev/null +++ b/sysinit/coqargs.ml @@ -0,0 +1,515 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* { opts with config = { opts.config with color = `ON }} + | "no" | "off" -> { opts with config = { opts.config with color = `OFF }} + | "auto" -> { opts with config = { opts.config with color = `AUTO }} + | _ -> + error_wrong_arg ("Error: on/off/auto expected after option color") + +let set_query opts q = + { opts with main = match opts.main with + | Run -> Queries (default_queries@[q]) + | Queries queries -> Queries (queries@[q]) + } + +let warn_deprecated_sprop_cumul = + CWarnings.create ~name:"deprecated-spropcumul" ~category:"deprecated" + (fun () -> Pp.strbrk "Use the \"Cumulative StrictProp\" flag instead.") + +let warn_deprecated_inputstate = + CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" + (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") + +let set_inputstate opts s = + warn_deprecated_inputstate (); + { opts with pre = { opts.pre with inputstate = Some s }} + +(******************************************************************************) +(* Parsing helpers *) +(******************************************************************************) +let get_bool ~opt = function + | "yes" | "on" -> true + | "no" | "off" -> false + | _ -> + error_wrong_arg ("Error: yes/no expected after option "^opt) + +let get_int ~opt n = + try int_of_string n + with Failure _ -> + error_wrong_arg ("Error: integer expected after option "^opt) +let get_int_opt ~opt n = + if n = "" then None + else Some (get_int ~opt n) + +let get_float ~opt n = + try float_of_string n + with Failure _ -> + error_wrong_arg ("Error: float expected after option "^opt) + +let get_native_name s = + (* We ignore even critical errors because this mode has to be super silent *) + try + Filename.(List.fold_left concat (dirname s) + [ !Nativelib.output_dir + ; Library.native_name_from_filename s + ]) + with _ -> "" + +let interp_set_option opt v old = + let open Goptions in + let opt = String.concat " " opt in + match old with + | BoolValue _ -> BoolValue (get_bool ~opt v) + | IntValue _ -> IntValue (get_int_opt ~opt v) + | StringValue _ -> StringValue v + | StringOptValue _ -> StringOptValue (Some v) + +let set_option = let open Goptions in function + | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt + | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true + | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v + | opt, OptionAppend v -> set_string_option_append_value_gen ~locality:OptLocal opt v + +let get_compat_file = function + | "8.14" -> "Coq.Compat.Coq814" + | "8.13" -> "Coq.Compat.Coq813" + | "8.12" -> "Coq.Compat.Coq812" + | "8.11" -> "Coq.Compat.Coq811" + | ("8.10" | "8.9" | "8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> + CErrors.user_err ~hdr:"get_compat_file" + Pp.(str "Compatibility with version " ++ str s ++ str " not supported.") + | s -> + CErrors.user_err ~hdr:"get_compat_file" + Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".") + +let to_opt_key = Str.(split (regexp " +")) + +let parse_option_set opt = + match String.index_opt opt '=' with + | None -> to_opt_key opt, None + | Some eqi -> + let len = String.length opt in + let v = String.sub opt (eqi+1) (len - eqi - 1) in + to_opt_key (String.sub opt 0 eqi), Some v + +let warn_no_native_compiler = + CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler" + Pp.(fun s -> strbrk "Native compiler is disabled," ++ + strbrk " -native-compiler " ++ strbrk s ++ + strbrk " option ignored.") + +let get_native_compiler s = + (* We use two boolean flags because the four states make sense, even if + only three are accessible to the user at the moment. The selection of the + produced artifact(s) (`.vo`, `.vio`, `.coq-native`, ...) should be done by + a separate flag, and the "ondemand" value removed. Once this is done, use + [get_bool] here. *) + let n = match s with + | ("yes" | "on") -> NativeOn {ondemand=false} + | "ondemand" -> NativeOn {ondemand=true} + | ("no" | "off") -> NativeOff + | _ -> + error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") in + if Coq_config.native_compiler = NativeOff && n <> NativeOff then + let () = warn_no_native_compiler s in + NativeOff + else + n + +(* Main parsing routine *) +(*s Parsing of the command line *) + +let parse_args ~help ~init arglist : t * string list = + let args = ref arglist in + let extras = ref [] in + let rec parse oval = match !args with + | [] -> + (oval, List.rev !extras) + | opt :: rem -> + args := rem; + let next () = match !args with + | x::rem -> args := rem; x + | [] -> error_missing_arg opt + in + let noval = begin match opt with + + (* Complex options with many args *) + |"-I"|"-include" -> + begin match rem with + | d :: rem -> + args := rem; + add_ml_include oval d + | [] -> error_missing_arg opt + end + |"-Q" -> + begin match rem with + | d :: p :: rem -> + args := rem; + add_vo_include oval d p false + | _ -> error_missing_arg opt + end + |"-R" -> + begin match rem with + | d :: p :: rem -> + args := rem; + add_vo_include oval d p true + | _ -> error_missing_arg opt + end + + (* Options with one arg *) + |"-coqlib" -> + { oval with config = { oval.config with coqlib = Some (next ()) + }} + + |"-compat" -> + add_vo_require oval (get_compat_file (next ())) None (Some false) + + |"-exclude-dir" -> + System.exclude_directory (next ()); oval + + |"-init-file" -> + { oval with config = { oval.config with rcfile = Some (next ()); }} + + |"-inputstate"|"-is" -> + set_inputstate oval (next ()) + + |"-load-vernac-object" -> + add_vo_require oval (next ()) None None + + |"-load-vernac-source"|"-l" -> + add_load_vernacular oval false (next ()) + + |"-load-vernac-source-verbose"|"-lv" -> + add_load_vernacular oval true (next ()) + + |"-mangle-names" -> + Goptions.set_bool_option_value ["Mangle"; "Names"] true; + Goptions.set_string_option_value ["Mangle"; "Names"; "Prefix"] (next ()); + oval + + |"-print-mod-uid" -> + let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 + + |"-profile-ltac-cutoff" -> + Flags.profile_ltac := true; + Flags.profile_ltac_cutoff := get_float ~opt (next ()); + oval + + |"-rfrom" -> + let from = next () in add_vo_require oval (next ()) (Some from) None + + |"-require-import" | "-ri" -> add_vo_require oval (next ()) None (Some false) + + |"-require-export" | "-re" -> add_vo_require oval (next ()) None (Some true) + + |"-require-import-from" | "-rifrom" -> + let from = next () in add_vo_require oval (next ()) (Some from) (Some false) + + |"-require-export-from" | "-refrom" -> + let from = next () in add_vo_require oval (next ()) (Some from) (Some true) + + |"-top" -> + let topname = Libnames.dirpath_of_string (next ()) in + if Names.DirPath.is_empty topname then + CErrors.user_err Pp.(str "Need a non empty toplevel module name"); + { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = TopLogical topname }}} + + |"-topfile" -> + { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = TopPhysical (next()) }}} + + |"-w" | "-W" -> + let w = next () in + if w = "none" then add_set_option oval ["Warnings"] (OptionSet(Some w)) + else add_set_option oval ["Warnings"] (OptionAppend w) + + |"-bytecode-compiler" -> + { oval with config = { oval.config with enable_VM = get_bool ~opt (next ()) }} + + |"-native-compiler" -> + let native_compiler = get_native_compiler (next ()) in + { oval with config = { oval.config with native_compiler }} + + | "-set" -> + let opt, v = parse_option_set @@ next() in + add_set_option oval opt (OptionSet v) + + | "-unset" -> + add_set_option oval (to_opt_key @@ next ()) OptionUnset + + |"-native-output-dir" -> + let native_output_dir = next () in + { oval with config = { oval.config with native_output_dir } } + + |"-nI" -> + let include_dir = next () in + { oval with config = {oval.config with native_include_dirs = include_dir :: oval.config.native_include_dirs } } + + (* Options with zero arg *) + |"-test-mode" -> Vernacinterp.test_mode := true; oval + |"-beautify" -> Flags.beautify := true; oval + |"-bt" -> Exninfo.record_backtrace true; oval + |"-color" -> set_color oval (next ()) + |"-config"|"--config" -> set_query oval PrintConfig + |"-debug" -> set_debug (); oval + |"-xml-debug" -> Flags.xml_debug := true; set_debug (); oval + |"-diffs" -> + add_set_option oval Proof_diffs.opt_name @@ OptionSet (Some (next ())) + |"-emacs" -> set_emacs oval + |"-impredicative-set" -> + set_logic (fun o -> { o with impredicative_set = Declarations.ImpredicativeSet }) oval + |"-allow-sprop" -> + add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None) + |"-disallow-sprop" -> + add_set_option oval Vernacentries.allow_sprop_opt_name OptionUnset + |"-sprop-cumulative" -> + warn_deprecated_sprop_cumul(); + add_set_option oval Vernacentries.cumul_sprop_opt_name (OptionSet None) + |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval + |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }} + |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }} + |"-boot" -> { oval with pre = { oval.pre with boot = true }} + |"-output-context" -> { oval with post = { oval.post with output_context = true }} + |"-profile-ltac" -> Flags.profile_ltac := true; oval + |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }} + |"-quiet"|"-silent" -> + Flags.quiet := true; + Flags.make_warn false; + oval + |"-list-tags" -> set_query oval PrintTags + |"-time" -> { oval with config = { oval.config with time = true }} + |"-type-in-type" -> set_type_in_type (); oval + |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) + |"-where" -> set_query oval PrintWhere + |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp help) + |"-v"|"--version" -> set_query oval PrintVersion + |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion + + (* Unknown option *) + | s -> + extras := s :: !extras; + oval + end in + parse noval + in + try + parse init + with any -> fatal_error any + +(* We need to reverse a few lists *) +let parse_args ~help ~init args = + let opts, extra = parse_args ~help ~init args in + let opts = + { opts with + pre = { opts.pre with + ml_includes = List.rev opts.pre.ml_includes + ; vo_includes = List.rev opts.pre.vo_includes + ; load_vernacular_list = List.rev opts.pre.load_vernacular_list + ; injections = List.rev opts.pre.injections + } + } in + opts, extra + +(******************************************************************************) +(* Startup LoadPath and Modules *) +(******************************************************************************) +(* prelude_data == From Coq Require Import Prelude. *) +let prelude_data = "Prelude", Some "Coq", Some false + +let injection_commands opts = + if opts.pre.load_init then RequireInjection prelude_data :: opts.pre.injections else opts.pre.injections + +let build_load_path opts = + let ml_path, vo_path = + if opts.pre.boot then [],[] + else + let coqlib = Envars.coqlib () in + Coqloadpath.init_load_path ~coqlib in + ml_path @ opts.pre.ml_includes , + vo_path @ opts.pre.vo_includes diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli new file mode 100644 index 0000000000..894e0f2ef3 --- /dev/null +++ b/sysinit/coqargs.mli @@ -0,0 +1,107 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* init:t -> string list -> t * string list + +val injection_commands : t -> injection_command list +val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list + +(* Common utilities *) + +val get_int : opt:string -> string -> int +val get_int_opt : opt:string -> string -> int option +val get_bool : opt:string -> string -> bool +val get_float : opt:string -> string -> float +val error_missing_arg : string -> 'a +val error_wrong_arg : string -> 'a + +val set_option : Goptions.option_name * option_command -> unit \ No newline at end of file diff --git a/sysinit/coqloadpath.ml b/sysinit/coqloadpath.ml new file mode 100644 index 0000000000..8635345e00 --- /dev/null +++ b/sysinit/coqloadpath.ml @@ -0,0 +1,73 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* List.map fst in + let vo_path = + { unix_path + ; coq_path = Libnames.default_root_prefix + ; has_ml = false + ; implicit = false + ; recursive = true + } in + ml_path, [vo_path] + else [], [] + +(* LoadPath for Coq user libraries *) +let init_load_path ~coqlib = + + let open Loadpath in + let user_contrib = coqlib/"user-contrib" in + let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in + let coqpath = Envars.coqpath in + let coq_path = Names.DirPath.make [Libnames.coq_root] in + + (* ML includes *) + let plugins_dirs = System.all_subdirs ~unix_path:(coqlib/"plugins") |> List.map fst in + + let contrib_ml, contrib_vo = build_userlib_path ~unix_path:user_contrib in + + let misc_ml, misc_vo = + List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) |> List.split in + + let ml_loadpath = plugins_dirs @ contrib_ml @ List.concat misc_ml in + let vo_loadpath = + (* current directory (not recursively!) *) + [ { unix_path = "." + ; coq_path = Libnames.default_root_prefix + ; implicit = false + ; has_ml = true + ; recursive = false + } ] @ + + (* then standard library *) + [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @ + + (* then user-contrib *) + contrib_vo @ + + (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *) + List.concat misc_vo + in + ml_loadpath, vo_loadpath diff --git a/sysinit/coqloadpath.mli b/sysinit/coqloadpath.mli new file mode 100644 index 0000000000..d853e9ea54 --- /dev/null +++ b/sysinit/coqloadpath.mli @@ -0,0 +1,16 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* CUnix.physical_path list * Loadpath.vo_path list diff --git a/sysinit/dune b/sysinit/dune new file mode 100644 index 0000000000..6146aa60d0 --- /dev/null +++ b/sysinit/dune @@ -0,0 +1,8 @@ +(library + (name sysinit) + (public_name coq.sysinit) + (synopsis "Coq's initialization") + (wrapped false) + (libraries coq.vernac) + (modules coqloadpath coqargs usage) + ) diff --git a/sysinit/sysinit.mllib b/sysinit/sysinit.mllib new file mode 100644 index 0000000000..9d35a931bc --- /dev/null +++ b/sysinit/sysinit.mllib @@ -0,0 +1,3 @@ +Usage +Coqloadpath +Coqargs diff --git a/sysinit/usage.ml b/sysinit/usage.ml new file mode 100644 index 0000000000..1831a3f9b2 --- /dev/null +++ b/sysinit/usage.ml @@ -0,0 +1,112 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* set the output directory for native objects\ +\n -nI dir OCaml include directories for the native compiler (default if not set) \ +\n -h, -help, --help print this list of options\ +\n" + +(* print the usage *) + +type specific_usage = { + executable_name : string; + extra_args : string; + extra_options : string; +} + +let print_usage co { executable_name; extra_args; extra_options } = + print_usage_common co ("Usage: " ^ executable_name ^ " " ^ extra_args ^ "\n\n"); + output_string co extra_options diff --git a/sysinit/usage.mli b/sysinit/usage.mli new file mode 100644 index 0000000000..2d1a8e94cc --- /dev/null +++ b/sysinit/usage.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* unit +val machine_readable_version : unit -> unit + +(** {6 extra arguments or options to print when asking usage for a + given executable. } *) + +type specific_usage = { + executable_name : string; + extra_args : string; + extra_options : string; +} + +(** {6 Prints the generic part and specific part of usage for a + given executable. } *) + +val print_usage : out_channel -> specific_usage -> unit diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index b75a4199ea..4747abceb5 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -24,7 +24,7 @@ let fatal_error msg = let load_init_file opts ~state = if opts.pre.load_rcfile then Topfmt.(in_phase ~phase:LoadingRcFile) (fun () -> - Coqinit.load_rcfile ~rcfile:opts.config.rcfile ~state) () + Coqrc.load_rcfile ~rcfile:opts.config.rcfile ~state) () else begin Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); state @@ -93,7 +93,7 @@ let create_empty_file filename = close_out f (* Compile a vernac file *) -let compile opts copts ~echo ~f_in ~f_out = +let compile opts stm_options copts ~echo ~f_in ~f_out = let open Vernac.State in let check_pending_proofs () = let pfs = Vernacstate.Declare.get_all_proof_names () [@ocaml.warning "-3"] in @@ -106,7 +106,6 @@ let compile opts copts ~echo ~f_in ~f_out = in let ml_load_path, vo_load_path = build_load_path opts in let injections = injection_commands opts in - 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 @@ -209,22 +208,22 @@ let compile opts copts ~echo ~f_in ~f_out = dump_empty_vos(); create_empty_file (long_f_dot_out ^ "k") -let compile opts copts ~echo ~f_in ~f_out = +let compile opts stm_opts copts ~echo ~f_in ~f_out = ignore(CoqworkmgrApi.get 1); - compile opts copts ~echo ~f_in ~f_out; + compile opts stm_opts copts ~echo ~f_in ~f_out; CoqworkmgrApi.giveback 1 -let compile_file opts copts (f_in, echo) = +let compile_file opts stm_opts copts (f_in, echo) = let f_out = copts.compilation_output_name in if !Flags.beautify then Flags.with_option Flags.beautify_file - (fun f_in -> compile opts copts ~echo ~f_in ~f_out) f_in + (fun f_in -> compile opts stm_opts copts ~echo ~f_in ~f_out) f_in else - compile opts copts ~echo ~f_in ~f_out + compile opts stm_opts copts ~echo ~f_in ~f_out -let compile_files opts copts = +let compile_files (opts, stm_opts) copts = let compile_list = copts.compile_list in - List.iter (compile_file opts copts) compile_list + List.iter (compile_file opts stm_opts copts) compile_list (******************************************************************************) (* VIO Dispatching *) diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli index 8c154488d0..1b670a8edc 100644 --- a/toplevel/ccompile.mli +++ b/toplevel/ccompile.mli @@ -13,7 +13,7 @@ val load_init_vernaculars : Coqargs.t -> state:Vernac.State.t-> Vernac.State.t (** [compile_files opts] compile files specified in [opts] *) -val compile_files : Coqargs.t -> Coqcargs.t -> unit +val compile_files : Coqargs.t * Stm.AsyncOpts.stm_opt -> Coqcargs.t -> unit (** [do_vio opts] process [.vio] files in [opts] *) val do_vio : Coqargs.t -> Coqcargs.t -> unit diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml deleted file mode 100644 index c114c43e26..0000000000 --- a/toplevel/coqargs.ml +++ /dev/null @@ -1,580 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* "master"); - Flags.async_proofs_worker_id := s - -let set_type_in_type () = - let typing_flags = Environ.typing_flags (Global.env ()) in - Global.set_typing_flags { typing_flags with Declarations.check_universes = false } - -(******************************************************************************) - -type color = [`ON | `AUTO | `EMACS | `OFF] - -type native_compiler = Coq_config.native_compiler = - NativeOff | NativeOn of { ondemand : bool } - -type coqargs_logic_config = { - impredicative_set : Declarations.set_predicativity; - indices_matter : bool; - toplevel_name : Stm.interactive_top; -} - -type coqargs_config = { - logic : coqargs_logic_config; - rcfile : string option; - coqlib : string option; - color : color; - enable_VM : bool; - native_compiler : native_compiler; - native_output_dir : CUnix.physical_path; - native_include_dirs : CUnix.physical_path list; - stm_flags : Stm.AsyncOpts.stm_opt; - debug : bool; - time : bool; - print_emacs : bool; -} - -type coqargs_pre = { - boot : bool; - load_init : bool; - load_rcfile : bool; - - ml_includes : string list; - vo_includes : Loadpath.vo_path list; - - load_vernacular_list : (string * bool) list; - injections : Stm.injection_command list; - - inputstate : string option; -} - -type coqargs_query = - | PrintTags | PrintWhere | PrintConfig - | PrintVersion | PrintMachineReadableVersion - | PrintHelp of Usage.specific_usage - -type coqargs_main = - | Queries of coqargs_query list - | Run - -type coqargs_post = { - memory_stat : bool; - output_context : bool; -} - -type t = { - config : coqargs_config; - pre : coqargs_pre; - main : coqargs_main; - post : coqargs_post; -} - -let default_toplevel = Names.(DirPath.make [Id.of_string "Top"]) - -let default_native = Coq_config.native_compiler - -let default_logic_config = { - impredicative_set = Declarations.PredicativeSet; - indices_matter = false; - toplevel_name = Stm.TopLogical default_toplevel; -} - -let default_config = { - logic = default_logic_config; - rcfile = None; - coqlib = None; - color = `AUTO; - enable_VM = true; - native_compiler = default_native; - native_output_dir = ".coq-native"; - native_include_dirs = []; - stm_flags = Stm.AsyncOpts.default_opts; - debug = false; - time = false; - print_emacs = false; - - (* Quiet / verbosity options should be here *) -} - -let default_pre = { - boot = false; - load_init = true; - load_rcfile = true; - ml_includes = []; - vo_includes = []; - load_vernacular_list = []; - injections = []; - inputstate = None; -} - -let default_queries = [] - -let default_post = { - memory_stat = false; - output_context = false; -} - -let default = { - config = default_config; - pre = default_pre; - main = Run; - post = default_post; -} - -(******************************************************************************) -(* Functional arguments *) -(******************************************************************************) -let add_ml_include opts s = - { opts with pre = { opts.pre with ml_includes = s :: opts.pre.ml_includes }} - -let add_vo_include opts unix_path coq_path implicit = - let open Loadpath in - let coq_path = Libnames.dirpath_of_string coq_path in - { opts with pre = { opts.pre with vo_includes = { - unix_path; coq_path; has_ml = false; implicit; recursive = true } :: opts.pre.vo_includes }} - -let add_vo_require opts d p export = - { opts with pre = { opts.pre with injections = Stm.RequireInjection (d, p, export) :: opts.pre.injections }} - -let add_load_vernacular opts verb s = - { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }} - -let add_set_option opts opt_name value = - { opts with pre = { opts.pre with injections = Stm.OptionInjection (opt_name, value) :: opts.pre.injections }} - -(** Options for proof general *) -let set_emacs opts = - Goptions.set_bool_option_value Printer.print_goal_tag_opt_name true; - { opts with config = { opts.config with color = `EMACS; print_emacs = true }} - -let set_logic f oval = - { oval with config = { oval.config with logic = f oval.config.logic }} - -let set_color opts = function - | "yes" | "on" -> { opts with config = { opts.config with color = `ON }} - | "no" | "off" -> { opts with config = { opts.config with color = `OFF }} - | "auto" -> { opts with config = { opts.config with color = `AUTO }} - | _ -> - error_wrong_arg ("Error: on/off/auto expected after option color") - -let set_query opts q = - { opts with main = match opts.main with - | Run -> Queries (default_queries@[q]) - | Queries queries -> Queries (queries@[q]) - } - -let warn_deprecated_sprop_cumul = - CWarnings.create ~name:"deprecated-spropcumul" ~category:"deprecated" - (fun () -> Pp.strbrk "Use the \"Cumulative StrictProp\" flag instead.") - -let warn_deprecated_inputstate = - CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" - (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") - -let set_inputstate opts s = - warn_deprecated_inputstate (); - { opts with pre = { opts.pre with inputstate = Some s }} - -(******************************************************************************) -(* Parsing helpers *) -(******************************************************************************) -let get_bool opt = function - | "yes" | "on" -> true - | "no" | "off" -> false - | _ -> - error_wrong_arg ("Error: yes/no expected after option "^opt) - -let get_int opt n = - try int_of_string n - with Failure _ -> - error_wrong_arg ("Error: integer expected after option "^opt) - -let get_float opt n = - try float_of_string n - with Failure _ -> - error_wrong_arg ("Error: float expected after option "^opt) - -let get_host_port opt s = - match String.split_on_char ':' s with - | [host; portr; portw] -> - Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) - | ["stdfds"] -> Some Spawned.AnonPipe - | _ -> - error_wrong_arg ("Error: host:portr:portw or stdfds expected after option "^opt) - -let get_error_resilience opt = function - | "on" | "all" | "yes" -> `All - | "off" | "no" -> `None - | s -> `Only (String.split_on_char ',' s) - -let get_priority opt s = - try CoqworkmgrApi.priority_of_string s - with Invalid_argument _ -> - error_wrong_arg ("Error: low/high expected after "^opt) - -let get_async_proofs_mode opt = let open Stm.AsyncOpts in function - | "no" | "off" -> APoff - | "yes" | "on" -> APon - | "lazy" -> APonLazy - | _ -> - error_wrong_arg ("Error: on/off/lazy expected after "^opt) - -let get_cache opt = function - | "force" -> Some Stm.AsyncOpts.Force - | _ -> - error_wrong_arg ("Error: force expected after "^opt) - - -let get_native_name s = - (* We ignore even critical errors because this mode has to be super silent *) - try - Filename.(List.fold_left concat (dirname s) - [ !Nativelib.output_dir - ; Library.native_name_from_filename s - ]) - with _ -> "" - -let get_compat_file = function - | "8.14" -> "Coq.Compat.Coq814" - | "8.13" -> "Coq.Compat.Coq813" - | "8.12" -> "Coq.Compat.Coq812" - | "8.11" -> "Coq.Compat.Coq811" - | ("8.10" | "8.9" | "8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> - CErrors.user_err ~hdr:"get_compat_file" - Pp.(str "Compatibility with version " ++ str s ++ str " not supported.") - | s -> - CErrors.user_err ~hdr:"get_compat_file" - Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".") - -let to_opt_key = Str.(split (regexp " +")) - -let parse_option_set opt = - match String.index_opt opt '=' with - | None -> to_opt_key opt, None - | Some eqi -> - let len = String.length opt in - let v = String.sub opt (eqi+1) (len - eqi - 1) in - to_opt_key (String.sub opt 0 eqi), Some v - -let warn_no_native_compiler = - CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler" - Pp.(fun s -> strbrk "Native compiler is disabled," ++ - strbrk " -native-compiler " ++ strbrk s ++ - strbrk " option ignored.") - -let get_native_compiler s = - (* We use two boolean flags because the four states make sense, even if - only three are accessible to the user at the moment. The selection of the - produced artifact(s) (`.vo`, `.vio`, `.coq-native`, ...) should be done by - a separate flag, and the "ondemand" value removed. Once this is done, use - [get_bool] here. *) - let n = match s with - | ("yes" | "on") -> NativeOn {ondemand=false} - | "ondemand" -> NativeOn {ondemand=true} - | ("no" | "off") -> NativeOff - | _ -> - error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") in - if Coq_config.native_compiler = NativeOff && n <> NativeOff then - let () = warn_no_native_compiler s in - NativeOff - else - n - -(* Main parsing routine *) -(*s Parsing of the command line *) - -let parse_args ~help ~init arglist : t * string list = - let args = ref arglist in - let extras = ref [] in - let rec parse oval = match !args with - | [] -> - (oval, List.rev !extras) - | opt :: rem -> - args := rem; - let next () = match !args with - | x::rem -> args := rem; x - | [] -> error_missing_arg opt - in - let noval = begin match opt with - - (* Complex options with many args *) - |"-I"|"-include" -> - begin match rem with - | d :: rem -> - args := rem; - add_ml_include oval d - | [] -> error_missing_arg opt - end - |"-Q" -> - begin match rem with - | d :: p :: rem -> - args := rem; - add_vo_include oval d p false - | _ -> error_missing_arg opt - end - |"-R" -> - begin match rem with - | d :: p :: rem -> - args := rem; - add_vo_include oval d p true - | _ -> error_missing_arg opt - end - - (* Options with one arg *) - |"-coqlib" -> - { oval with config = { oval.config with coqlib = Some (next ()) - }} - - |"-async-proofs" -> - { 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 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 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 config = { oval.config with stm_flags = { oval.config.stm_flags with - Stm.AsyncOpts.async_proofs_n_tacworkers = j - }}} - - |"-async-proofs-worker-priority" -> - { 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 - Stm.AsyncOpts.async_proofs_private_flags = Some (next ()); - }}} - - |"-async-proofs-tactic-error-resilience" -> - { 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 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 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 - - |"-compat" -> - add_vo_require oval (get_compat_file (next ())) None (Some false) - - |"-exclude-dir" -> - System.exclude_directory (next ()); oval - - |"-init-file" -> - { oval with config = { oval.config with rcfile = Some (next ()); }} - - |"-inputstate"|"-is" -> - set_inputstate oval (next ()) - - |"-load-vernac-object" -> - add_vo_require oval (next ()) None None - - |"-load-vernac-source"|"-l" -> - add_load_vernacular oval false (next ()) - - |"-load-vernac-source-verbose"|"-lv" -> - add_load_vernacular oval true (next ()) - - |"-mangle-names" -> - Goptions.set_bool_option_value ["Mangle"; "Names"] true; - Goptions.set_string_option_value ["Mangle"; "Names"; "Prefix"] (next ()); - oval - - |"-print-mod-uid" -> - let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 - - |"-profile-ltac-cutoff" -> - Flags.profile_ltac := true; - Flags.profile_ltac_cutoff := get_float opt (next ()); - oval - - |"-rfrom" -> - let from = next () in add_vo_require oval (next ()) (Some from) None - - |"-require-import" | "-ri" -> add_vo_require oval (next ()) None (Some false) - - |"-require-export" | "-re" -> add_vo_require oval (next ()) None (Some true) - - |"-require-import-from" | "-rifrom" -> - let from = next () in add_vo_require oval (next ()) (Some from) (Some false) - - |"-require-export-from" | "-refrom" -> - let from = next () in add_vo_require oval (next ()) (Some from) (Some true) - - |"-top" -> - let topname = Libnames.dirpath_of_string (next ()) in - if Names.DirPath.is_empty topname then - CErrors.user_err Pp.(str "Need a non empty toplevel module name"); - { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = Stm.TopLogical topname }}} - - |"-topfile" -> - { 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 - - |"-control-channel" -> - Spawned.control_channel := get_host_port opt (next()); oval - - |"-w" | "-W" -> - let w = next () in - if w = "none" then add_set_option oval ["Warnings"] (Stm.OptionSet(Some w)) - else add_set_option oval ["Warnings"] (Stm.OptionAppend w) - - |"-bytecode-compiler" -> - { oval with config = { oval.config with enable_VM = get_bool opt (next ()) }} - - |"-native-compiler" -> - let native_compiler = get_native_compiler (next ()) in - { oval with config = { oval.config with native_compiler }} - - | "-set" -> - let opt, v = parse_option_set @@ next() in - add_set_option oval opt (Stm.OptionSet v) - - | "-unset" -> - add_set_option oval (to_opt_key @@ next ()) Stm.OptionUnset - - |"-native-output-dir" -> - let native_output_dir = next () in - { oval with config = { oval.config with native_output_dir } } - - |"-nI" -> - let include_dir = next () in - { oval with config = {oval.config with native_include_dirs = include_dir :: oval.config.native_include_dirs } } - - (* Options with zero arg *) - |"-async-queries-always-delegate" - |"-async-proofs-always-delegate" - |"-async-proofs-never-reopen-branch" -> - { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with - Stm.AsyncOpts.async_proofs_never_reopen_branch = true - }}} - |"-test-mode" -> Vernacinterp.test_mode := true; oval - |"-beautify" -> Flags.beautify := true; oval - |"-bt" -> Exninfo.record_backtrace true; oval - |"-color" -> set_color oval (next ()) - |"-config"|"--config" -> set_query oval PrintConfig - |"-debug" -> Coqinit.set_debug (); oval - |"-xml-debug" -> Flags.xml_debug := true; Coqinit.set_debug (); oval - |"-diffs" -> - add_set_option oval Proof_diffs.opt_name @@ Stm.OptionSet (Some (next ())) - |"-stm-debug" -> Stm.stm_debug := true; oval - |"-emacs" -> set_emacs oval - |"-impredicative-set" -> - set_logic (fun o -> { o with impredicative_set = Declarations.ImpredicativeSet }) oval - |"-allow-sprop" -> - add_set_option oval Vernacentries.allow_sprop_opt_name (Stm.OptionSet None) - |"-disallow-sprop" -> - add_set_option oval Vernacentries.allow_sprop_opt_name Stm.OptionUnset - |"-sprop-cumulative" -> - warn_deprecated_sprop_cumul(); - add_set_option oval Vernacentries.cumul_sprop_opt_name (Stm.OptionSet None) - |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval - |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }} - |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }} - |"-boot" -> { oval with pre = { oval.pre with boot = true }} - |"-output-context" -> { oval with post = { oval.post with output_context = true }} - |"-profile-ltac" -> Flags.profile_ltac := true; oval - |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }} - |"-quiet"|"-silent" -> - Flags.quiet := true; - Flags.make_warn false; - oval - |"-list-tags" -> set_query oval PrintTags - |"-time" -> { oval with config = { oval.config with time = true }} - |"-type-in-type" -> set_type_in_type (); oval - |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) - |"-where" -> set_query oval PrintWhere - |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp help) - |"-v"|"--version" -> set_query oval PrintVersion - |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion - - (* Unknown option *) - | s -> - extras := s :: !extras; - oval - end in - parse noval - in - try - parse init - with any -> fatal_error any - -(* We need to reverse a few lists *) -let parse_args ~help ~init args = - let opts, extra = parse_args ~help ~init args in - let opts = - { opts with - pre = { opts.pre with - ml_includes = List.rev opts.pre.ml_includes - ; vo_includes = List.rev opts.pre.vo_includes - ; load_vernacular_list = List.rev opts.pre.load_vernacular_list - ; injections = List.rev opts.pre.injections - } - } in - opts, extra - -(******************************************************************************) -(* Startup LoadPath and Modules *) -(******************************************************************************) -(* prelude_data == From Coq Require Import Prelude. *) -let prelude_data = "Prelude", Some "Coq", Some false - -let injection_commands opts = - if opts.pre.load_init then Stm.RequireInjection prelude_data :: opts.pre.injections else opts.pre.injections - -let build_load_path opts = - let ml_path, vo_path = - if opts.pre.boot then [],[] - else - let coqlib = Envars.coqlib () in - Coqinit.libs_init_load_path ~coqlib in - ml_path @ opts.pre.ml_includes , - vo_path @ opts.pre.vo_includes diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli deleted file mode 100644 index f6222e4ec4..0000000000 --- a/toplevel/coqargs.mli +++ /dev/null @@ -1,81 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* init:t -> string list -> t * string list -val error_wrong_arg : string -> unit - -val injection_commands : t -> Stm.injection_command list -val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 03c53d6991..0c23c9f4e9 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -41,9 +41,9 @@ coqc specific options:\ \n" } -let coqc_main copts ~opts = +let coqc_main (copts,stm_opts) ~opts = Topfmt.(in_phase ~phase:CompilationPhase) - Ccompile.compile_files opts copts; + Ccompile.compile_files (opts,stm_opts) copts; (* Careful this will modify the load-path and state so after this point some stuff may not be safe anymore. *) @@ -73,8 +73,11 @@ let coqc_run copts ~opts () = 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, []); +let custom_coqc : (Coqcargs.t * Stm.AsyncOpts.stm_opt, 'b) Coqtop.custom_toplevel + = Coqtop.{ + parse_extra = (fun ~opts extras -> + let stm_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in + (Coqcargs.parse extras, stm_opts), []); help = coqc_specific_usage; init = coqc_init; run = coqc_run; diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml deleted file mode 100644 index 501047c520..0000000000 --- a/toplevel/coqinit.ml +++ /dev/null @@ -1,111 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* - if CUnix.file_readable_p rcfile then - Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state rcfile - else raise (Sys_error ("Cannot read rcfile: "^ rcfile)) - | None -> - try - let warn x = Feedback.msg_warning (str x) in - let inferedrc = List.find CUnix.file_readable_p [ - Envars.xdg_config_home warn / rcdefaultname^"."^Coq_config.version; - Envars.xdg_config_home warn / rcdefaultname; - Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version; - Envars.home ~warn / "."^rcdefaultname - ] in - Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state inferedrc - with Not_found -> state - (* - Flags.if_verbose - mSGNL (str ("No coqrc or coqrc."^Coq_config.version^ - " found. Skipping rcfile loading.")) - *) - with reraise -> - let reraise = Exninfo.capture reraise in - let () = Feedback.msg_info (str"Load of rcfile failed.") in - Exninfo.iraise reraise - -(* Recursively puts `.v` files in the LoadPath *) -let build_stdlib_vo_path ~unix_path ~coq_path = - let open Loadpath in - { unix_path; coq_path ; has_ml = false; implicit = true; recursive = true } - -(* Note we don't use has_ml=true due to #12771 , we need to see if we - should just remove that option *) -let build_userlib_path ~unix_path = - let open Loadpath in - if Sys.file_exists unix_path then - let ml_path = System.all_subdirs ~unix_path |> List.map fst in - let vo_path = - { unix_path - ; coq_path = Libnames.default_root_prefix - ; has_ml = false - ; implicit = false - ; recursive = true - } in - ml_path, [vo_path] - else [], [] - -(* LoadPath for Coq user libraries *) -let libs_init_load_path ~coqlib = - - let open Loadpath in - let user_contrib = coqlib/"user-contrib" in - let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in - let coqpath = Envars.coqpath in - let coq_path = Names.DirPath.make [Libnames.coq_root] in - - (* ML includes *) - let plugins_dirs = System.all_subdirs ~unix_path:(coqlib/"plugins") |> List.map fst in - - let contrib_ml, contrib_vo = build_userlib_path ~unix_path:user_contrib in - - let misc_ml, misc_vo = - List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) |> List.split in - - let ml_loadpath = plugins_dirs @ contrib_ml @ List.concat misc_ml in - let vo_loadpath = - (* current directory (not recursively!) *) - [ { unix_path = "." - ; coq_path = Libnames.default_root_prefix - ; implicit = false - ; has_ml = true - ; recursive = false - } ] @ - - (* then standard library *) - [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @ - - (* then user-contrib *) - contrib_vo @ - - (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *) - List.concat misc_vo - in - ml_loadpath, vo_loadpath diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli deleted file mode 100644 index b96a0ef162..0000000000 --- a/toplevel/coqinit.mli +++ /dev/null @@ -1,22 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* unit - -val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State.t - -(** Standard LoadPath for Coq user libraries; in particular it - includes (in-order) Coq's standard library, Coq's [user-contrib] - folder, and directories specified in [COQPATH] and [XDG_DIRS] *) -val libs_init_load_path - : coqlib:CUnix.physical_path - -> CUnix.physical_path list * Loadpath.vo_path list diff --git a/toplevel/coqrc.ml b/toplevel/coqrc.ml new file mode 100644 index 0000000000..e074e621da --- /dev/null +++ b/toplevel/coqrc.ml @@ -0,0 +1,45 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* + if CUnix.file_readable_p rcfile then + Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state rcfile + else raise (Sys_error ("Cannot read rcfile: "^ rcfile)) + | None -> + try + let warn x = Feedback.msg_warning (Pp.str x) in + let inferedrc = List.find CUnix.file_readable_p [ + Envars.xdg_config_home warn / rcdefaultname^"."^Coq_config.version; + Envars.xdg_config_home warn / rcdefaultname; + Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version; + Envars.home ~warn / "."^rcdefaultname + ] in + Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state inferedrc + with Not_found -> state + (* + Flags.if_verbose + mSGNL (str ("No coqrc or coqrc."^Coq_config.version^ + " found. Skipping rcfile loading.")) + *) + with reraise -> + let reraise = Exninfo.capture reraise in + let () = Feedback.msg_info (Pp.str"Load of rcfile failed.") in + Exninfo.iraise reraise diff --git a/toplevel/coqrc.mli b/toplevel/coqrc.mli new file mode 100644 index 0000000000..3b8a31b2a5 --- /dev/null +++ b/toplevel/coqrc.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* state:Vernac.State.t -> Vernac.State.t diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index d0d50aee70..7596df788b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -198,11 +198,7 @@ let init_parse parse_extra help init_opts = (** Coq's init process, phase 2: Basic Coq environment, plugins. *) let init_execution opts custom_init = - (* 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 (); if opts.post.memory_stat then at_exit print_memory_stat; - 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; @@ -241,10 +237,11 @@ let init_toplevel custom = | Queries q -> List.iter (print_query opts) q; exit 0 | Run -> let () = init_coqlib opts in + Stm.init_process (snd customopts); let customstate = init_execution opts (custom.init customopts) in opts, customopts, customstate -let init_document opts = +let init_document opts stm_options = (* Coq init process, phase 3: Stm initialization, backtracking state. It is essential that the module system is in a consistent @@ -255,7 +252,6 @@ let init_document opts = Flags.load_vos_libraries := true; let ml_load_path, vo_load_path = build_load_path opts in let injections = injection_commands opts in - let stm_options = opts.config.stm_flags in let open Vernac.State in let doc, sid = Stm.(new_doc @@ -281,16 +277,16 @@ let start_coq custom = type run_mode = Interactive | Batch -let init_toploop opts = - let state = init_document opts in +let init_toploop opts stm_opts = + let state = init_document opts stm_opts in let state = Ccompile.load_init_vernaculars opts ~state in state -let coqtop_init run_mode ~opts = +let coqtop_init (run_mode,stm_opts) ~opts = if run_mode = Batch then Flags.quiet := true; init_color opts.config; Flags.if_verbose print_header (); - init_toploop opts + init_toploop opts stm_opts let coqtop_parse_extra ~opts extras = let rec parse_extra run_mode = function @@ -299,9 +295,10 @@ let coqtop_parse_extra ~opts extras = 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 stm_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in + (run_mode, stm_opts), extras -let coqtop_run run_mode ~opts state = +let coqtop_run (run_mode,_) ~opts state = match run_mode with | Interactive -> Coqloop.loop ~opts ~state; | Batch -> exit 0 diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index e535c19252..9ae0d86cf1 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -28,7 +28,7 @@ type ('a,'b) custom_toplevel = 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 : ('a,'b) custom_toplevel -> unit +val start_coq : ('a * Stm.AsyncOpts.stm_opt,'b) custom_toplevel -> unit (** Initializer color for output *) @@ -36,10 +36,10 @@ val init_color : Coqargs.coqargs_config -> unit (** Prepare state for interactive loop *) -val init_toploop : Coqargs.t -> Vernac.State.t +val init_toploop : Coqargs.t -> Stm.AsyncOpts.stm_opt -> Vernac.State.t (** The specific characterization of the coqtop_toplevel *) type run_mode = Interactive | Batch -val coqtop_toplevel : (run_mode,Vernac.State.t) custom_toplevel +val coqtop_toplevel : (run_mode * Stm.AsyncOpts.stm_opt,Vernac.State.t) custom_toplevel diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index ddd11fd160..90f8fb9686 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -1,7 +1,5 @@ Vernac -Usage -Coqinit -Coqargs +Coqrc Coqcargs G_toplevel Coqloop diff --git a/toplevel/usage.ml b/toplevel/usage.ml deleted file mode 100644 index 6fb5f821ee..0000000000 --- a/toplevel/usage.ml +++ /dev/null @@ -1,113 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* set the output directory for native objects\ -\n -nI dir OCaml include directories for the native compiler (default if not set) \ -\n -h, -help, --help print this list of options\ -\n" - -(* print the usage *) - -type specific_usage = { - executable_name : string; - extra_args : string; - extra_options : string; -} - -let print_usage co { executable_name; extra_args; extra_options } = - print_usage_common co ("Usage: " ^ executable_name ^ " " ^ extra_args ^ "\n\n"); - output_string co extra_options diff --git a/toplevel/usage.mli b/toplevel/usage.mli deleted file mode 100644 index cbc3b4f7e8..0000000000 --- a/toplevel/usage.mli +++ /dev/null @@ -1,29 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* unit -val machine_readable_version : unit -> unit - -(** {6 extra arguments or options to print when asking usage for a - given executable. } *) - -type specific_usage = { - executable_name : string; - extra_args : string; - extra_options : string; -} - -(** {6 Prints the generic part and specific part of usage for a - given executable. } *) - -val print_usage : out_channel -> specific_usage -> unit - diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index 59e10b09a0..b0d7bb6f78 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -9,9 +9,10 @@ (************************************************************************) let worker_parse_extra ~opts extra_args = - (), extra_args + let stm_opts, extra_args = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extra_args in + ((),stm_opts), extra_args -let worker_init init () ~opts = +let worker_init init ((),_) ~opts = Flags.quiet := true; init (); Coqtop.init_toploop opts @@ -30,6 +31,6 @@ let start ~init ~loop name = help = worker_specific_usage name; opts = Coqargs.default; init = worker_init init; - run = (fun () ~opts:_ _state (* why is state not used *) -> loop ()); + run = (fun ((),_) ~opts:_ _state (* why is state not used *) -> loop ()); } in start_coq custom -- cgit v1.2.3