From 1ee761a2b315970a0169c1e99f4729f11ac1eea1 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 29 Jan 2018 03:18:56 +0100 Subject: [toplevel] Refactor load path handling. We refactor top-level load path handling. This is in preparation to make load paths become local to a particular document. To this effect, we introduce a new data type `coq_path` that includes the full specification of a load path: ``` type add_ml = AddNoML | AddTopML | AddRecML type vo_path_spec = { unix_path : string; (* Filesystem path contaning vo/ml files *) coq_path : Names.DirPath.t; (* Coq prefix for the path *) implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *) has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *) } type coq_path_spec = | VoPath of vo_path_spec | MlPath of string type coq_path = { path_spec: coq_path_spec; recursive: bool; } ``` Then, initialization of load paths is split into building a list of load paths and actually making them effective. A future commit will make thus the list of load paths a parameter for document creation. This API is necessarily internal [for now] thus I don't think a changes entry is needed. --- toplevel/coqinit.ml | 106 +++++++++++++++++++++++++++++++-------------------- toplevel/coqinit.mli | 4 +- toplevel/coqtop.ml | 11 +++--- 3 files changed, 72 insertions(+), 49 deletions(-) (limited to 'toplevel') diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 176dfb3c9..b3b5375bf 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -59,13 +59,23 @@ let load_rcfile ~time doc sid = doc, sid) (* Recursively puts dir in the LoadPath if -nois was not passed *) -let add_stdlib_path ~load_init ~unix_path ~coq_root ~with_ml = - let add_ml = if with_ml then Mltop.AddRecML else Mltop.AddNoML in - Mltop.add_rec_path add_ml ~unix_path ~coq_root ~implicit:load_init +let build_stdlib_path ~load_init ~unix_path ~coq_path ~with_ml = + let open Mltop in + let add_ml = if with_ml then AddRecML else AddNoML in + { recursive = true; + path_spec = VoPath { unix_path; coq_path ; has_ml = add_ml; implicit = load_init } + } -let add_userlib_path ~unix_path = - Mltop.add_rec_path Mltop.AddRecML ~unix_path - ~coq_root:Libnames.default_root_prefix ~implicit:false +let build_userlib_path ~unix_path = + let open Mltop in + { recursive = true; + path_spec = VoPath { + unix_path; + coq_path = Libnames.default_root_prefix; + has_ml = Mltop.AddRecML; + implicit = false; + } + } (* Options -I, -I-as, and -R of the command line *) let includes = ref [] @@ -74,51 +84,65 @@ let push_include s alias implicit = let ml_includes = ref [] let push_ml_include s = ml_includes := s :: !ml_includes +let ml_path_if c p = + let open Mltop in + 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 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_root = Names.DirPath.make [Libnames.coq_root] in - (* NOTE: These directories are searched from last to first *) - (* first, developer specific directory to open *) - if Coq_config.local then - Mltop.add_ml_dir (coqlib/"dev"); - (* main loops *) - if Coq_config.local || !Flags.boot then begin - Mltop.add_ml_dir (coqlib/"stm"); - Mltop.add_ml_dir (coqlib/"ide") - end; - if System.exists_dir (coqlib/"toploop") then - Mltop.add_ml_dir (coqlib/"toploop"); - (* then standard library *) - add_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false; - (* then plugins *) - add_stdlib_path ~load_init ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:true; - (* then user-contrib *) - if Sys.file_exists user_contrib then - add_userlib_path ~unix_path:user_contrib; - (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *) - List.iter (fun s -> add_userlib_path ~unix_path:s) xdg_dirs; - (* then directories in COQPATH *) - List.iter (fun s -> add_userlib_path ~unix_path:s) coqpath; - (* then current directory (not recursively!) *) - Mltop.add_ml_dir "."; - Loadpath.add_load_path "." Libnames.default_root_prefix ~implicit:false; - (* additional loadpath, given with options -Q and -R *) - List.iter - (fun (unix_path, coq_root, implicit) -> - Mltop.add_rec_path Mltop.AddNoML ~unix_path ~coq_root ~implicit) - (List.rev !includes); - (* additional ml directories, given with option -I *) - List.iter Mltop.add_ml_dir (List.rev !ml_includes) + 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"] @ + + (* then standard library and plugins *) + [build_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path ~with_ml:false; + build_stdlib_path ~load_init ~unix_path:(coqlib/"plugins") ~coq_path ~with_ml:true ] @ + + (* then user-contrib *) + (if Sys.file_exists user_contrib then + [build_userlib_path ~unix_path:user_contrib] else [] + ) @ + + (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *) + List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) @ + + (* then current directory (not recursively!) *) + [ { recursive = false; + path_spec = VoPath { unix_path = "."; + coq_path = Libnames.default_root_prefix; + implicit = false; + has_ml = AddTopML } + } ] @ + + (* additional loadpaths, given with options -Q and -R *) + List.map + (fun (unix_path, coq_path, implicit) -> + { recursive = true; + path_spec = VoPath { unix_path; coq_path; has_ml = Mltop.AddNoML; implicit } }) + (List.rev !includes) @ + + (* additional ml directories, given with option -I *) + List.map (fun s -> {recursive = false; path_spec = MlPath s}) (List.rev !ml_includes) (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) let init_ocaml_path () = + let open Mltop in + let lp s = { recursive = false; path_spec = MlPath s } in let add_subdir dl = - Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot [dl]) + Mltop.add_coq_path (lp (List.fold_left (/) Envars.coqroot [dl])) in - Mltop.add_ml_dir (Envars.coqlib ()); + Mltop.add_coq_path (lp (Envars.coqlib ())); List.iter add_subdir Coq_config.all_src_dirs diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index c3fd72754..089847f5d 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -19,7 +19,5 @@ 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 -> unit - +val init_load_path : load_init:bool -> Mltop.coq_path list val init_ocaml_path : unit -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a3a4e20af..9719f60bb 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -489,11 +489,11 @@ exception NoCoqLib let usage batch = begin - try - Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib); - Coqinit.init_load_path ~load_init:!load_init; - with NoCoqLib -> usage_no_coqlib () + 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 + List.iter Mltop.add_coq_path lp; if batch then Usage.print_usage_coqc () else begin Mltop.load_ml_objects_raw_rex @@ -776,7 +776,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); - Coqinit.init_load_path ~load_init:!load_init; + let lp = Coqinit.init_load_path ~load_init:!load_init in + List.iter Mltop.add_coq_path lp; Option.iter Mltop.load_ml_object_raw !toploop; let extras = !toploop_init extras in if not (CList.is_empty extras) then begin -- cgit v1.2.3