Merge PR #9895: [loadpath] Make loadpath handling self-contained and move to vernac

Reviewed-by: maximedenes

5 files changed, 22 insertions, 285 deletions

diff --git a/library/library.ml b/library/library.ml
index d8eaf5f659..9f4eb531ed 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -264,85 +264,6 @@ let in_import_library : DirPath.t list * bool -> obj =
        subst_function = subst_import_library;
        classify_function = classify_import_library }
 
-
-(************************************************************************)
-(*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"
-         (fun (vi, vo) -> 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 = split_dirpath dir in
-  let loadpath = 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 = repr_qualid qid in
-  let loadpath = 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 = add_dirpath_suffix (String.List.assoc lpath loadpath) base in
-  (* Look if loaded *)
-  if library_is_loaded dir then (LibLoaded, dir,library_full_filename dir)
-  (* Otherwise, look for it in the file system *)
-  else (LibInPath, dir, file)
-
-let error_unmapped_dir qid =
-  let prefix, _ = repr_qualid qid in
-  user_err ~hdr:"load_absolute_library_from"
-    (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++
-     str "no physical path bound to" ++ spc () ++ DirPath.print prefix ++ fnl ())
-
-let error_lib_not_found qid =
-  user_err ~hdr:"load_absolute_library_from"
-    (str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath")
-
-let try_locate_absolute_library dir =
-  try
-    locate_absolute_library dir
-  with
-    | LibUnmappedDir -> error_unmapped_dir (qualid_of_dirpath dir)
-    | LibNotFound -> error_lib_not_found (qualid_of_dirpath dir)
-
 (************************************************************************)
 (** {6 Tables of opaque proof terms} *)
 
@@ -450,7 +371,7 @@ let intern_from_file f =
 
 module DPMap = Map.Make(DirPath)
 
-let rec intern_library (needed, contents) (dir, f) from =
+let rec intern_library ~lib_resolver (needed, contents) (dir, f) from =
   (* Look if in the current logical environment *)
   try (find_library dir).libsum_digests, (needed, contents)
   with Not_found ->
@@ -459,7 +380,7 @@ let rec intern_library (needed, contents) (dir, f) from =
   with Not_found ->
   Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
   (* [dir] is an absolute name which matches [f] which must be in loadpath *)
-  let f = match f with Some f -> f | None -> try_locate_absolute_library dir in
+  let f = match f with Some f -> f | None -> lib_resolver dir in
   let m = intern_from_file f in
   if not (DirPath.equal dir m.library_name) then
     user_err ~hdr:"load_physical_library"
@@ -467,22 +388,24 @@ let rec intern_library (needed, contents) (dir, f) from =
        DirPath.print m.library_name ++ spc () ++ str "and not library" ++
        spc() ++ DirPath.print dir);
   Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f));
-  m.library_digests, intern_library_deps (needed, contents) dir m f
+  m.library_digests, intern_library_deps ~lib_resolver (needed, contents) dir m f
 
-and intern_library_deps libs dir m from =
-  let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in
+and intern_library_deps ~lib_resolver libs dir m from =
+  let needed, contents =
+    Array.fold_left (intern_mandatory_library ~lib_resolver dir from)
+      libs m.library_deps in
   (dir :: needed, DPMap.add dir m contents )
 
-and intern_mandatory_library caller from libs (dir,d) =
-  let digest, libs = intern_library libs (dir, None) (Some from) in
+and intern_mandatory_library ~lib_resolver caller from libs (dir,d) =
+  let digest, libs = intern_library ~lib_resolver libs (dir, None) (Some from) in
   if not (Safe_typing.digest_match ~actual:digest ~required:d) then
     user_err (str "Compiled library " ++ DirPath.print caller ++
     str " (in file " ++ str from ++ str ") makes inconsistent assumptions \
     over library " ++ DirPath.print dir);
   libs
 
-let rec_intern_library libs (dir, f) =
-  let _, libs = intern_library libs (dir, Some f) None in
+let rec_intern_library ~lib_resolver libs (dir, f) =
+  let _, libs = intern_library ~lib_resolver libs (dir, Some f) None in
   libs
 
 let native_name_from_filename f =
@@ -557,8 +480,8 @@ let warn_require_in_module =
                               strbrk "You can Require a module at toplevel " ++
                               strbrk "and optionally Import it inside another one.")
 
-let require_library_from_dirpath modrefl export =
-  let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in
+let require_library_from_dirpath ~lib_resolver modrefl export =
+  let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPMap.empty) modrefl in
   let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in
   let modrefl = List.map fst modrefl in
     if Lib.is_module_or_modtype () then
diff --git a/library/library.mli b/library/library.mli
index 390299bf56..f3186d847f 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -22,7 +22,11 @@ open Libnames
 (** {6 ... }
     Require = load in the environment + open (if the optional boolean
     is not [None]); mark also for export if the boolean is [Some true] *)
-val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit
+val require_library_from_dirpath
+  :  lib_resolver:(DirPath.t -> CUnix.physical_path)
+  -> (DirPath.t * string) list
+  -> bool option
+  -> unit
 
 (** {6 Start the compilation of a library } *)
 
@@ -45,8 +49,10 @@ val save_library_to :
   output_native_objects:bool ->
   DirPath.t -> string -> Opaqueproof.opaquetab -> unit
 
-val load_library_todo :
-  string -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
+val load_library_todo
+  :  CUnix.physical_path
+  -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
+
 val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit
 
 (** {6 Interrogate the status of libraries } *)
@@ -65,20 +71,5 @@ val library_full_filename : DirPath.t -> string
   (** - Overwrite the filename of all libraries (used when restoring a state) *)
 val overwrite_library_filenames : string -> unit
 
-(** {6 Locate a library in the load paths } *)
-exception LibUnmappedDir
-exception LibNotFound
-type library_location = LibLoaded | LibInPath
-
-val locate_qualified_library :
-  ?root:DirPath.t -> ?warn:bool -> 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
-
-*)
-
 (** {6 Native compiler. } *)
 val native_name_from_filename : string -> string
diff --git a/library/library.mllib b/library/library.mllib
index 8f694f4a31..ef53471377 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -7,7 +7,6 @@ Global
 Decl_kinds
 Lib
 Declaremods
-Loadpath
 Library
 States
 Kindops
diff --git a/library/loadpath.ml b/library/loadpath.ml
deleted file mode 100644
index fc13c864d0..0000000000
--- a/library/loadpath.ml
+++ /dev/null
@@ -1,119 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Pp
-open Util
-open CErrors
-open Names
-open Libnames
-
-(** Load paths. Mapping from physical to logical paths. *)
-
-type t = {
-  path_physical : CUnix.physical_path;
-  path_logical : DirPath.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 get_load_paths () = !load_paths
-
-let anomaly_too_many_paths path =
-  anomaly (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
-  let filter p = String.equal p.path_physical phys_dir in
-  let paths = List.filter filter !load_paths in
-  match paths with
-  | [] -> 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
diff --git a/library/loadpath.mli b/library/loadpath.mli
deleted file mode 100644
index 4044ca1127..0000000000
--- a/library/loadpath.mli
+++ /dev/null
@@ -1,57 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Names
-
-(** * Load paths.
-
-  A load path is a physical path in the file system; to each load path is
-  associated a Coq [DirPath.t] (the "logical" path of the physical path).
-
-*)
-
-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 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. *)