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 --- stm/dune | 2 +- stm/stm.ml | 71 +++++----------------------- stm/stm.mli | 29 +++--------- stm/stm.mllib | 1 + stm/stmargs.ml | 140 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ stm/stmargs.mli | 13 ++++++ 6 files changed, 172 insertions(+), 84 deletions(-) create mode 100644 stm/stmargs.ml create mode 100644 stm/stmargs.mli (limited to 'stm') 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 -- cgit v1.2.3