From b44fce96503c39a4306a627e5ba992634728954d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 14 Feb 2020 00:49:01 +0100 Subject: [loadpath] Rework and simplify ML loadpath handling This PR refactors the handling of ML loadpaths to get it closer to what (as of 2020) the standard OCaml toolchain (ocamlfind, dune) does. This is motivated as I am leaning toward letting the standard OCaml machinery handle OCaml includes; this has several benefits [for example plugins become regular OCaml libs] It will also help in improving dependency handling in plugin dynload. The main change is that "recursive" ML loadpaths are no longer supported, so Coq's `-I` option becomes closer to OCaml's semantics. We still allow `-Q` to extend the OCaml path recursively, but this may become deprecated in the future if we decide to install the ML parts of plugins in the standard OCaml location. Due to this `Loadpath` still hooks into `Mltop`, but other than that `.v` location handling is actually very close to become fully independent of Coq [thus it can be used in other tools such coqdep, the build system, etc...] In terms of vernaculars the changes are: - The `Add Rec ML Path` command has been removed, - The `Add Loadpath "foo".` has been removed. We now require that the form with the explicit prefix `Add Loadpath "foo" as Prefix.` is used. We did modify `fake_ide` as not to add a directory with the empty `Prefix`, which was not used. This exposed some bugs in the implementation of the document model, which relied on having an initial sentence; we have workarounded them just by adding a dummy one in the two relevant cases. --- stm/stm.ml | 8 +++++--- stm/stm.mli | 3 ++- 2 files changed, 7 insertions(+), 4 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 95c58b9043..6312bff5f3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2578,7 +2578,8 @@ type stm_init_options = { (* Initial load path in scope for the document. Usually extracted from -R options / _CoqProject *) - iload_path : Loadpath.coq_path list; + ml_load_path : CUnix.physical_path list; + vo_load_path : Loadpath.vo_path list; (* Require [require_libs] before the initial state is ready. Parameters follow [Library], that is to say, @@ -2615,7 +2616,7 @@ let dirpath_of_file f = let ldir = Libnames.add_dirpath_suffix ldir0 id in ldir -let new_doc { doc_type ; iload_path; require_libs; stm_options } = +let new_doc { doc_type ; ml_load_path; vo_load_path; require_libs; stm_options } = let require_file (dir, from, exp) = let mp = Libnames.qualid_of_string dir in @@ -2633,7 +2634,8 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = (* Set load path; important, this has to happen before we declare the library below as [Declaremods/Library] will infer the module name by looking at the load path! *) - List.iter Loadpath.add_coq_path iload_path; + List.iter Mltop.add_ml_dir ml_load_path; + List.iter Loadpath.add_vo_path vo_load_path; Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff; diff --git a/stm/stm.mli b/stm/stm.mli index 841adcf05b..e242225cf2 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -71,7 +71,8 @@ type stm_init_options = { (* Initial load path in scope for the document. Usually extracted from -R options / _CoqProject *) - iload_path : Loadpath.coq_path list; + ml_load_path : CUnix.physical_path list; + vo_load_path : Loadpath.vo_path list; (* Require [require_libs] before the initial state is ready. Parameters follow [Library], that is to say, -- cgit v1.2.3 From 8de81cf2b6059e1e5aa84ea483dba38e42b35792 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 20 Feb 2020 11:52:24 -0500 Subject: [stm] Port documentation of init options to ocamldoc --- stm/stm.ml | 39 +++++++++++++++++++++------------------ stm/stm.mli | 47 +++++++++++++++++++---------------------------- 2 files changed, 40 insertions(+), 46 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 6312bff5f3..109ac2d8b4 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2569,29 +2569,32 @@ end (* }}} *) (********************************* STM API ************************************) (******************************************************************************) -(* Main initialization routine *) -type stm_init_options = { - (* The STM will set some internal flags differently depending on the - specified [doc_type]. This distinction should disappear at some - some point. *) - doc_type : stm_doc_type; - - (* Initial load path in scope for the document. Usually extracted - from -R options / _CoqProject *) - ml_load_path : CUnix.physical_path list; - vo_load_path : Loadpath.vo_path list; - - (* Require [require_libs] before the initial state is +(** STM initialization options: *) +type stm_init_options = + { doc_type : stm_doc_type + (** The STM does set some internal flags differently depending on + the specified [doc_type]. This distinction should disappear at + some some point. *) + + ; ml_load_path : CUnix.physical_path list + (** OCaml load paths for the document. *) + + ; vo_load_path : Loadpath.vo_path list + (** [vo] load paths for the document. Usually extracted from -R + options / _CoqProject *) + + ; require_libs : (string * string option * bool option) list + (** Require [require_libs] 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. *) - require_libs : (string * string option * bool option) list; - (* STM options that apply to the current document. *) - stm_options : AsyncOpts.stm_opt; -} -(* fb_handler : Feedback.feedback -> unit; *) + ; stm_options : AsyncOpts.stm_opt + (** Low-level STM options *) + } + + (* fb_handler : Feedback.feedback -> unit; *) (* let doc_type_module_name (std : stm_doc_type) = diff --git a/stm/stm.mli b/stm/stm.mli index e242225cf2..e56bac6e0f 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -52,39 +52,30 @@ type stm_doc_type = | VioDoc of string (* file path *) | Interactive of interactive_top (* module path *) -(** Coq initialization options: - - - [doc_type]: Type of document being created. - - - [require_libs]: list of libraries/modules to be pre-loaded at - startup. A tuple [(modname,modfrom,import)] is equivalent to [From - modfrom Require modname]; [import] works similarly to - [Library.require_library_from_dirpath], [Some false] will import - the module, [Some true] will additionally export it. - -*) -type stm_init_options = { - (* The STM will set some internal flags differently depending on the - specified [doc_type]. This distinction should disappear at some - some point. *) - doc_type : stm_doc_type; - - (* Initial load path in scope for the document. Usually extracted - from -R options / _CoqProject *) - ml_load_path : CUnix.physical_path list; - vo_load_path : Loadpath.vo_path list; - - (* Require [require_libs] before the initial state is +(** STM initialization options: *) +type stm_init_options = + { doc_type : stm_doc_type + (** The STM does set some internal flags differently depending on + the specified [doc_type]. This distinction should disappear at + some some point. *) + + ; ml_load_path : CUnix.physical_path list + (** OCaml load paths for the document. *) + + ; vo_load_path : Loadpath.vo_path list + (** [vo] load paths for the document. Usually extracted from -R + options / _CoqProject *) + + ; require_libs : (string * string option * bool option) list + (** Require [require_libs] 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. *) - require_libs : (string * string option * bool option) list; - (* STM options that apply to the current document. *) - stm_options : AsyncOpts.stm_opt; -} -(* fb_handler : Feedback.feedback -> unit; *) + ; stm_options : AsyncOpts.stm_opt + (** Low-level STM options *) + } (** The type of a STM document *) type doc -- cgit v1.2.3