From c13213ced52f8f1383d5bed9c5a826d111603318 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 31 Jan 2018 04:55:52 +0100 Subject: [stm] [toplevel] Make loadpath a parameter of the document. We allow to provide a Coq load path at document creation time. This is natural as the document naming process is sensible to a particular load path, thus clarifying this API point. The changes are minimal, as #6663 did most of the work here. The only point of interest is that we have split the initial load path into two components: - a ML-only load path that is used to locate "plugable" toplevels. - the normal loadpath that includes `theories` and `user-contrib`, command line options, etc... --- toplevel/coqinit.ml | 22 +++++++++++++--------- toplevel/coqinit.mli | 7 ++++++- toplevel/coqtop.ml | 35 +++++++++++++++++++++++++---------- 3 files changed, 44 insertions(+), 20 deletions(-) (limited to 'toplevel') diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index b3b5375bf..10205964a 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -89,22 +89,26 @@ let ml_path_if c p = let f x = { recursive = false; path_spec = MlPath x } in if c then List.map f p else [] -(* Initializes the LoadPath *) -let init_load_path ~load_init = - let open Mltop in +(* LoadPath for toploop toplevels *) +let toplevel_init_load_path () = let coqlib = Envars.coqlib () 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 - (* NOTE: These directories are searched from last to first *) (* first, developer specific directory to open *) ml_path_if Coq_config.local [coqlib/"dev"] @ (* main loops *) ml_path_if (Coq_config.local || !Flags.boot) [coqlib/"stm"; coqlib/"ide"] @ - ml_path_if (System.exists_dir (coqlib/"toploop")) [coqlib/"toploop"] @ + ml_path_if (System.exists_dir (coqlib/"toploop")) [coqlib/"toploop"] + +(* LoadPath for Coq user libraries *) +let libs_init_load_path ~load_init = + + let open Mltop in + let coqlib = Envars.coqlib () 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 (* then standard library and plugins *) [build_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path ~with_ml:false; diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 089847f5d..0d2da84bb 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -19,5 +19,10 @@ val push_include : string -> Names.DirPath.t -> bool -> unit (** [push_include phys_path log_path implicit] *) val push_ml_include : string -> unit -val init_load_path : load_init:bool -> Mltop.coq_path list + val init_ocaml_path : unit -> unit + +(* LoadPath for toploop toplevels *) +val toplevel_init_load_path : unit -> Mltop.coq_path list +(* LoadPath for Coq user libraries *) +val libs_init_load_path : load_init:bool -> Mltop.coq_path list diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index bf090862f..400f7048d 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -304,6 +304,9 @@ let compile ~time ~verbosely ~f_in ~f_out = |> prlist_with_sep pr_comma Names.Id.print) ++ str ".") in + let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in + let require_libs = require_libs () in + let stm_options = !top_stm_options in match !compilation_mode with | BuildVo -> Flags.record_aux_file := true; @@ -316,8 +319,9 @@ let compile ~time ~verbosely ~f_in ~f_out = let doc, sid = Stm.(new_doc { doc_type = VoDoc long_f_dot_vo; - require_libs = require_libs (); - stm_options = !top_stm_options; + iload_path; + require_libs; + stm_options; }) in let doc, sid = load_init_vernaculars ~time doc sid in @@ -352,8 +356,9 @@ let compile ~time ~verbosely ~f_in ~f_out = let doc, sid = Stm.(new_doc { doc_type = VioDoc long_f_dot_vio; - require_libs = require_libs (); - stm_options = !top_stm_options; + iload_path; + require_libs; + stm_options; }) in let doc, sid = load_init_vernaculars ~time doc sid in @@ -424,7 +429,12 @@ let set_vio_checking_j opt j = prerr_endline "setting the J variable like in 'make vio2vo J=3'"; exit 1 -let schedule_vio opts = +let schedule_vio () = + (* We must add update the loadpath here as the scheduling process + happens outside of the STM *) + let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in + List.iter Mltop.add_coq_path iload_path; + if !vio_checking then Vio_checking.schedule_vio_checking !vio_files_j !vio_files else @@ -494,7 +504,8 @@ let usage batch = try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib) with NoCoqLib -> usage_no_coqlib () end; - let lp = Coqinit.init_load_path ~load_init:!load_init in + let lp = Coqinit.toplevel_init_load_path () in + (* Necessary for finding the toplevels below *) List.iter Mltop.add_coq_path lp; if batch then Usage.print_usage_coqc () else begin @@ -808,8 +819,8 @@ let init_toplevel arglist = if !print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode ())); if !print_tags then (print_style_tags (); exit (exitcode ())); if !filter_opts then (print_string (String.concat "\n" extras); exit 0); - let lp = Coqinit.init_load_path ~load_init:!load_init in - List.iter Mltop.add_coq_path lp; + let top_lp = Coqinit.toplevel_init_load_path () in + List.iter Mltop.add_coq_path top_lp; Option.iter Mltop.load_ml_object_raw !toploop; let extras = !toploop_init extras in if not (CList.is_empty extras) then begin @@ -845,11 +856,15 @@ let init_toplevel arglist = || CList.(is_empty !compile_list && is_empty !vio_files && is_empty !vio_tasks)) (* Interactive *) then begin + let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in + let require_libs = require_libs () in + let stm_options = !top_stm_options in try let doc, sid = Stm.(new_doc { doc_type = Interactive !toplevel_name; - require_libs = require_libs (); - stm_options = !top_stm_options; + iload_path; + require_libs; + stm_options; }) in Some (load_init_vernaculars ~time:!measure_time doc sid) with any -> flush_all(); fatal_error any -- cgit v1.2.3