[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 .

18 files changed, 385 insertions, 352 deletions

diff --git a/library/library.ml b/library/library.ml
index 500e77f89b..f99bcc7ecf 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/stm/stm.ml b/stm/stm.ml
index 6f7cefb582..2a7fb084fc 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2661,7 +2661,7 @@ type stm_init_options = {
 
   (* Initial load path in scope for the document. Usually extracted
      from -R options / _CoqProject *)
-  iload_path   : Mltop.coq_path list;
+  iload_path   : Loadpath.coq_path list;
 
   (* Require [require_libs] before the initial state is
      ready. Parameters follow [Library], that is to say,
@@ -2719,7 +2719,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
   (* Set load path; important, this has to happen before we declare
      the library below as [Declaremods/Library] will infer the module
      name by looking at the load path! *)
-  List.iter Mltop.add_coq_path iload_path;
+  List.iter Loadpath.add_coq_path iload_path;
 
   Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff;
 
diff --git a/stm/stm.mli b/stm/stm.mli
index 9d2bf56629..73f3ffab7e 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -69,7 +69,7 @@ type stm_init_options = {
 
   (* Initial load path in scope for the document. Usually extracted
      from -R options / _CoqProject *)
-  iload_path   : Mltop.coq_path list;
+  iload_path   : Loadpath.coq_path list;
 
   (* Require [require_libs] before the initial state is
      ready. Parameters follow [Library], that is to say,
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 2f63410761..7748134146 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -225,7 +225,7 @@ let do_vio opts copts =
      process happens outside of the STM *)
   if copts.vio_files <> [] || copts.vio_tasks <> [] then
     let iload_path = build_load_path opts in
-    List.iter Mltop.add_coq_path iload_path;
+    List.iter Loadpath.add_coq_path iload_path;
 
   (* Vio compile pass *)
   if copts.vio_files <> [] then schedule_vio copts;
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index ec43dbb1d7..4ef31c73b7 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -46,8 +46,8 @@ type t = {
   load_rcfile : bool;
   rcfile      : string option;
 
-  ml_includes : Mltop.coq_path list;
-  vo_includes : Mltop.coq_path list;
+  ml_includes : Loadpath.coq_path list;
+  vo_includes : Loadpath.coq_path list;
   vo_requires : (string * string option * bool option) list;
   (* None = No Import; Some false = Import; Some true = Export *)
 
@@ -147,10 +147,10 @@ let default = {
 (* Functional arguments                                                       *)
 (******************************************************************************)
 let add_ml_include opts s =
-  Mltop.{ opts with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.ml_includes }
+  Loadpath.{ opts with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.ml_includes }
 
 let add_vo_include opts unix_path coq_path implicit =
-  let open Mltop in
+  let open Loadpath in
   let coq_path = Libnames.dirpath_of_string coq_path in
   { opts with vo_includes = {
         recursive = true;
@@ -273,7 +273,7 @@ let usage help =
   end;
   let lp = Coqinit.toplevel_init_load_path () in
   (* Necessary for finding the toplevels below *)
-  List.iter Mltop.add_coq_path lp;
+  List.iter Loadpath.add_coq_path lp;
   help ()
 
 (* Main parsing routine *)
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index d7f9819bee..015789c1f3 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -22,8 +22,8 @@ type t = {
   load_rcfile : bool;
   rcfile      : string option;
 
-  ml_includes : Mltop.coq_path list;
-  vo_includes : Mltop.coq_path list;
+  ml_includes : Loadpath.coq_path list;
+  vo_includes : Loadpath.coq_path list;
   vo_requires : (string * string option * bool option) list;
 
   toplevel_name : Stm.interactive_top;
@@ -69,4 +69,4 @@ val parse_args : help:(unit -> unit) -> init:t -> string list -> t * string list
 val exitcode : t -> int
 
 val require_libs : t -> (string * string option * bool option) list
-val build_load_path : t -> Mltop.coq_path list
+val build_load_path : t -> Loadpath.coq_path list
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 74a089510e..cbe353004e 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -53,25 +53,25 @@ let load_rcfile ~rcfile ~state =
 
 (* Recursively puts dir in the LoadPath if -nois was not passed *)
 let build_stdlib_path ~load_init ~unix_path ~coq_path ~with_ml =
-  let open Mltop in
+  let open Loadpath 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 build_userlib_path ~unix_path =
-  let open Mltop in
+  let open Loadpath in
   { recursive = true;
     path_spec = VoPath {
         unix_path;
         coq_path = Libnames.default_root_prefix;
-        has_ml = Mltop.AddRecML;
+        has_ml = AddRecML;
         implicit = false;
       }
   }
 
 let ml_path_if c p =
-  let open Mltop in
+  let open Loadpath in
   let f x = { recursive = false; path_spec = MlPath x } in
   if c then List.map f p else []
 
@@ -85,7 +85,7 @@ let toplevel_init_load_path () =
 (* LoadPath for Coq user libraries *)
 let libs_init_load_path ~load_init =
 
-  let open Mltop in
+  let open Loadpath 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
@@ -115,10 +115,10 @@ let libs_init_load_path ~load_init =
 (* 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 open Loadpath in
   let lp s = { recursive = false; path_spec = MlPath s } in
   let add_subdir dl =
-    Mltop.add_coq_path (lp (List.fold_left (/) Envars.coqroot [dl]))
+    Loadpath.add_coq_path (lp (List.fold_left (/) Envars.coqroot [dl]))
   in
-    Mltop.add_coq_path (lp (Envars.coqlib ()));
+    Loadpath.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 c891e736b4..04ec77a025 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -17,7 +17,7 @@ val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State
 val init_ocaml_path : unit -> unit
 
 (* LoadPath for toploop toplevels *)
-val toplevel_init_load_path : unit -> Mltop.coq_path list
+val toplevel_init_load_path : unit -> Loadpath.coq_path list
 
 (* LoadPath for Coq user libraries *)
-val libs_init_load_path : load_init:bool -> Mltop.coq_path list
+val libs_init_load_path : load_init:bool -> Loadpath.coq_path list
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b769405cf6..460c2f126e 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -222,7 +222,7 @@ let init_toplevel ~help ~init custom_init arglist =
     exit 0;
   end;
   let top_lp = Coqinit.toplevel_init_load_path () in
-  List.iter Mltop.add_coq_path top_lp;
+  List.iter Loadpath.add_coq_path top_lp;
   let opts, extras = custom_init ~opts extras in
   Mltop.init_known_plugins ();
 
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       *)
+(* <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
+
+(************************************************************************)
+(*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/library/loadpath.mli b/vernac/loadpath.mli
index 4044ca1127..fe4dc55c21 100644
--- a/library/loadpath.mli
+++ b/vernac/loadpath.mli
@@ -55,3 +55,47 @@ val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list
 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 =