From 8b2505b5526395d2ad3c5126624a070e0f55a8af Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 2 Apr 2019 17:04:30 +0200 Subject: [loadpath] Make loadpath handling self-contained and move to vernac We consolidate loadpath handling as a single `Loadpath` module from parts in `Library` and `Mltop`, placing it at the `vernac` level [as `Mltop`] This idea was first suggested in https://github.com/coq/coq/pull/9808 , and indeed it makes sense as library resolution tends to be business of the upper layers: IDE / build tools. Logic could be pushed upwards, but this is good enough for now. This consolidation has enabled some good and long overdue refactorings, and the module should become self-contained enough as to allow the resolution logic to be shared with `coqdep` in the future. The `Mltop` module only cares now about ML-level modules, and should go away once we rewrite the loader using `findlib` to solve https://github.com/coq/coq/issues/7698 . --- vernac/loadpath.ml | 275 ++++++++++++++++++++++++++++++++++++++++++++++++ vernac/loadpath.mli | 101 ++++++++++++++++++ vernac/mltop.ml | 72 +------------ vernac/mltop.mli | 24 +---- vernac/vernac.mllib | 1 + vernac/vernacentries.ml | 25 +++-- 6 files changed, 397 insertions(+), 101 deletions(-) create mode 100644 vernac/loadpath.ml create mode 100644 vernac/loadpath.mli (limited to 'vernac') diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml new file mode 100644 index 0000000000..cd5ccd856b --- /dev/null +++ b/vernac/loadpath.ml @@ -0,0 +1,275 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* raise Not_found + | [p] -> p + | _ -> anomaly_too_many_paths phys_dir + +let is_in_load_paths phys_dir = + let dir = CUnix.canonical_path_name phys_dir in + let lp = get_load_paths () in + let check_p p = String.equal dir p.path_physical in + List.exists check_p lp + +let remove_load_path dir = + let filter p = not (String.equal p.path_physical dir) in + load_paths := List.filter filter !load_paths + +let warn_overriding_logical_loadpath = + CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath" + (fun (phys_path, old_path, coq_path) -> + str phys_path ++ strbrk " was previously bound to " ++ + DirPath.print old_path ++ strbrk "; it is remapped to " ++ + DirPath.print coq_path) + +let add_load_path phys_path coq_path ~implicit = + let phys_path = CUnix.canonical_path_name phys_path in + let filter p = String.equal p.path_physical phys_path in + let binding = { + path_logical = coq_path; + path_physical = phys_path; + path_implicit = implicit; + } in + match List.filter filter !load_paths with + | [] -> + load_paths := binding :: !load_paths + | [{ path_logical = old_path; path_implicit = old_implicit }] -> + let replace = + if DirPath.equal coq_path old_path then + implicit <> old_implicit + else + let () = + (* Do not warn when overriding the default "-I ." path *) + if not (DirPath.equal old_path Libnames.default_root_prefix) then + warn_overriding_logical_loadpath (phys_path, old_path, coq_path) + in + true in + if replace then + begin + remove_load_path phys_path; + load_paths := binding :: !load_paths; + end + | _ -> anomaly_too_many_paths phys_path + +let filter_path f = + let rec aux = function + | [] -> [] + | p :: l -> + if f p.path_logical then (p.path_physical, p.path_logical) :: aux l + else aux l + in + aux !load_paths + +let expand_path ?root dir = + let rec aux = function + | [] -> [] + | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l -> + let success = + match root with + | None -> + if implicit then is_dirpath_suffix_of dir lg + else DirPath.equal dir lg + | Some root -> + is_dirpath_prefix_of root lg && + is_dirpath_suffix_of dir (drop_dirpath_prefix root lg) in + if success then (ph, lg) :: aux l else aux l in + aux !load_paths + +let locate_file fname = + let paths = List.map physical !load_paths in + let _,longfname = + System.find_file_in_path ~warn:(not !Flags.quiet) paths fname in + longfname + +(************************************************************************) +(*s Locate absolute or partially qualified library names in the path *) + +exception LibUnmappedDir +exception LibNotFound +type library_location = LibLoaded | LibInPath + +let warn_several_object_files = + CWarnings.create ~name:"several-object-files" ~category:"require" + Pp.(fun (vi, vo) -> + seq [ str "Loading"; spc (); str vi + ; strbrk " instead of "; str vo + ; strbrk " because it is more recent" + ]) + +let locate_absolute_library dir = + (* Search in loadpath *) + let pref, base = Libnames.split_dirpath dir in + let loadpath = filter_path (fun dir -> DirPath.equal dir pref) in + let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in + let loadpath = List.map fst loadpath in + let find ext = + try + let name = Id.to_string base ^ ext in + let _, file = System.where_in_path ~warn:false loadpath name in + Some file + with Not_found -> None in + match find ".vo", find ".vio" with + | None, None -> raise LibNotFound + | Some file, None | None, Some file -> file + | Some vo, Some vi when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> + warn_several_object_files (vi, vo); + vi + | Some vo, Some _ -> vo + +let locate_qualified_library ?root ?(warn = true) qid = + (* Search library in loadpath *) + let dir, base = Libnames.repr_qualid qid in + let loadpath = expand_path ?root dir in + let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in + let find ext = + try + let name = Id.to_string base ^ ext in + let lpath, file = + System.where_in_path ~warn (List.map fst loadpath) name in + Some (lpath, file) + with Not_found -> None in + let lpath, file = + match find ".vo", find ".vio" with + | None, None -> raise LibNotFound + | Some res, None | None, Some res -> res + | Some (_, vo), Some (_, vi as resvi) + when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> + warn_several_object_files (vi, vo); + resvi + | Some resvo, Some _ -> resvo + in + let dir = Libnames.add_dirpath_suffix + (CString.List.assoc lpath loadpath) base in + (* Look if loaded *) + if Library.library_is_loaded dir + then (LibLoaded, dir, Library.library_full_filename dir) + (* Otherwise, look for it in the file system *) + else (LibInPath, dir, file) + +let error_unmapped_dir qid = + let prefix, _ = Libnames.repr_qualid qid in + CErrors.user_err ~hdr:"load_absolute_library_from" + Pp.(seq [ str "Cannot load "; Libnames.pr_qualid qid; str ":"; spc () + ; str "no physical path bound to"; spc () + ; DirPath.print prefix; fnl () + ]) + +let error_lib_not_found qid = + CErrors.user_err ~hdr:"load_absolute_library_from" + Pp.(seq [ str "Cannot find library "; Libnames.pr_qualid qid; str" in loadpath"]) + +let try_locate_absolute_library dir = + try + locate_absolute_library dir + with + | LibUnmappedDir -> error_unmapped_dir (Libnames.qualid_of_dirpath dir) + | LibNotFound -> error_lib_not_found (Libnames.qualid_of_dirpath dir) + + +(** { 5 Extending the load path } *) + +(* Adds a path to the Coq and ML paths *) +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; +} + +let warn_cannot_open_path = + CWarnings.create ~name:"cannot-open-path" ~category:"filesystem" + (fun unix_path -> str "Cannot open " ++ str unix_path) + +let warn_cannot_use_directory = + CWarnings.create ~name:"cannot-use-directory" ~category:"filesystem" + (fun d -> + str "Directory " ++ str d ++ + strbrk " cannot be used as a Coq identifier (skipped)") + +let convert_string d = + try Names.Id.of_string d + with UserError _ -> + let d = Unicode.escaped_if_non_utf8 d in + warn_cannot_use_directory d; + raise Exit + +let add_vo_path ~recursive lp = + let unix_path = lp.unix_path in + let implicit = lp.implicit in + if System.exists_dir unix_path then + let dirs = if recursive then System.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 + Some (lp, Names.DirPath.make path) + with Exit -> None + in + let dirs = List.map_filter convert_dirs dirs in + let add_ml_dir = Mltop.add_ml_dir ~recursive:false in + let () = match lp.has_ml with + | AddNoML -> () + | AddTopML -> + Mltop.add_ml_dir ~recursive:false unix_path + | AddRecML -> + List.iter (fun (lp,_) -> add_ml_dir lp) dirs; + add_ml_dir unix_path in + let add (path, dir) = add_load_path path ~implicit dir in + let () = List.iter add dirs in + 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 -> + Mltop.add_ml_dir ~recursive dir diff --git a/vernac/loadpath.mli b/vernac/loadpath.mli new file mode 100644 index 0000000000..fe4dc55c21 --- /dev/null +++ b/vernac/loadpath.mli @@ -0,0 +1,101 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* CUnix.physical_path +(** Get the physical path (filesystem location) of a loadpath. *) + +val logical : t -> DirPath.t +(** Get the logical path (Coq module hierarchy) of a loadpath. *) + +val get_load_paths : unit -> t list +(** Get the current loadpath association. *) + +val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit +(** [add_load_path phys log type] adds the binding [phys := log] to the current + loadpaths. *) + +val remove_load_path : CUnix.physical_path -> unit +(** Remove the current logical path binding associated to a given physical path, + if any. *) + +val find_load_path : CUnix.physical_path -> t +(** Get the binding associated to a physical path. Raises [Not_found] if there + is none. *) + +val is_in_load_paths : CUnix.physical_path -> bool +(** Whether a physical path is currently bound. *) + +val expand_path : ?root:DirPath.t -> DirPath.t -> (CUnix.physical_path * DirPath.t) list +(** Given a relative logical path, associate the list of absolute physical and + logical paths which are possible matches of it. *) + +val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list +(** As {!expand_path} but uses a filter function instead, and ignores the + implicit status of loadpaths. *) + +val locate_file : string -> string +(** Locate a file among the registered paths. Do not use this function, as + it does not respect the visibility of paths. *) + +(** {6 Locate a library in the load path } *) +exception LibUnmappedDir +exception LibNotFound +type library_location = LibLoaded | LibInPath + +val locate_qualified_library : + ?root:DirPath.t -> ?warn:bool -> Libnames.qualid -> + library_location * DirPath.t * CUnix.physical_path +(** Locates a library by implicit name. + + @raise LibUnmappedDir if the library is not in the path + @raise LibNotFound if there is no corresponding file in the path + +*) + +val try_locate_absolute_library : DirPath.t -> string + +(** {6 Extending the Load Path } *) + +(** Adds a path to the Coq and ML paths *) +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; +} + +val add_coq_path : coq_path -> unit diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 78e26c65d4..bbee9988d0 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -159,75 +159,9 @@ let add_ml_dir s = | _ -> () (* For Rec Add ML Path (-R) *) -let add_rec_ml_dir unix_path = - List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path) - -(* Adding files to Coq and ML loadpath *) - -let warn_cannot_use_directory = - CWarnings.create ~name:"cannot-use-directory" ~category:"filesystem" - (fun d -> - str "Directory " ++ str d ++ - strbrk " cannot be used as a Coq identifier (skipped)") - -let convert_string d = - try Names.Id.of_string d - with UserError _ -> - let d = Unicode.escaped_if_non_utf8 d in - warn_cannot_use_directory d; - raise Exit - -let warn_cannot_open_path = - CWarnings.create ~name:"cannot-open-path" ~category:"filesystem" - (fun unix_path -> str "Cannot open " ++ str unix_path) - -type add_ml = AddNoML | AddTopML | AddRecML - -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 = 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 - Some (lp, Names.DirPath.make path) - with Exit -> None - in - let dirs = List.map_filter convert_dirs dirs in - let () = match lp.has_ml with - | AddNoML -> () - | AddTopML -> add_ml_dir unix_path - | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs; add_ml_dir unix_path 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 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 +let add_ml_dir ~recursive unix_path = + let dirs = if recursive then (all_subdirs ~unix_path) else [unix_path,[]] in + List.iter (fun (lp,_) -> add_ml_dir lp) dirs (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = diff --git a/vernac/mltop.mli b/vernac/mltop.mli index 3d796aa4aa..b457c9c88f 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -32,6 +32,9 @@ val ocaml_toploop : unit -> unit (** {5 ML Dynlink} *) +(** Adds a dir to the plugin search path *) +val add_ml_dir : recursive:bool -> string -> unit + (** Tests if we can load ML files *) val has_dynlink : bool @@ -41,27 +44,6 @@ val dir_ml_load : string -> unit (** Dynamic interpretation of .ml *) val dir_ml_use : string -> unit -(** Adds a path to the Coq and ML paths *) -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; -} - -val add_coq_path : coq_path -> unit - (** List of modules linked to the toplevel *) val add_known_module : string -> unit val module_is_known : string -> bool diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 7f5c265eea..57c56a58f9 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -32,6 +32,7 @@ Assumptions Vernacstate Mltop Topfmt +Loadpath Vernacentries Misctypes diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 918852239a..4fd9c713b9 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -444,9 +444,9 @@ let locate_file f = str file let msg_found_library = function - | Library.LibLoaded, fulldir, file -> + | Loadpath.LibLoaded, fulldir, file -> hov 0 (DirPath.print fulldir ++ strbrk " has been loaded from file " ++ str file) - | Library.LibInPath, fulldir, file -> + | Loadpath.LibInPath, fulldir, file -> hov 0 (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file) let err_unmapped_library ?from qid = @@ -471,10 +471,11 @@ let err_notfound_library ?from qid = (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) let print_located_library qid = - try msg_found_library (Library.locate_qualified_library ~warn:false qid) + let open Loadpath in + try msg_found_library (locate_qualified_library ~warn:false qid) with - | Library.LibUnmappedDir -> err_unmapped_library qid - | Library.LibNotFound -> err_notfound_library qid + | LibUnmappedDir -> err_unmapped_library qid + | LibNotFound -> err_notfound_library qid let smart_global r = let gr = Smartlocate.smart_global r in @@ -1026,18 +1027,20 @@ let vernac_require from import qidl = Some (Libnames.add_dirpath_suffix hd tl) in let locate qid = + let open Loadpath in try let warn = not !Flags.quiet in - let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in + let (_, dir, f) = locate_qualified_library ?root ~warn qid in (dir, f) with - | Library.LibUnmappedDir -> err_unmapped_library ?from:root qid - | Library.LibNotFound -> err_notfound_library ?from:root qid + | LibUnmappedDir -> err_unmapped_library ?from:root qid + | LibNotFound -> err_notfound_library ?from:root qid in let modrefl = List.map locate qidl in if Dumpglob.dump () then List.iter2 (fun {CAst.loc} dp -> Dumpglob.dump_libref ?loc dp "lib") qidl (List.map fst modrefl); - Library.require_library_from_dirpath modrefl import + let lib_resolver = Loadpath.try_locate_absolute_library in + Library.require_library_from_dirpath ~lib_resolver modrefl import (* Coercions and canonical structures *) @@ -1133,7 +1136,7 @@ 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 open Loadpath in let pdir = expand pdir in let alias = Option.default Libnames.default_root_prefix ldiropt in add_coq_path { recursive = true; @@ -1145,7 +1148,7 @@ let vernac_remove_loadpath path = (* Coq syntax for ML or system commands *) let vernac_add_ml_path isrec path = - let open Mltop in + let open Loadpath in add_coq_path { recursive = isrec; path_spec = MlPath (expand path) } let vernac_declare_ml_module ~local l = -- cgit v1.2.3 From b7b78d8ca8d6fc6fdb0f744be02c386bc00da8bf Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 5 Apr 2019 15:44:36 +0200 Subject: [loadpath] Further cleanup after merge with MlTop. We cleanup a bit the implementation of LoadPath which is not possible as now all the loadpath logic is in the same place. In particular, we remove exceptions in favor a `locate_result` monad. More cleanup should still be possible, in particular `locate_absolute_library` and `locate_qualified_library` should be merged. --- vernac/loadpath.ml | 184 +++++++++++++++++++++++++----------------------- vernac/loadpath.mli | 34 +++------ vernac/vernacentries.ml | 28 +++----- 3 files changed, 118 insertions(+), 128 deletions(-) (limited to 'vernac') diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml index cd5ccd856b..b164a2e37a 100644 --- a/vernac/loadpath.ml +++ b/vernac/loadpath.ml @@ -8,30 +8,31 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Pp open Util -open CErrors -open Names -open Libnames +module DP = Names.DirPath (** Load paths. Mapping from physical to logical paths. *) type t = { path_physical : CUnix.physical_path; - path_logical : DirPath.t; + path_logical : DP.t; path_implicit : bool; } let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS" let logical p = p.path_logical - let physical p = p.path_physical +let pp p = + let dir = DP.print p.path_logical in + let path = Pp.str (CUnix.escaped_string_of_physical_path p.path_physical) in + Pp.(hov 2 (dir ++ spc () ++ path)) + let get_load_paths () = !load_paths let anomaly_too_many_paths path = - anomaly (str "Several logical paths are associated to" ++ spc () ++ str path ++ str ".") + CErrors.anomaly Pp.(str "Several logical paths are associated to" ++ spc () ++ str path ++ str ".") let find_load_path phys_dir = let phys_dir = CUnix.canonical_path_name phys_dir in @@ -42,22 +43,16 @@ let find_load_path phys_dir = | [p] -> p | _ -> anomaly_too_many_paths phys_dir -let is_in_load_paths phys_dir = - let dir = CUnix.canonical_path_name phys_dir in - let lp = get_load_paths () in - let check_p p = String.equal dir p.path_physical in - List.exists check_p lp - let remove_load_path dir = let filter p = not (String.equal p.path_physical dir) in load_paths := List.filter filter !load_paths let warn_overriding_logical_loadpath = CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath" - (fun (phys_path, old_path, coq_path) -> - str phys_path ++ strbrk " was previously bound to " ++ - DirPath.print old_path ++ strbrk "; it is remapped to " ++ - DirPath.print coq_path) + (fun (phys_path, old_path, coq_path) -> + Pp.(seq [str phys_path; strbrk " was previously bound to " + ; DP.print old_path; strbrk "; it is remapped to " + ; DP.print coq_path])) let add_load_path phys_path coq_path ~implicit = let phys_path = CUnix.canonical_path_name phys_path in @@ -72,12 +67,12 @@ let add_load_path phys_path coq_path ~implicit = load_paths := binding :: !load_paths | [{ path_logical = old_path; path_implicit = old_implicit }] -> let replace = - if DirPath.equal coq_path old_path then + if DP.equal coq_path old_path then implicit <> old_implicit else let () = (* Do not warn when overriding the default "-I ." path *) - if not (DirPath.equal old_path Libnames.default_root_prefix) then + if not (DP.equal old_path Libnames.default_root_prefix) then warn_overriding_logical_loadpath (phys_path, old_path, coq_path) in true in @@ -104,11 +99,11 @@ let expand_path ?root dir = let success = match root with | None -> - if implicit then is_dirpath_suffix_of dir lg - else DirPath.equal dir lg + if implicit then Libnames.is_dirpath_suffix_of dir lg + else DP.equal dir lg | Some root -> - is_dirpath_prefix_of root lg && - is_dirpath_suffix_of dir (drop_dirpath_prefix root lg) in + Libnames.(is_dirpath_prefix_of root lg && + is_dirpath_suffix_of dir (drop_dirpath_prefix root lg)) in if success then (ph, lg) :: aux l else aux l in aux !load_paths @@ -121,9 +116,9 @@ let locate_file fname = (************************************************************************) (*s Locate absolute or partially qualified library names in the path *) -exception LibUnmappedDir -exception LibNotFound type library_location = LibLoaded | LibInPath +type locate_error = LibUnmappedDir | LibNotFound +type 'a locate_result = ('a, locate_error) result let warn_several_object_files = CWarnings.create ~name:"several-object-files" ~category:"require" @@ -133,62 +128,76 @@ let warn_several_object_files = ; strbrk " because it is more recent" ]) -let locate_absolute_library dir = +let locate_absolute_library dir : CUnix.physical_path locate_result = (* Search in loadpath *) let pref, base = Libnames.split_dirpath dir in - let loadpath = filter_path (fun dir -> DirPath.equal dir pref) in - let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in - let loadpath = List.map fst loadpath in - let find ext = - try - let name = Id.to_string base ^ ext in - let _, file = System.where_in_path ~warn:false loadpath name in - Some file - with Not_found -> None in - match find ".vo", find ".vio" with - | None, None -> raise LibNotFound - | Some file, None | None, Some file -> file - | Some vo, Some vi when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - warn_several_object_files (vi, vo); - vi - | Some vo, Some _ -> vo - -let locate_qualified_library ?root ?(warn = true) qid = + let loadpath = filter_path (fun dir -> DP.equal dir pref) in + match loadpath with + | [] -> Error LibUnmappedDir + | _ -> + let loadpath = List.map fst loadpath in + let find ext = + try + let name = Names.Id.to_string base ^ ext in + let _, file = System.where_in_path ~warn:false loadpath name in + Some file + with Not_found -> None in + match find ".vo", find ".vio" with + | None, None -> + Error LibNotFound + | Some file, None | None, Some file -> + Ok file + | Some vo, Some vi when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> + warn_several_object_files (vi, vo); + Ok vi + | Some vo, Some _ -> + Ok vo + +let locate_qualified_library ?root ?(warn = true) qid : + (library_location * DP.t * CUnix.physical_path) locate_result = (* Search library in loadpath *) let dir, base = Libnames.repr_qualid qid in let loadpath = expand_path ?root dir in - let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in - let find ext = - try - let name = Id.to_string base ^ ext in - let lpath, file = - System.where_in_path ~warn (List.map fst loadpath) name in - Some (lpath, file) - with Not_found -> None in - let lpath, file = - match find ".vo", find ".vio" with - | None, None -> raise LibNotFound - | Some res, None | None, Some res -> res - | Some (_, vo), Some (_, vi as resvi) - when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - warn_several_object_files (vi, vo); - resvi - | Some resvo, Some _ -> resvo - in - let dir = Libnames.add_dirpath_suffix - (CString.List.assoc lpath loadpath) base in - (* Look if loaded *) - if Library.library_is_loaded dir - then (LibLoaded, dir, Library.library_full_filename dir) - (* Otherwise, look for it in the file system *) - else (LibInPath, dir, file) + match loadpath with + | [] -> Error LibUnmappedDir + | _ -> + let find ext = + try + let name = Names.Id.to_string base ^ ext in + let lpath, file = + System.where_in_path ~warn (List.map fst loadpath) name in + Some (lpath, file) + with Not_found -> None in + let vores = + match find ".vo", find ".vio" with + | None, None -> + Error LibNotFound + | Some res, None | None, Some res -> + Ok res + | Some (_, vo), Some (_, vi as resvi) + when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> + warn_several_object_files (vi, vo); + Ok resvi + | Some resvo, Some _ -> + Ok resvo + in + match vores with + | Ok (lpath, file) -> + let dir = Libnames.add_dirpath_suffix + (CString.List.assoc lpath loadpath) base in + (* Look if loaded *) + if Library.library_is_loaded dir + then Ok (LibLoaded, dir, Library.library_full_filename dir) + (* Otherwise, look for it in the file system *) + else Ok (LibInPath, dir, file) + | Error fail -> Error fail let error_unmapped_dir qid = let prefix, _ = Libnames.repr_qualid qid in CErrors.user_err ~hdr:"load_absolute_library_from" Pp.(seq [ str "Cannot load "; Libnames.pr_qualid qid; str ":"; spc () ; str "no physical path bound to"; spc () - ; DirPath.print prefix; fnl () + ; DP.print prefix; fnl () ]) let error_lib_not_found qid = @@ -196,12 +205,12 @@ let error_lib_not_found qid = Pp.(seq [ str "Cannot find library "; Libnames.pr_qualid qid; str" in loadpath"]) let try_locate_absolute_library dir = - try - locate_absolute_library dir - with - | LibUnmappedDir -> error_unmapped_dir (Libnames.qualid_of_dirpath dir) - | LibNotFound -> error_lib_not_found (Libnames.qualid_of_dirpath dir) - + match locate_absolute_library dir with + | Ok res -> res + | Error LibUnmappedDir -> + error_unmapped_dir (Libnames.qualid_of_dirpath dir) + | Error LibNotFound -> + error_lib_not_found (Libnames.qualid_of_dirpath dir) (** { 5 Extending the load path } *) @@ -209,10 +218,10 @@ let try_locate_absolute_library dir = 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 *) + unix_path : string; (* Filesystem path contaning vo/ml files *) + coq_path : DP.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 = @@ -226,17 +235,18 @@ type coq_path = { let warn_cannot_open_path = CWarnings.create ~name:"cannot-open-path" ~category:"filesystem" - (fun unix_path -> str "Cannot open " ++ str unix_path) + (fun unix_path -> Pp.(str "Cannot open " ++ str unix_path)) let warn_cannot_use_directory = CWarnings.create ~name:"cannot-use-directory" ~category:"filesystem" - (fun d -> - str "Directory " ++ str d ++ - strbrk " cannot be used as a Coq identifier (skipped)") + (fun d -> + Pp.(str "Directory " ++ str d ++ + strbrk " cannot be used as a Coq identifier (skipped)")) let convert_string d = try Names.Id.of_string d - with UserError _ -> + with + | CErrors.UserError _ -> let d = Unicode.escaped_if_non_utf8 d in warn_cannot_use_directory d; raise Exit @@ -246,11 +256,11 @@ let add_vo_path ~recursive lp = let implicit = lp.implicit in if System.exists_dir unix_path then let dirs = if recursive then System.all_subdirs ~unix_path else [] in - let prefix = Names.DirPath.repr lp.coq_path in + let prefix = DP.repr lp.coq_path in let convert_dirs (lp, cp) = try let path = List.rev_map convert_string cp @ prefix in - Some (lp, Names.DirPath.make path) + Some (lp, DP.make path) with Exit -> None in let dirs = List.map_filter convert_dirs dirs in diff --git a/vernac/loadpath.mli b/vernac/loadpath.mli index fe4dc55c21..d393fc35b5 100644 --- a/vernac/loadpath.mli +++ b/vernac/loadpath.mli @@ -20,19 +20,15 @@ open Names type t (** Type of loadpath bindings. *) -val physical : t -> CUnix.physical_path -(** Get the physical path (filesystem location) of a loadpath. *) - val logical : t -> DirPath.t (** Get the logical path (Coq module hierarchy) of a loadpath. *) +val pp : t -> Pp.t +(** Print a load path *) + val get_load_paths : unit -> t list (** Get the current loadpath association. *) -val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit -(** [add_load_path phys log type] adds the binding [phys := log] to the current - loadpaths. *) - val remove_load_path : CUnix.physical_path -> unit (** Remove the current logical path binding associated to a given physical path, if any. *) @@ -41,29 +37,21 @@ val find_load_path : CUnix.physical_path -> t (** Get the binding associated to a physical path. Raises [Not_found] if there is none. *) -val is_in_load_paths : CUnix.physical_path -> bool -(** Whether a physical path is currently bound. *) - -val expand_path : ?root:DirPath.t -> DirPath.t -> (CUnix.physical_path * DirPath.t) list -(** Given a relative logical path, associate the list of absolute physical and - logical paths which are possible matches of it. *) - -val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list -(** As {!expand_path} but uses a filter function instead, and ignores the - implicit status of loadpaths. *) - val locate_file : string -> string (** Locate a file among the registered paths. Do not use this function, as it does not respect the visibility of paths. *) (** {6 Locate a library in the load path } *) -exception LibUnmappedDir -exception LibNotFound type library_location = LibLoaded | LibInPath +type locate_error = LibUnmappedDir | LibNotFound +type 'a locate_result = ('a, locate_error) result + +val locate_qualified_library + : ?root:DirPath.t + -> ?warn:bool + -> Libnames.qualid + -> (library_location * DirPath.t * CUnix.physical_path) locate_result -val locate_qualified_library : - ?root:DirPath.t -> ?warn:bool -> Libnames.qualid -> - library_location * DirPath.t * CUnix.physical_path (** Locates a library by implicit name. @raise LibUnmappedDir if the library is not in the path diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4fd9c713b9..29b78a5195 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -201,11 +201,6 @@ let show_match id = (* "Print" commands *) -let print_path_entry p = - let dir = DirPath.print (Loadpath.logical p) in - let path = str (CUnix.escaped_string_of_physical_path (Loadpath.physical p)) in - Pp.hov 2 (dir ++ spc () ++ path) - let print_loadpath dir = let l = Loadpath.get_load_paths () in let l = match dir with @@ -215,7 +210,7 @@ let print_loadpath dir = List.filter filter l in str "Logical Path / Physical path:" ++ fnl () ++ - prlist_with_sep fnl print_path_entry l + prlist_with_sep fnl Loadpath.pp l let print_modules () = let opened = Library.opened_libraries () @@ -472,10 +467,10 @@ let err_notfound_library ?from qid = let print_located_library qid = let open Loadpath in - try msg_found_library (locate_qualified_library ~warn:false qid) - with - | LibUnmappedDir -> err_unmapped_library qid - | LibNotFound -> err_notfound_library qid + match locate_qualified_library ~warn:false qid with + | Ok lib -> msg_found_library lib + | Error LibUnmappedDir -> err_unmapped_library qid + | Error LibNotFound -> err_notfound_library qid let smart_global r = let gr = Smartlocate.smart_global r in @@ -1028,13 +1023,11 @@ let vernac_require from import qidl = in let locate qid = let open Loadpath in - try - let warn = not !Flags.quiet in - let (_, dir, f) = locate_qualified_library ?root ~warn qid in - (dir, f) - with - | LibUnmappedDir -> err_unmapped_library ?from:root qid - | LibNotFound -> err_notfound_library ?from:root qid + let warn = not !Flags.quiet in + match locate_qualified_library ?root ~warn qid with + | Ok (_,dir,f) -> dir, f + | Error LibUnmappedDir -> err_unmapped_library ?from:root qid + | Error LibNotFound -> err_notfound_library ?from:root qid in let modrefl = List.map locate qidl in if Dumpglob.dump () then @@ -1144,7 +1137,6 @@ let vernac_add_loadpath implicit pdir ldiropt = let vernac_remove_loadpath path = Loadpath.remove_load_path (expand path) - (* Coq syntax for ML or system commands *) let vernac_add_ml_path isrec path = -- cgit v1.2.3 From c4b23f08247cb6a91b585f9b173934bbe3994b43 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 11 Apr 2019 00:41:47 +0200 Subject: [loadpath] Factor in common logic for vio/vo file selection. --- vernac/loadpath.ml | 64 ++++++++++++++++++++++-------------------------------- 1 file changed, 26 insertions(+), 38 deletions(-) (limited to 'vernac') diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml index b164a2e37a..1bb44d0ef1 100644 --- a/vernac/loadpath.ml +++ b/vernac/loadpath.ml @@ -128,6 +128,28 @@ let warn_several_object_files = ; strbrk " because it is more recent" ]) + +let select_vo_file ~warn loadpath base = + let find ext = + let loadpath = List.map fst loadpath in + try + let name = Names.Id.to_string base ^ ext in + let lpath, file = + System.where_in_path ~warn loadpath name in + Some (lpath, file) + with Not_found -> None in + match find ".vo", find ".vio" with + | None, None -> + Error LibNotFound + | Some res, None | None, Some res -> + Ok res + | Some (_, vo), Some (_, vi as resvi) + when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> + warn_several_object_files (vi, vo); + Ok resvi + | Some resvo, Some _ -> + Ok resvo + let locate_absolute_library dir : CUnix.physical_path locate_result = (* Search in loadpath *) let pref, base = Libnames.split_dirpath dir in @@ -135,23 +157,9 @@ let locate_absolute_library dir : CUnix.physical_path locate_result = match loadpath with | [] -> Error LibUnmappedDir | _ -> - let loadpath = List.map fst loadpath in - let find ext = - try - let name = Names.Id.to_string base ^ ext in - let _, file = System.where_in_path ~warn:false loadpath name in - Some file - with Not_found -> None in - match find ".vo", find ".vio" with - | None, None -> - Error LibNotFound - | Some file, None | None, Some file -> - Ok file - | Some vo, Some vi when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - warn_several_object_files (vi, vo); - Ok vi - | Some vo, Some _ -> - Ok vo + match select_vo_file ~warn:false loadpath base with + | Ok (_, file) -> Ok file + | Error fail -> Error fail let locate_qualified_library ?root ?(warn = true) qid : (library_location * DP.t * CUnix.physical_path) locate_result = @@ -161,27 +169,7 @@ let locate_qualified_library ?root ?(warn = true) qid : match loadpath with | [] -> Error LibUnmappedDir | _ -> - let find ext = - try - let name = Names.Id.to_string base ^ ext in - let lpath, file = - System.where_in_path ~warn (List.map fst loadpath) name in - Some (lpath, file) - with Not_found -> None in - let vores = - match find ".vo", find ".vio" with - | None, None -> - Error LibNotFound - | Some res, None | None, Some res -> - Ok res - | Some (_, vo), Some (_, vi as resvi) - when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - warn_several_object_files (vi, vo); - Ok resvi - | Some resvo, Some _ -> - Ok resvo - in - match vores with + match select_vo_file ~warn loadpath base with | Ok (lpath, file) -> let dir = Libnames.add_dirpath_suffix (CString.List.assoc lpath loadpath) base in -- cgit v1.2.3