From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- library/library.ml | 326 +++++++++++++++++++++++++++++++---------------------- 1 file changed, 193 insertions(+), 133 deletions(-) (limited to 'library/library.ml') diff --git a/library/library.ml b/library/library.ml index b078e2c4..b4261309 100644 --- a/library/library.ml +++ b/library/library.ml @@ -16,6 +16,59 @@ open Nameops open Libobject open Lib +(************************************************************************) +(*s Low-level interning/externing of libraries to files *) + +(*s Loading from disk to cache (preparation phase) *) + +let (raw_extern_library, raw_intern_library) = + System.raw_extern_intern Coq_config.vo_magic_number + +(************************************************************************) +(** Serialized objects loaded on-the-fly *) + +exception Faulty of string + +module Delayed : +sig + +type 'a delayed +val in_delayed : string -> in_channel -> 'a delayed +val fetch_delayed : 'a delayed -> 'a + +end = +struct + +type 'a delayed = { + del_file : string; + del_off : int; + del_digest : Digest.t; +} + +let in_delayed f ch = + let pos = pos_in ch in + let _, digest = System.skip_in_segment f ch in + { del_file = f; del_digest = digest; del_off = pos; } + +(** Fetching a table of opaque terms at position [pos] in file [f], + expecting to find first a copy of [digest]. *) + +let fetch_delayed del = + let { del_digest = digest; del_file = f; del_off = pos; } = del in + try + let ch = System.with_magic_number_check raw_intern_library f in + let () = seek_in ch pos in + let obj, _, digest' = System.marshal_in_segment f ch in + let () = close_in ch in + if not (String.equal digest digest') then raise (Faulty f); + obj + with e when Errors.noncritical e -> raise (Faulty f) + +end + +open Delayed + + (************************************************************************) (*s Modules on disk contain the following informations (after the magic number, and before the digest). *) @@ -42,12 +95,19 @@ type library_t = { library_extra_univs : Univ.universe_context_set; } +type library_summary = { + libsum_name : compilation_unit_name; + libsum_digests : Safe_typing.vodigest; + libsum_imports : compilation_unit_name array; +} + module LibraryOrdered = DirPath module LibraryMap = Map.Make(LibraryOrdered) module LibraryFilenameMap = Map.Make(LibraryOrdered) (* This is a map from names to loaded libraries *) -let libraries_table = Summary.ref LibraryMap.empty ~name:"LIBRARY" +let libraries_table : library_summary LibraryMap.t ref = + Summary.ref LibraryMap.empty ~name:"LIBRARY" (* This is the map of loaded libraries filename *) (* (not synchronized so as not to be caught in the states on disk) *) @@ -89,32 +149,31 @@ let library_is_loaded dir = with Not_found -> false let library_is_opened dir = - List.exists (fun m -> DirPath.equal m.library_name dir) !libraries_imports_list + List.exists (fun name -> DirPath.equal name dir) !libraries_imports_list -let loaded_libraries () = - List.map (fun m -> m.library_name) !libraries_loaded_list +let loaded_libraries () = !libraries_loaded_list -let opened_libraries () = - List.map (fun m -> m.library_name) !libraries_imports_list +let opened_libraries () = !libraries_imports_list (* If a library is loaded several time, then the first occurrence must be performed first, thus the libraries_loaded_list ... *) let register_loaded_library m = + let libname = m.libsum_name in let link m = - let dirname = Filename.dirname (library_full_filename m.library_name) in - let prefix = Nativecode.mod_uid_of_dirpath m.library_name ^ "." in + let dirname = Filename.dirname (library_full_filename libname) in + let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in let f = prefix ^ "cmo" in let f = Dynlink.adapt_filename f in if not !Flags.no_native_compiler then Nativelib.link_library ~prefix ~dirname ~basename:f in let rec aux = function - | [] -> link m; [m] - | m'::_ as l when DirPath.equal m'.library_name m.library_name -> l + | [] -> link m; [libname] + | m'::_ as l when DirPath.equal m' libname -> l | m'::l' -> m' :: aux l' in libraries_loaded_list := aux !libraries_loaded_list; - libraries_table := LibraryMap.add m.library_name m !libraries_table + libraries_table := LibraryMap.add libname m !libraries_table (* ... while if a library is imported/exported several time, then only the last occurrence is really needed - though the imported @@ -125,7 +184,7 @@ let register_loaded_library m = let rec remember_last_of_each l m = match l with | [] -> [m] - | m'::l' when DirPath.equal m'.library_name m.library_name -> remember_last_of_each l' m + | m'::l' when DirPath.equal m' m -> remember_last_of_each l' m | m'::l' -> m' :: remember_last_of_each l' m let register_open_library export m = @@ -139,17 +198,15 @@ let register_open_library export m = (* [open_library export explicit m] opens library [m] if not already opened _or_ if explicitly asked to be (re)opened *) -let eq_lib_name m1 m2 = DirPath.equal m1.library_name m2.library_name - let open_library export explicit_libs m = if (* Only libraries indirectly to open are not reopen *) (* Libraries explicitly mentionned by the user are always reopen *) - List.exists (eq_lib_name m) explicit_libs - || not (library_is_opened m.library_name) + List.exists (fun m' -> DirPath.equal m m') explicit_libs + || not (library_is_opened m) then begin register_open_library export m; - Declaremods.really_import_module (MPfile m.library_name) + Declaremods.really_import_module (MPfile m) end else if export then @@ -164,46 +221,43 @@ let open_libraries export modl = (fun l m -> let subimport = Array.fold_left - (fun l m -> remember_last_of_each l (try_find_library m)) - l m.library_imports - in remember_last_of_each subimport m) + (fun l m -> remember_last_of_each l m) + l m.libsum_imports + in remember_last_of_each subimport m.libsum_name) [] modl in - List.iter (open_library export modl) to_open_list + let explicit = List.map (fun m -> m.libsum_name) modl in + List.iter (open_library export explicit) to_open_list (**********************************************************************) -(* import and export - synchronous operations*) +(* import and export of libraries - synchronous operations *) +(* at the end similar to import and export of modules except that it *) +(* is optimized: when importing several libraries at the same time *) +(* which themselves indirectly imports the very same modules, these *) +(* ones are imported only ones *) -let open_import i (_,(dir,export)) = +let open_import_library i (_,(modl,export)) = if Int.equal i 1 then (* even if the library is already imported, we re-import it *) (* if not (library_is_opened dir) then *) - open_libraries export [try_find_library dir] + open_libraries export (List.map try_find_library modl) -let cache_import obj = - open_import 1 obj +let cache_import_library obj = + open_import_library 1 obj -let subst_import (_,o) = o +let subst_import_library (_,o) = o -let classify_import (_,export as obj) = +let classify_import_library (_,export as obj) = if export then Substitute obj else Dispose -let in_import : DirPath.t * bool -> obj = +let in_import_library : DirPath.t list * bool -> obj = declare_object {(default_object "IMPORT LIBRARY") with - cache_function = cache_import; - open_function = open_import; - subst_function = subst_import; - classify_function = classify_import } + cache_function = cache_import_library; + open_function = open_import_library; + subst_function = subst_import_library; + classify_function = classify_import_library } -(************************************************************************) -(*s Low-level interning/externing of libraries to files *) - -(*s Loading from disk to cache (preparation phase) *) - -let (raw_extern_library, raw_intern_library) = - System.raw_extern_intern Coq_config.vo_magic_number - (************************************************************************) (*s Locate absolute or partially qualified library names in the path *) @@ -214,8 +268,9 @@ type library_location = LibLoaded | LibInPath let locate_absolute_library dir = (* Search in loadpath *) let pref, base = split_dirpath dir in - let loadpath = Loadpath.expand_root_path pref 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 @@ -232,10 +287,20 @@ let locate_absolute_library dir = | [vo;vi] -> dir, vo | _ -> assert false -let locate_qualified_library warn qid = +let locate_qualified_library ?root ?(warn = true) qid = (* Search library in loadpath *) let dir, base = repr_qualid qid in - let loadpath = Loadpath.expand_path dir in + let loadpath = match root with + | None -> Loadpath.expand_path dir + | Some root -> + let filter path = + if is_dirpath_prefix_of root path then + let path = drop_dirpath_prefix root path in + is_dirpath_suffix_of dir path + else false + in + Loadpath.filter_path filter + in let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in let find ext = try @@ -279,14 +344,6 @@ let try_locate_absolute_library dir = | LibUnmappedDir -> error_unmapped_dir (qualid_of_dirpath dir) | LibNotFound -> error_lib_not_found (qualid_of_dirpath dir) -let try_locate_qualified_library (loc,qid) = - try - let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in - dir,f - with - | LibUnmappedDir -> error_unmapped_dir qid - | LibNotFound -> error_lib_not_found qid - (************************************************************************) (** {6 Tables of opaque proof terms} *) @@ -296,34 +353,10 @@ let try_locate_qualified_library (loc,qid) = terms, and access them only when a specific command (e.g. Print or Print Assumptions) needs it. *) -exception Faulty - -(** Fetching a table of opaque terms at position [pos] in file [f], - expecting to find first a copy of [digest]. *) - -let fetch_table what dp (f,pos,digest) = - let dir_path = Names.DirPath.to_string dp in - try - msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); - let ch = System.with_magic_number_check raw_intern_library f in - let () = seek_in ch pos in - if not (String.equal (System.digest_in f ch) digest) then raise Faulty; - let table, pos', digest' = System.marshal_in_segment f ch in - let () = close_in ch in - let ch' = open_in f in - if not (String.equal (Digest.channel ch' pos') digest') then raise Faulty; - let () = close_in ch' in - table - with e when Errors.noncritical e -> - error - ("The file "^f^" (bound to " ^ dir_path ^ - ") is inaccessible or corrupted,\n" ^ - "cannot load some "^what^" in it.\n") - (** Delayed / available tables of opaque terms *) type 'a table_status = - | ToFetch of string * int * Digest.t + | ToFetch of 'a Future.computation array delayed | Fetched of 'a Future.computation array let opaque_tables = @@ -336,25 +369,33 @@ let add_opaque_table dp st = let add_univ_table dp st = univ_tables := LibraryMap.add dp st !univ_tables -let access_table fetch_table add_table tables dp i = - let t = match LibraryMap.find dp tables with +let access_table what tables dp i = + let t = match LibraryMap.find dp !tables with | Fetched t -> t - | ToFetch (f,pos,digest) -> - let t = fetch_table dp (f,pos,digest) in - add_table dp (Fetched t); + | ToFetch f -> + let dir_path = Names.DirPath.to_string dp in + msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); + let t = + try fetch_delayed f + with Faulty f -> + error + ("The file "^f^" (bound to " ^ dir_path ^ + ") is inaccessible or corrupted,\n" ^ + "cannot load some "^what^" in it.\n") + in + tables := LibraryMap.add dp (Fetched t) !tables; t in assert (i < Array.length t); t.(i) let access_opaque_table dp i = - access_table - (fetch_table "opaque proofs") - add_opaque_table !opaque_tables dp i + let what = "opaque proofs" in + access_table what opaque_tables dp i + let access_univ_table dp i = try - Some (access_table - (fetch_table "universe contexts of opaque proofs") - add_univ_table !univ_tables dp i) + let what = "universe contexts of opaque proofs" in + Some (access_table what univ_tables dp i) with Not_found -> None let () = @@ -381,15 +422,22 @@ let mk_library md digests univs = library_extra_univs = univs; } +let mk_summary m = { + libsum_name = m.library_name; + libsum_imports = m.library_imports; + libsum_digests = m.library_digests; +} + let intern_from_file f = let ch = System.with_magic_number_check raw_intern_library f in let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment f ch in let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in let _ = System.skip_in_segment f ch in - let pos, digest = System.skip_in_segment f ch in + let _ = System.skip_in_segment f ch in + let (del_opaque : seg_proofs delayed) = in_delayed f ch in close_in ch; register_library_filename lmd.md_name f; - add_opaque_table lmd.md_name (ToFetch (f,pos,digest)); + add_opaque_table lmd.md_name (ToFetch del_opaque); let open Safe_typing in match univs with | None -> mk_library lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty @@ -402,16 +450,13 @@ let intern_from_file f = module DPMap = Map.Make(DirPath) -let deps_to_string deps = - Array.fold_left (fun s (n, _) -> s^"\n - "^(DirPath.to_string n)) "" deps - let rec intern_library (needed, contents) (dir, f) from = Pp.feedback(Feedback.FileDependency (from, f)); (* Look if in the current logical environment *) - try find_library dir, (needed, contents) + try (find_library dir).libsum_digests, (needed, contents) with Not_found -> (* Look if already listed and consequently its dependencies too *) - try DPMap.find dir contents, (needed, contents) + 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 m = intern_from_file f in @@ -421,15 +466,15 @@ let rec intern_library (needed, contents) (dir, f) from = pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f)); - m, intern_library_deps (needed, contents) dir m (Some f) + m.library_digests, intern_library_deps (needed, contents) dir m (Some 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 (dir :: needed, DPMap.add dir m contents ) and intern_mandatory_library caller from libs (dir,d) = - let m, libs = intern_library libs (try_locate_absolute_library dir) from in - if not (Safe_typing.digest_match ~actual:m.library_digests ~required:d) then + let digest, libs = intern_library libs (try_locate_absolute_library dir) from in + if not (Safe_typing.digest_match ~actual:digest ~required:d) then errorlabstrm "" (strbrk ("Compiled library "^ DirPath.to_string caller ^ ".vo makes inconsistent assumptions over library " ^ DirPath.to_string dir)); @@ -500,7 +545,7 @@ let register_library m = m.library_objects m.library_digests m.library_extra_univs; - register_loaded_library m + register_loaded_library (mk_summary m) (* Follow the semantics of Anticipate object: - called at module or module type closing when a Require occurs in @@ -543,23 +588,19 @@ let require_library_from_dirpath modrefl export = begin add_anonymous_leaf (in_require (needed,modrefl,None)); Option.iter (fun exp -> - List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl) + add_anonymous_leaf (in_import_library (modrefl,exp))) export end else add_anonymous_leaf (in_require (needed,modrefl,export)); add_frozen_state () -let require_library qidl export = - let modrefl = List.map try_locate_qualified_library qidl in - require_library_from_dirpath modrefl export - let require_library_from_file idopt file export = let modref,needed = rec_intern_library_from_file idopt file in let needed = List.rev_map snd needed in if Lib.is_module_or_modtype () then begin add_anonymous_leaf (in_require (needed,[modref],None)); - Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp))) + Option.iter (fun exp -> add_anonymous_leaf (in_import_library ([modref],exp))) export end else @@ -568,21 +609,38 @@ let require_library_from_file idopt file export = (* the function called by Vernacentries.vernac_import *) -let import_module export (loc,qid) = - try - match Nametab.locate_module qid with - | MPfile dir -> - if Lib.is_module_or_modtype () || not export then - add_anonymous_leaf (in_import (dir, export)) - else - add_anonymous_leaf (in_import (dir, export)) - | mp -> - Declaremods.import_module export mp - with - Not_found -> - user_err_loc - (loc,"import_library", - str ((string_of_qualid qid)^" is not a module")) +let safe_locate_module (loc,qid) = + try Nametab.locate_module qid + with Not_found -> + user_err_loc + (loc,"import_library", str (string_of_qualid qid ^ " is not a module")) + +let import_module export modl = + (* Optimization: libraries in a raw in the list are imported + "globally". If there is non-library in the list; it breaks the + optimization For instance: "Import Arith MyModule Zarith" will + not be optimized (possibly resulting in redefinitions, but + "Import MyModule Arith Zarith" and "Import Arith Zarith MyModule" + will have the submodules imported by both Arith and ZArith + imported only once *) + let flush = function + | [] -> () + | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in + let rec aux acc = function + | (loc,dir as m) :: l -> + let m,acc = + try Nametab.locate_module dir, acc + with Not_found-> flush acc; safe_locate_module m, [] in + (match m with + | MPfile dir -> aux (dir::acc) l + | mp -> + flush acc; + try Declaremods.import_module export mp; aux [] l + with Not_found -> + user_err_loc (loc,"import_library", + str ((string_of_qualid dir)^" is not a module"))) + | [] -> flush acc + in aux [] modl (************************************************************************) (*s Initializing the compilation of a library. *) @@ -654,10 +712,13 @@ let load_library_todo f = (*s [save_library dir] ends library [dir] and save it to the disk. *) let current_deps () = - List.map (fun m -> m.library_name, m.library_digests) !libraries_loaded_list + let map name = + let m = try_find_library name in + (name, m.libsum_digests) + in + List.map map !libraries_loaded_list -let current_reexports () = - List.map (fun m -> m.library_name) !libraries_exports_list +let current_reexports () = !libraries_exports_list let error_recursively_dependent_library dir = errorlabstrm "" @@ -683,7 +744,7 @@ let save_library_to ?todo dir f otab = f ^ "o", Future.UUIDSet.empty | Some (l,_) -> f ^ "io", - List.fold_left (fun e r -> Future.UUIDSet.add r.Stateid.uuid e) + List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty l in let cenv, seg, ast = Declaremods.end_library ~except dir in let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in @@ -692,14 +753,17 @@ let save_library_to ?todo dir f otab = | None -> None, None, None | Some (tasks, rcbackup) -> let tasks = - List.map Stateid.(fun r -> - { r with uuid = Future.UUIDMap.find r.uuid f2t_map }) tasks in + List.map Stateid.(fun (r,b) -> + try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b + with Not_found -> assert b; { r with uuid = -1 }, b) + tasks in Some (tasks,rcbackup), Some (univ_table,Univ.ContextSet.empty,false), Some disch_table in let except = Future.UUIDSet.fold (fun uuid acc -> - Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc) + try Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc + with Not_found -> acc) except Int.Set.empty in let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in Array.iteri (fun i x -> @@ -750,11 +814,7 @@ let save_library_raw f lib univs proofs = open Printf -let mem s = - let m = try_find_library s in - h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)" - (CObj.size_kb m) (CObj.size_kb m.library_compiled) - (CObj.size_kb m.library_objects))) +let mem s = Pp.mt () module StringOrd = struct type t = string let compare = String.compare end module StringSet = Set.Make(StringOrd) @@ -762,7 +822,7 @@ module StringSet = Set.Make(StringOrd) let get_used_load_paths () = StringSet.elements (List.fold_left (fun acc m -> StringSet.add - (Filename.dirname (library_full_filename m.library_name)) acc) + (Filename.dirname (library_full_filename m)) acc) StringSet.empty !libraries_loaded_list) let _ = Nativelib.get_load_paths := get_used_load_paths -- cgit v1.2.3