diff options
| -rw-r--r-- | META.coq.in | 17 | ||||
| -rw-r--r-- | Makefile.common | 4 | ||||
| -rw-r--r-- | Makefile.dev | 3 | ||||
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rw-r--r-- | dev/dune | 1 | ||||
| -rwxr-xr-x | dev/tools/update-compat.py | 2 | ||||
| -rw-r--r-- | ide/coqide/idetop.ml | 16 | ||||
| -rw-r--r-- | stm/dune | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 71 | ||||
| -rw-r--r-- | stm/stm.mli | 29 | ||||
| -rw-r--r-- | stm/stm.mllib | 1 | ||||
| -rw-r--r-- | stm/stmargs.ml | 140 | ||||
| -rw-r--r-- | stm/stmargs.mli | 13 | ||||
| -rw-r--r-- | sysinit/coqargs.ml (renamed from toplevel/coqargs.ml) | 179 | ||||
| -rw-r--r-- | sysinit/coqargs.mli (renamed from toplevel/coqargs.mli) | 36 | ||||
| -rw-r--r-- | sysinit/coqloadpath.ml (renamed from toplevel/coqinit.ml) | 40 | ||||
| -rw-r--r-- | sysinit/coqloadpath.mli (renamed from toplevel/coqinit.mli) | 8 | ||||
| -rw-r--r-- | sysinit/dune | 8 | ||||
| -rw-r--r-- | sysinit/sysinit.mllib | 3 | ||||
| -rw-r--r-- | sysinit/usage.ml (renamed from toplevel/usage.ml) | 1 | ||||
| -rw-r--r-- | sysinit/usage.mli (renamed from toplevel/usage.mli) | 1 | ||||
| -rw-r--r-- | toplevel/ccompile.ml | 19 | ||||
| -rw-r--r-- | toplevel/ccompile.mli | 2 | ||||
| -rw-r--r-- | toplevel/coqc.ml | 11 | ||||
| -rw-r--r-- | toplevel/coqrc.ml | 45 | ||||
| -rw-r--r-- | toplevel/coqrc.mli | 11 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 21 | ||||
| -rw-r--r-- | toplevel/coqtop.mli | 6 | ||||
| -rw-r--r-- | toplevel/toplevel.mllib | 4 | ||||
| -rw-r--r-- | toplevel/workerLoop.ml | 7 |
30 files changed, 390 insertions, 312 deletions
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 @@ -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 @@ -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 *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +let fatal_error exn = + Topfmt.(in_phase ~phase:ParsingCommandLine print_err_exn exn); + let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in + exit exit_code + +let set_worker_id opt s = + assert (s <> "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 *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val parse_args : init:Stm.AsyncOpts.stm_opt -> string list -> Stm.AsyncOpts.stm_opt * string list + +val usage : string diff --git a/toplevel/coqargs.ml b/sysinit/coqargs.ml index c114c43e26..930c3b135f 100644 --- a/toplevel/coqargs.ml +++ b/sysinit/coqargs.ml @@ -24,14 +24,15 @@ let error_missing_arg s = (******************************************************************************) (* Imperative effects! This must be fixed at some point. *) (******************************************************************************) -let set_worker_id opt s = - assert (s <> "master"); - Flags.async_proofs_worker_id := s let set_type_in_type () = let typing_flags = Environ.typing_flags (Global.env ()) in Global.set_typing_flags { typing_flags with Declarations.check_universes = false } +let set_debug () = + let () = Exninfo.record_backtrace true in + Flags.debug := true + (******************************************************************************) type color = [`ON | `AUTO | `EMACS | `OFF] @@ -39,10 +40,21 @@ type color = [`ON | `AUTO | `EMACS | `OFF] type native_compiler = Coq_config.native_compiler = NativeOff | NativeOn of { ondemand : bool } +type interactive_top = TopLogical of Names.DirPath.t | TopPhysical of string + +type option_command = + | OptionSet of string option + | OptionUnset + | OptionAppend of string + +type injection_command = + | OptionInjection of (Goptions.option_name * option_command) + | RequireInjection of (string * string option * bool option) + type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; - toplevel_name : Stm.interactive_top; + toplevel_name : interactive_top; } type coqargs_config = { @@ -54,7 +66,6 @@ type coqargs_config = { 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; @@ -69,7 +80,7 @@ type coqargs_pre = { vo_includes : Loadpath.vo_path list; load_vernacular_list : (string * bool) list; - injections : Stm.injection_command list; + injections : injection_command list; inputstate : string option; } @@ -102,7 +113,7 @@ let default_native = Coq_config.native_compiler let default_logic_config = { impredicative_set = Declarations.PredicativeSet; indices_matter = false; - toplevel_name = Stm.TopLogical default_toplevel; + toplevel_name = TopLogical default_toplevel; } let default_config = { @@ -114,7 +125,6 @@ let default_config = { 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; @@ -160,13 +170,13 @@ let add_vo_include opts unix_path coq_path implicit = 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 }} + { opts with pre = { opts.pre with injections = 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 }} + { opts with pre = { opts.pre with injections = OptionInjection (opt_name, value) :: opts.pre.injections }} (** Options for proof general *) let set_emacs opts = @@ -204,53 +214,25 @@ let set_inputstate opts s = (******************************************************************************) (* Parsing helpers *) (******************************************************************************) -let get_bool opt = function +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 = +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 = +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 @@ -260,6 +242,21 @@ let get_native_name 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" @@ -351,55 +348,6 @@ let parse_args ~help ~init arglist : t * string list = { 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) @@ -431,7 +379,7 @@ let parse_args ~help ~init arglist : t * string list = |"-profile-ltac-cutoff" -> Flags.profile_ltac := true; - Flags.profile_ltac_cutoff := get_float opt (next ()); + Flags.profile_ltac_cutoff := get_float ~opt (next ()); oval |"-rfrom" -> @@ -451,24 +399,18 @@ 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 config = { oval.config with logic = { oval.config.logic with toplevel_name = Stm.TopLogical topname }}} + { 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 = 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 + { 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"] (Stm.OptionSet(Some w)) - else add_set_option oval ["Warnings"] (Stm.OptionAppend w) + 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 ()) }} + { oval with config = { oval.config with enable_VM = get_bool ~opt (next ()) }} |"-native-compiler" -> let native_compiler = get_native_compiler (next ()) in @@ -476,10 +418,10 @@ let parse_args ~help ~init arglist : t * string list = | "-set" -> let opt, v = parse_option_set @@ next() in - add_set_option oval opt (Stm.OptionSet v) + add_set_option oval opt (OptionSet v) | "-unset" -> - add_set_option oval (to_opt_key @@ next ()) Stm.OptionUnset + add_set_option oval (to_opt_key @@ next ()) OptionUnset |"-native-output-dir" -> let native_output_dir = next () in @@ -490,32 +432,25 @@ let parse_args ~help ~init arglist : t * string list = { 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 + |"-debug" -> set_debug (); oval + |"-xml-debug" -> Flags.xml_debug := true; set_debug (); oval |"-diffs" -> - add_set_option oval Proof_diffs.opt_name @@ Stm.OptionSet (Some (next ())) - |"-stm-debug" -> Stm.stm_debug := true; oval + 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 (Stm.OptionSet None) + add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None) |"-disallow-sprop" -> - add_set_option oval Vernacentries.allow_sprop_opt_name Stm.OptionUnset + 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 (Stm.OptionSet None) + 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 }} @@ -568,13 +503,13 @@ let parse_args ~help ~init args = 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 + 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 - Coqinit.libs_init_load_path ~coqlib in + Coqloadpath.init_load_path ~coqlib in ml_path @ opts.pre.ml_includes , vo_path @ opts.pre.vo_includes diff --git a/toplevel/coqargs.mli b/sysinit/coqargs.mli index f6222e4ec4..894e0f2ef3 100644 --- a/toplevel/coqargs.mli +++ b/sysinit/coqargs.mli @@ -15,10 +15,27 @@ val default_toplevel : Names.DirPath.t type native_compiler = Coq_config.native_compiler = NativeOff | NativeOn of { ondemand : bool } +type interactive_top = TopLogical of Names.DirPath.t | TopPhysical of string + +type option_command = + | OptionSet of string option + | OptionUnset + | OptionAppend of string + +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. *) + type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; - toplevel_name : Stm.interactive_top; + toplevel_name : interactive_top; } type coqargs_config = { @@ -30,7 +47,6 @@ type coqargs_config = { 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; @@ -45,7 +61,7 @@ type coqargs_pre = { vo_includes : Loadpath.vo_path list; load_vernacular_list : (string * bool) list; - injections : Stm.injection_command list; + injections : injection_command list; inputstate : string option; } @@ -75,7 +91,17 @@ type t = { val default : t val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * string list -val error_wrong_arg : string -> unit -val injection_commands : t -> Stm.injection_command 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/toplevel/coqinit.ml b/sysinit/coqloadpath.ml index 501047c520..8635345e00 100644 --- a/toplevel/coqinit.ml +++ b/sysinit/coqloadpath.ml @@ -13,44 +13,6 @@ open Pp let ( / ) s1 s2 = Filename.concat s1 s2 -let set_debug () = - let () = Exninfo.record_backtrace true in - Flags.debug := true - -(* Loading of the resource file. - rcfile is either $XDG_CONFIG_HOME/.coqrc.VERSION, or $XDG_CONFIG_HOME/.coqrc if the first one - does not exist. *) - -let rcdefaultname = "coqrc" - -let load_rcfile ~rcfile ~state = - try - match rcfile with - | Some rcfile -> - 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 @@ -73,7 +35,7 @@ let build_userlib_path ~unix_path = else [], [] (* LoadPath for Coq user libraries *) -let libs_init_load_path ~coqlib = +let init_load_path ~coqlib = let open Loadpath in let user_contrib = coqlib/"user-contrib" in diff --git a/toplevel/coqinit.mli b/sysinit/coqloadpath.mli index b96a0ef162..d853e9ea54 100644 --- a/toplevel/coqinit.mli +++ b/sysinit/coqloadpath.mli @@ -8,15 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Initialization. *) - -val set_debug : unit -> 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 +val init_load_path : coqlib:CUnix.physical_path -> 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/toplevel/usage.ml b/sysinit/usage.ml index 6fb5f821ee..1831a3f9b2 100644 --- a/toplevel/usage.ml +++ b/sysinit/usage.ml @@ -74,7 +74,6 @@ let print_usage_common co command = \n -debug debug mode (implies -bt)\ \n -xml-debug debug mode and print XML messages to/from coqide\ \n -diffs (on|off|removed) highlight differences between proof steps\ -\n -stm-debug STM debug mode (will trace every transaction)\ \n -noglob do not dump globalizations\ \n -dump-glob f dump globalizations in file f (to be used by coqdoc)\ \n -impredicative-set set sort Set impredicative\ diff --git a/toplevel/usage.mli b/sysinit/usage.mli index cbc3b4f7e8..2d1a8e94cc 100644 --- a/toplevel/usage.mli +++ b/sysinit/usage.mli @@ -26,4 +26,3 @@ type specific_usage = { 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/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/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 *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +let ( / ) s1 s2 = Filename.concat s1 s2 + +(* Loading of the resource file. + rcfile is either $XDG_CONFIG_HOME/.coqrc.VERSION, or $XDG_CONFIG_HOME/.coqrc if the first one + does not exist. *) + +let rcdefaultname = "coqrc" + +let load_rcfile ~rcfile ~state = + try + match rcfile with + | Some rcfile -> + 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 *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val load_rcfile : rcfile:(string option) -> 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/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 |