diff options
| -rw-r--r-- | kernel/nativelib.ml | 9 | ||||
| -rw-r--r-- | kernel/nativelib.mli | 3 | ||||
| -rw-r--r-- | library/library.ml | 15 | ||||
| -rw-r--r-- | library/loadpath.ml | 10 | ||||
| -rw-r--r-- | library/loadpath.mli | 3 |
5 files changed, 17 insertions, 23 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 05e470da9..b877dda8f 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -59,7 +59,8 @@ let write_ml_code fn ?(header=[]) code = List.iter (pp_global fmt) (header@code); close_out ch_out -let call_compiler ml_filename load_path = +let call_compiler ml_filename = + let load_path = !get_load_paths () in let load_path = List.map (fun dn -> dn / output_dir) load_path in let include_dirs = List.map Filename.quote (include_dirs () @ load_path) in let include_dirs = String.concat " -I " include_dirs in @@ -75,9 +76,9 @@ let call_compiler ml_filename load_path = let compile fn code = write_ml_code fn code; - call_compiler fn (!get_load_paths()) + call_compiler fn -let compile_library dir code load_path fn = +let compile_library dir code fn = let header = mk_library_header dir in let fn = fn ^ source_ext in let basename = Filename.basename fn in @@ -86,7 +87,7 @@ let compile_library dir code load_path fn = if not (Sys.file_exists dirname) then Unix.mkdir dirname 0o755; let fn = dirname / basename in write_ml_code fn ~header code; - fst (call_compiler fn load_path) + fst (call_compiler fn) (* call_linker links dynamically the code for constants in environment or a *) (* conversion test. Silently fails if the file does not exist in bytecode *) diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index e577a9032..a2633ac2c 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -18,8 +18,7 @@ val get_ml_filename : unit -> string * string val compile : string -> global list -> int * string -val compile_library : Names.dir_path -> - global list -> string list -> string -> int +val compile_library : Names.dir_path -> global list -> string -> int val call_linker : ?fatal:bool -> string -> string -> code_location_updates option -> unit diff --git a/library/library.ml b/library/library.ml index d2d2d72e4..a9cdf1f2f 100644 --- a/library/library.ml +++ b/library/library.ml @@ -763,9 +763,8 @@ 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_accessible_paths () in let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in - if not (Int.equal (Nativelib.compile_library dir ast lp fn) 0) then + if not (Int.equal (Nativelib.compile_library dir ast fn) 0) then msg_error (str"Could not compile the library to native code. Skipping.") with reraise -> let reraise = Errors.push reraise in @@ -794,7 +793,13 @@ let mem s = (CObj.size_kb m) (CObj.size_kb m.library_compiled) (CObj.size_kb m.library_objects))) -let get_load_paths_str () = - List.map CUnix.string_of_physical_path (Loadpath.get_accessible_paths ()) +module StringOrd = struct type t = string let compare = String.compare end +module StringSet = Set.Make(StringOrd) -let _ = Nativelib.get_load_paths := get_load_paths_str +let get_used_load_paths () = + StringSet.elements + (List.fold_left (fun acc m -> StringSet.add + (Filename.dirname (library_full_filename m.library_name)) acc) + StringSet.empty !libraries_loaded_list) + +let _ = Nativelib.get_load_paths := get_used_load_paths diff --git a/library/loadpath.ml b/library/loadpath.ml index 2a548fcb6..bc6ea8910 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -24,9 +24,6 @@ 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 @@ -35,8 +32,6 @@ 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) @@ -69,10 +64,7 @@ let add_load_path phys_path path_type coq_path = } in match List.filter filter !load_paths with | [] -> - load_paths := binding :: !load_paths; - if path_type <> ImplicitPath then - accessible_paths := List.fold_left (fun acc v -> (fst v) :: acc) - (phys_path :: !accessible_paths) (System.all_subdirs phys_path) + load_paths := binding :: !load_paths | [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 af86122cf..c8bfd2e59 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -35,9 +35,6 @@ 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 -> path_type -> DirPath.t -> unit (** [add_load_path phys type log] adds the binding [phys := log] to the current loadpaths. *) |