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 ++--- vernac/mltop.ml | 34 +++++++++++++--- vernac/mltop.mli | 24 ++++++++--- vernac/vernacentries.ml | 7 +++- 6 files changed, 124 insertions(+), 62 deletions(-) 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 diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 00554e3ba..053b9d070 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -184,10 +184,28 @@ let warn_cannot_open_path = type add_ml = AddNoML | AddTopML | AddRecML -let add_rec_path add_ml ~unix_path ~coq_root ~implicit = +type vo_path_spec = { + unix_path : string; + coq_path : Names.DirPath.t; + implicit : bool; + has_ml : add_ml; +} + +type coq_path_spec = + | VoPath of vo_path_spec + | MlPath of string + +type coq_path = { + path_spec: coq_path_spec; + recursive: bool; +} + +let add_vo_path ~recursive lp = + let unix_path = lp.unix_path in + let implicit = lp.implicit in if exists_dir unix_path then - let dirs = all_subdirs ~unix_path in - let prefix = Names.DirPath.repr coq_root in + let dirs = if recursive then all_subdirs ~unix_path else [] in + let prefix = Names.DirPath.repr lp.coq_path in let convert_dirs (lp, cp) = try let path = List.rev_map convert_string cp @ prefix in @@ -195,17 +213,23 @@ let add_rec_path add_ml ~unix_path ~coq_root ~implicit = with Exit -> None in let dirs = List.map_filter convert_dirs dirs in - let () = match add_ml with + let () = match lp.has_ml with | AddNoML -> () | AddTopML -> add_ml_dir unix_path | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs in let add (path, dir) = Loadpath.add_load_path path ~implicit dir in let () = List.iter add dirs in - Loadpath.add_load_path unix_path ~implicit coq_root + Loadpath.add_load_path unix_path ~implicit lp.coq_path else warn_cannot_open_path unix_path +let add_coq_path { recursive; path_spec } = match path_spec with + | VoPath lp -> + add_vo_path ~recursive lp + | MlPath dir -> + if recursive then add_rec_ml_dir dir else add_ml_dir dir + (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = if Filename.check_suffix name ".cmo" then diff --git a/vernac/mltop.mli b/vernac/mltop.mli index 324a66d38..e44a7c243 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -42,14 +42,26 @@ val dir_ml_load : string -> unit (** Dynamic interpretation of .ml *) val dir_ml_use : string -> unit -(** Adds a path to the ML paths *) -val add_ml_dir : string -> unit -val add_rec_ml_dir : string -> unit - +(** Adds a path to the Coq and ML paths *) type add_ml = AddNoML | AddTopML | AddRecML -(** Adds a path to the Coq and ML paths *) -val add_rec_path : add_ml -> unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit +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; +} + +val add_coq_path : coq_path -> unit (** List of modules linked to the toplevel *) val add_known_module : string -> unit diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3358951f4..1a02a22a5 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -905,9 +905,11 @@ let expand filename = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename let vernac_add_loadpath implicit pdir ldiropt = + let open Mltop in let pdir = expand pdir in let alias = Option.default Libnames.default_root_prefix ldiropt in - Mltop.add_rec_path Mltop.AddTopML ~unix_path:pdir ~coq_root:alias ~implicit + add_coq_path { recursive = true; + path_spec = VoPath { unix_path = pdir; coq_path = alias; has_ml = AddTopML; implicit } } let vernac_remove_loadpath path = Loadpath.remove_load_path (expand path) @@ -915,7 +917,8 @@ let vernac_remove_loadpath path = (* Coq syntax for ML or system commands *) let vernac_add_ml_path isrec path = - (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) (expand path) + let open Mltop in + add_coq_path { recursive = isrec; path_spec = MlPath (expand path) } let vernac_declare_ml_module ~atts l = let local = make_locality atts.locality in -- cgit v1.2.3