aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-12-22 11:21:42 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-12-22 11:21:42 +0100
commitafb9c9a65097dd901df18c443ca13ad4bf394985 (patch)
treef1436684288cfcd7db59f1b1e1cf3b2e743af38f /library
parent8c51055e67da3fea8b66ebcff6c82cbea079dcee (diff)
Do not query module files that have already been loaded.
For a script that does just "Require Reals", this avoids 40k queries. Note that this changes the signature of the FileDependency feedback. Indeed, it no longer provides the physical path to the dependency but only its logical path (since the physical path is no longer available). The physical path could still have been recovered thanks to the libraries_filename_table list. But due to the existence of the overwrite_library_filenames function, its content cannot be trusted. So anyone interested in the actual physical path should now also rely on the FileLoaded feedback.
Diffstat (limited to 'library')
-rw-r--r--library/library.ml15
1 files changed, 8 insertions, 7 deletions
diff --git a/library/library.ml b/library/library.ml
index 024ac9e6f..734a50fe3 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -286,12 +286,12 @@ let locate_absolute_library dir =
with Not_found -> [] in
match find ".vo" @ find ".vio" with
| [] -> raise LibNotFound
- | [file] -> dir, file
+ | [file] -> file
| [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
str vo ++ str " because it is more recent");
- dir, vi
- | [vo;vi] -> dir, vo
+ vi
+ | [vo;vi] -> vo
| _ -> assert false
let locate_qualified_library ?root ?(warn = true) qid =
@@ -459,7 +459,7 @@ let intern_from_file f =
module DPMap = Map.Make(DirPath)
let rec intern_library (needed, contents) (dir, f) from =
- Pp.feedback(Feedback.FileDependency (from, f));
+ Pp.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
(* Look if in the current logical environment *)
try (find_library dir).libsum_digests, (needed, contents)
with Not_found ->
@@ -467,6 +467,7 @@ let rec intern_library (needed, contents) (dir, f) from =
try (DPMap.find dir contents).library_digests, (needed, contents)
with Not_found ->
(* [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 m = intern_from_file f in
if not (DirPath.equal dir m.library_name) then
errorlabstrm "load_physical_library"
@@ -481,13 +482,13 @@ and intern_library_deps libs dir m from =
(dir :: needed, DPMap.add dir m contents )
and intern_mandatory_library caller from libs (dir,d) =
- let digest, libs = intern_library libs (try_locate_absolute_library dir) from in
+ let digest, libs = intern_library libs (dir, None) from in
if not (Safe_typing.digest_match ~actual:digest ~required:d) then
errorlabstrm "" (str "Compiled library " ++ str (DirPath.to_string caller) ++ str ".vo makes inconsistent assumptions over library " ++ str (DirPath.to_string dir));
libs
-let rec_intern_library libs mref =
- let _, libs = intern_library libs mref None in
+let rec_intern_library libs (dir, f) =
+ let _, libs = intern_library libs (dir, Some f) None in
libs
let native_name_from_filename f =