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

Reviewed-by: maximedenes

6 files changed, 387 insertions, 113 deletions

diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml
new file mode 100644
index 0000000000..1bb44d0ef1
--- /dev/null
+++ b/vernac/loadpath.ml
@@ -0,0 +1,273 @@
+(************************************************************************)
+(*         *   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 Util
+module DP = Names.DirPath
+
+(** Load paths. Mapping from physical to logical paths. *)
+
+type t = {
+  path_physical : CUnix.physical_path;
+  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 =
+  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
+  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 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) ->
+       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
+  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 DP.equal coq_path old_path then
+        implicit <> old_implicit
+      else
+        let () =
+          (* Do not warn when overriding the default "-I ." path *)
+          if not (DP.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 Libnames.is_dirpath_suffix_of dir lg
+        else DP.equal dir lg
+      | Some root ->
+        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
+
+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 *)
+
+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"
+    Pp.(fun (vi, vo) ->
+        seq [ str "Loading"; spc (); str vi
+            ; strbrk " instead of "; str vo
+            ; 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
+  let loadpath = filter_path (fun dir -> DP.equal dir pref) in
+  match loadpath with
+  | [] -> Error LibUnmappedDir
+  | _ ->
+    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 =
+  (* Search library in loadpath *)
+  let dir, base = Libnames.repr_qualid qid in
+  let loadpath = expand_path ?root dir in
+  match loadpath with
+  | [] -> Error LibUnmappedDir
+  | _ ->
+    match select_vo_file ~warn loadpath base 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 ()
+            ; DP.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 =
+  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 } *)
+
+(* 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  : 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 =
+  | 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 -> Pp.(str "Cannot open " ++ str unix_path))
+
+let warn_cannot_use_directory =
+  CWarnings.create ~name:"cannot-use-directory" ~category:"filesystem"
+    (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
+  | CErrors.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 = DP.repr lp.coq_path in
+    let convert_dirs (lp, cp) =
+      try
+        let path = List.rev_map convert_string cp @ prefix in
+        Some (lp, DP.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..d393fc35b5
--- /dev/null
+++ b/vernac/loadpath.mli
@@ -0,0 +1,89 @@
+(************************************************************************)
+(*         *   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 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 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 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 } *)
+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
+
+(** 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 828356d31d..b9d1326ba5 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 ()
@@ -444,9 +439,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 +466,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)
-  with
-    | Library.LibUnmappedDir -> err_unmapped_library qid
-    | Library.LibNotFound -> err_notfound_library qid
+  let open Loadpath in
+  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
@@ -1026,18 +1022,18 @@ let vernac_require from import qidl =
     Some (Libnames.add_dirpath_suffix hd tl)
   in
   let locate qid =
-    try
-      let warn = not !Flags.quiet in
-      let (_, dir, f) = Library.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
+    let open Loadpath in
+    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
     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 +1129,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;
@@ -1141,11 +1137,10 @@ 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 =
-  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 =