diff options
| -rw-r--r-- | library/library.ml | 8 | ||||
| -rw-r--r-- | library/loadpath.ml | 8 | ||||
| -rw-r--r-- | library/loadpath.mli | 3 |
3 files changed, 13 insertions, 6 deletions
diff --git a/library/library.ml b/library/library.ml index 64c2c2ad5..a1760cdf1 100644 --- a/library/library.ml +++ b/library/library.ml @@ -754,9 +754,7 @@ let save_library_to ?todo dir f = close_out ch; (* Writing native code files *) if not !Flags.no_native_compiler then - let lp = Loadpath.get_load_paths () in - let map_path p = CUnix.string_of_physical_path (Loadpath.physical p) in - let lp = List.map map_path lp in + let lp = Loadpath.get_accessible_paths () in let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in if not (Int.equal (Nativelibrary.compile_library dir ast lp fn) 0) then msg_error (str"Could not compile the library to native code. Skipping.") @@ -788,8 +786,6 @@ let mem s = (CObj.size_kb m.library_objects))) let get_load_paths_str () = - let lp = Loadpath.get_load_paths () in - let map_path p = CUnix.string_of_physical_path (Loadpath.physical p) in - List.map map_path lp + List.map CUnix.string_of_physical_path (Loadpath.get_accessible_paths ()) let _ = Nativelib.get_load_paths := get_load_paths_str diff --git a/library/loadpath.ml b/library/loadpath.ml index 60799a8a7..7c203bc88 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -22,6 +22,9 @@ type t = { let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS" +let accessible_paths = + Summary.ref ([] : CUnix.physical_path list) ~name:"ACCPATHS" + let logical p = p.path_logical let physical p = p.path_physical @@ -30,6 +33,8 @@ let get_load_paths () = !load_paths let get_paths () = List.map physical !load_paths +let get_accessible_paths () = !accessible_paths + let anomaly_too_many_paths path = anomaly (str "Several logical paths are associated to" ++ spc () ++ str path) @@ -63,6 +68,9 @@ let add_load_path phys_path isroot coq_path = match List.filter filter !load_paths with | [] -> load_paths := binding :: !load_paths; + if isroot then + accessible_paths := List.fold_left (fun acc v -> (fst v) :: acc) + (phys_path :: !accessible_paths) (System.all_subdirs phys_path) | [p] -> let dir = p.path_logical in if not (DirPath.equal coq_path dir) diff --git a/library/loadpath.mli b/library/loadpath.mli index 8928542a6..f755ace9e 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -30,6 +30,9 @@ val get_load_paths : unit -> t list val get_paths : unit -> CUnix.physical_path list (** Same as [get_load_paths] but only get the physical part. *) +val get_accessible_paths : unit -> CUnix.physical_path list +(** Same as [get_paths] but also get paths that can be relatively accessed. *) + val add_load_path : CUnix.physical_path -> bool -> DirPath.t -> unit (** [add_load_path root phys log] adds the binding [phys := log] to the current loadpaths. The [root] flag indicates whether this loadpath has to be treated |