diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-02-06 14:15:19 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-06 14:15:19 +0100 |
commit | b1d56e48b2453814a5d2898688fbc7c5d29d32fa (patch) | |
tree | 4fc10644e5db337a6d931ad1a26974a34399b97e /stm | |
parent | 5ac5ba83b7527f29b6a00c51806d4842b2e22e44 (diff) | |
parent | c13213ced52f8f1383d5bed9c5a826d111603318 (diff) |
Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.
Diffstat (limited to 'stm')
-rw-r--r-- | stm/stm.ml | 33 | ||||
-rw-r--r-- | stm/stm.mli | 21 |
2 files changed, 42 insertions, 12 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 1b649194d..b5848c662 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2532,16 +2532,28 @@ end (* }}} *) (********************************* STM API ************************************) (******************************************************************************) +(* Main initalization routine *) type stm_init_options = { + (* The STM will set some internal flags differently depending on the + specified [doc_type]. This distinction should dissappear at some + some point. *) doc_type : stm_doc_type; + + (* Initial load path in scope for the document. Usually extracted + from -R options / _CoqProject *) + iload_path : Mltop.coq_path 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; - iload_path : (string list * string * bool) list; - implicit_std : bool; -*) } +(* fb_handler : Feedback.feedback -> unit; *) (* let doc_type_module_name (std : stm_doc_type) = @@ -2554,7 +2566,7 @@ let init_core () = if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true; State.register_root_state () -let new_doc { doc_type ; stm_options; require_libs } = +let new_doc { doc_type ; iload_path; require_libs; stm_options } = let load_objs libs = let rq_file (dir, from, exp) = @@ -2572,6 +2584,11 @@ let new_doc { doc_type ; stm_options; require_libs } = let doc = VCS.init doc_type Stateid.initial in + (* 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 Mltop.add_coq_path iload_path; + begin match doc_type with | Interactive ln -> Safe_typing.allow_delayed_constants := true; @@ -2588,9 +2605,11 @@ let new_doc { doc_type ; stm_options; require_libs } = VCS.set_ldir ldir; set_compilation_hints ln end; + + (* Import initial libraries. *) load_objs require_libs; - (* We record the state here! *) + (* We record the state at this point! *) State.define ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial; Backtrack.record (); Slaves.init (); diff --git a/stm/stm.mli b/stm/stm.mli index 8b5581979..8a4de34b4 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -46,15 +46,26 @@ type stm_doc_type = (* Main initalization routine *) type stm_init_options = { + (* The STM will set some internal flags differently depending on the + specified [doc_type]. This distinction should dissappear at some + some point. *) doc_type : stm_doc_type; + + (* Initial load path in scope for the document. Usually extracted + from -R options / _CoqProject *) + iload_path : Mltop.coq_path 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; - iload_path : (string list * string * bool) list; - implicit_std : bool; -*) } +(* fb_handler : Feedback.feedback -> unit; *) (** The type of a STM document *) type doc |