diff options
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 502 |
1 files changed, 260 insertions, 242 deletions
diff --git a/library/library.ml b/library/library.ml index 93ab76371..8dd3c5432 100644 --- a/library/library.ml +++ b/library/library.ml @@ -12,13 +12,16 @@ open Pp open Util open Names +open Libnames open Nameops -open Environ +open Safe_typing open Libobject open Lib open Nametab +open Declaremods -(*s Load path. *) +(*************************************************************************) +(*s Load path. Mapping from physical to logical paths etc.*) type logical_path = dir_path @@ -54,6 +57,7 @@ let canonical_path_name p = (* We give up to find a canonical name and just simplify it... *) strip_path p + let find_logical_path phys_dir = let phys_dir = canonical_path_name phys_dir in match list_filter2 (fun p d -> p = phys_dir) !load_path with @@ -75,7 +79,7 @@ let add_load_path_entry (phys_path,coq_path) = && coq_path = Nameops.default_root_prefix) then begin - (* Assume the user is concerned by module naming *) + (* Assume the user is concerned by library naming *) if dir <> Nameops.default_root_prefix then (Options.if_verbose warning (phys_path^" was previously bound to " ^(string_of_dirpath dir) @@ -95,31 +99,32 @@ let load_path_of_logical_path dir = let get_full_load_path () = List.combine (fst !load_path) (snd !load_path) +(***********************************************************************) (*s Modules on disk contain the following informations (after the magic number, and before the digest). *) type compilation_unit_name = dir_path -type module_disk = { +type library_disk = { md_name : compilation_unit_name; - md_compiled_env : compiled_env; - md_declarations : library_segment; + md_compiled : compiled_library; + md_objects : library_objects; md_deps : (compilation_unit_name * Digest.t) list; md_imports : compilation_unit_name list } (*s Modules loaded in memory contain the following informations. They are - kept in the global table [modules_table]. *) - -type module_t = { - module_name : compilation_unit_name; - module_filename : System.physical_path; - module_compiled_env : compiled_env; - module_declarations : library_segment; - module_deps : (compilation_unit_name * Digest.t) list; - module_imports : compilation_unit_name list; - module_digest : Digest.t } - -module CompUnitOrdered = + kept in the global table [libraries_table]. *) + +type library_t = { + library_name : compilation_unit_name; + library_filename : System.physical_path; + library_compiled : compiled_library; + library_objects : library_objects; + library_deps : (compilation_unit_name * Digest.t) list; + library_imports : compilation_unit_name list; + library_digest : Digest.t } + +module CompilingModuleOrdered = struct type t = dir_path let compare d1 d2 = @@ -127,33 +132,33 @@ module CompUnitOrdered = (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) end -module CompUnitmap = Map.Make(CompUnitOrdered) +module CompilingModulemap = Map.Make(CompilingModuleOrdered) -(* This is a map from names to modules *) -let modules_table = ref CompUnitmap.empty +(* This is a map from names to libraries *) +let libraries_table = ref CompilingModulemap.empty -(* These are the _ordered_ lists of loaded, imported and exported modules *) -let modules_loaded_list = ref [] -let modules_imports_list = ref [] -let modules_exports_list = ref [] +(* These are the _ordered_ lists of loaded, imported and exported libraries *) +let libraries_loaded_list = ref [] +let libraries_imports_list = ref [] +let libraries_exports_list = ref [] let freeze () = - !modules_table, - !modules_loaded_list, - !modules_imports_list, - !modules_exports_list + !libraries_table, + !libraries_loaded_list, + !libraries_imports_list, + !libraries_exports_list let unfreeze (mt,mo,mi,me) = - modules_table := mt; - modules_loaded_list := mo; - modules_imports_list := mi; - modules_exports_list := me + libraries_table := mt; + libraries_loaded_list := mo; + libraries_imports_list := mi; + libraries_exports_list := me let init () = - modules_table := CompUnitmap.empty; - modules_loaded_list := []; - modules_imports_list := []; - modules_exports_list := [] + libraries_table := CompilingModulemap.empty; + libraries_loaded_list := []; + libraries_imports_list := []; + libraries_exports_list := [] let _ = Summary.declare_summary "MODULES" @@ -162,40 +167,42 @@ let _ = Summary.init_function = init; Summary.survive_section = false } -let find_module s = +let find_library s = try - CompUnitmap.find s !modules_table + CompilingModulemap.find s !libraries_table with Not_found -> - error ("Unknown module " ^ (string_of_dirpath s)) + error ("Unknown library " ^ (string_of_dirpath s)) -let module_is_loaded dir = - try let _ = CompUnitmap.find dir !modules_table in true +let library_full_filename m = (find_library m).library_filename + +let library_is_loaded dir = + try let _ = CompilingModulemap.find dir !libraries_table in true with Not_found -> false -let module_is_opened dir = - List.exists (fun m -> m.module_name = dir) !modules_imports_list +let library_is_opened dir = + List.exists (fun m -> m.library_name = dir) !libraries_imports_list -let module_is_exported dir = - List.exists (fun m -> m.module_name = dir) !modules_exports_list +let library_is_exported dir = + List.exists (fun m -> m.library_name = dir) !libraries_exports_list -let loaded_modules () = - List.map (fun m -> m.module_name) !modules_loaded_list +let loaded_libraries () = + List.map (fun m -> m.library_name) !libraries_loaded_list -let opened_modules () = - List.map (fun m -> m.module_name) !modules_imports_list +let opened_libraries () = + List.map (fun m -> m.library_name) !libraries_imports_list - (* If a module is loaded several time, then the first occurrence must - be performed first, thus the modules_loaded_list ... *) + (* If a library is loaded several time, then the first occurrence must + be performed first, thus the libraries_loaded_list ... *) -let register_loaded_module m = +let register_loaded_library m = let rec aux = function | [] -> [m] - | m'::_ as l when m'.module_name = m.module_name -> l + | m'::_ as l when m'.library_name = m.library_name -> l | m'::l' -> m' :: aux l' in - modules_loaded_list := aux !modules_loaded_list; - modules_table := CompUnitmap.add m.module_name m !modules_table + libraries_loaded_list := aux !libraries_loaded_list; + libraries_table := CompilingModulemap.add m.library_name m !libraries_table - (* ... while if a module is imported/exported several time, then + (* ... while if a library is imported/exported several time, then only the last occurrence is really needed - though the imported list may differ from the exported list (consider the sequence Export A; Export B; Import A which results in A;B for exports but @@ -204,87 +211,89 @@ let register_loaded_module m = let rec remember_last_of_each l m = match l with | [] -> [m] - | m'::l' when m'.module_name = m.module_name -> remember_last_of_each l' m + | m'::l' when m'.library_name = m.library_name -> remember_last_of_each l' m | m'::l' -> m' :: remember_last_of_each l' m -let register_open_module export m = - modules_imports_list := remember_last_of_each !modules_imports_list m; +let register_open_library export m = + libraries_imports_list := remember_last_of_each !libraries_imports_list m; if export then - modules_exports_list := remember_last_of_each !modules_exports_list m - -let compunit_cache = ref CompUnitmap.empty - -let module_segment = function - | None -> contents_after None - | Some m -> (find_module m).module_declarations - -let module_full_filename m = (find_module m).module_filename - -let vo_magic_number = 0703 (* V7.3 *) + libraries_exports_list := remember_last_of_each !libraries_exports_list m -let (raw_extern_module, raw_intern_module) = - System.raw_extern_intern vo_magic_number ".vo" +(************************************************************************) +(*s Operations on library objects and opening *) -let segment_rec_iter f = +(*let segment_rec_iter f = let rec apply = function | sp,Leaf obj -> f (sp,obj) | _,OpenedSection _ -> assert false | _,ClosedSection (_,_,seg) -> iter seg - | _,(FrozenState _ | Module _) -> () + | _,(FrozenState _ | CompilingModule _ + | OpenedModule _ | OpenedModtype _) -> () and iter seg = List.iter apply seg in iter -let segment_iter f = +let segment_iter i v f = let rec apply = function - | sp,Leaf obj -> f (sp,obj) + | sp,Leaf obj -> f (i,sp,obj) | _,OpenedSection _ -> assert false | sp,ClosedSection (export,dir,seg) -> - push_section dir; + push_dir v dir (DirClosedSection dir); if export then iter seg - | _,(FrozenState _ | Module _) -> () + | _,(FrozenState _ | CompilingModule _ + | OpenedModule _ | OpenedModtype _) -> () and iter seg = List.iter apply seg in iter +*) -(*s [open_module s] opens a module. The module [s] and all modules needed by +(*s [open_library s] opens a library. The library [s] and all libraries needed by [s] are assumed to be already loaded. When opening [s] we recursively open - all the modules needed by [s] and tagged [exported]. *) + all the libraries needed by [s] and tagged [exported]. *) -let open_objects decls = - segment_iter open_object decls +(*let open_objects i decls = + segment_iter i (Exactly i) open_object decls*) -let open_module export m = - if not (module_is_opened m.module_name) then - (register_open_module export m; - open_objects m.module_declarations) +let open_library export m = + if not (library_is_opened m.library_name) then begin + register_open_library export m; + Declaremods.import_module (MPfile m.library_name) + end else if export then - modules_exports_list := remember_last_of_each !modules_exports_list m + libraries_exports_list := remember_last_of_each !libraries_exports_list m -let open_modules export modl = +let open_libraries export modl = let to_open_list = List.fold_left (fun l m -> let subimport = List.fold_left - (fun l m -> remember_last_of_each l (find_module m)) - [] m.module_imports + (fun l m -> remember_last_of_each l (find_library m)) + [] m.library_imports in remember_last_of_each subimport m) [] modl in - List.iter (open_module export) to_open_list + List.iter (open_library export) to_open_list -(*s [load_module s] loads the module [s] from the disk, and [find_module s] - returns the module of name [s], loading it if necessary. - The boolean [doexp] specifies if we open the modules which are declared + +(************************************************************************) +(*s Loading from disk to cache (preparation phase) *) + +let compunit_cache = ref CompilingModulemap.empty + +let vo_magic_number = 0703 (* V7.3 *) + +let (raw_extern_library, raw_intern_library) = + System.raw_extern_intern vo_magic_number ".vo" + +(*s [load_library s] loads the library [s] from the disk, and [find_library s] + returns the library of name [s], loading it if necessary. + The boolean [doexp] specifies if we open the libraries which are declared exported in the dependencies (it is [true] at the highest level; then same value as for caller is reused in recursive loadings). *) -let load_objects decls = - segment_iter load_object decls - exception LibUnmappedDir exception LibNotFound type library_location = LibLoaded | LibInPath @@ -292,8 +301,8 @@ type library_location = LibLoaded | LibInPath let locate_absolute_library dir = (* Look if loaded in current environment *) try - let m = CompUnitmap.find dir !modules_table in - (dir, m.module_filename) + let m = CompilingModulemap.find dir !libraries_table in + (dir, m.library_filename) with Not_found -> (* Look if in loadpath *) try @@ -313,112 +322,94 @@ let with_magic_number_check f a = spc () ++ str"It is corrupted" ++ spc () ++ str"or was compiled with another version of Coq.") -let rec load_module dir = - try - (* Look if loaded in current env (and consequently its dependencies) *) - CompUnitmap.find dir !modules_table - with Not_found -> - (* [dir] is an absolute name which matches [f] which must be in loadpath *) - let m = - try CompUnitmap.find dir !compunit_cache - with Not_found -> - anomaly ((string_of_dirpath dir)^" should be in cache") - in - List.iter (fun (dir,_) -> ignore (load_module dir)) m.module_deps; - Global.import m.module_compiled_env; - load_objects m.module_declarations; - register_loaded_module m; - Nametab.push_loaded_library m.module_name; - m - -let mk_module md f digest = { - module_name = md.md_name; - module_filename = f; - module_compiled_env = md.md_compiled_env; - module_declarations = md.md_declarations; - module_deps = md.md_deps; - module_imports = md.md_imports; - module_digest = digest } +let mk_library md f digest = { + library_name = md.md_name; + library_filename = f; + library_compiled = md.md_compiled; + library_objects = md.md_objects; + library_deps = md.md_deps; + library_imports = md.md_imports; + library_digest = digest } let intern_from_file f = - let ch = with_magic_number_check raw_intern_module f in + let ch = with_magic_number_check raw_intern_library f in let md = System.marshal_in ch in let digest = System.marshal_in ch in close_in ch; - mk_module md f digest + mk_library md f digest -let rec intern_module (dir, f) = +let rec intern_library (dir, f) = try (* Look if in the current logical environment *) - CompUnitmap.find dir !modules_table + CompilingModulemap.find dir !libraries_table with Not_found -> try (* Look if already loaded in cache and consequently its dependencies *) - CompUnitmap.find dir !compunit_cache + CompilingModulemap.find dir !compunit_cache with Not_found -> (* [dir] is an absolute name which matches [f] which must be in loadpath *) let m = intern_from_file f in - if dir <> m.module_name then - errorlabstrm "load_physical_module" - (str ("The file " ^ f ^ " contains module") ++ spc () ++ - pr_dirpath m.module_name ++ spc () ++ str "and not module" ++ + if dir <> m.library_name then + errorlabstrm "load_physical_library" + (str ("The file " ^ f ^ " contains library") ++ spc () ++ + pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); - compunit_cache := CompUnitmap.add dir m !compunit_cache; - List.iter (intern_mandatory_module dir) m.module_deps; + compunit_cache := CompilingModulemap.add dir m !compunit_cache; + List.iter (intern_mandatory_library dir) m.library_deps; m -and intern_mandatory_module caller (dir,d) = - let m = intern_absolute_module_from dir in - if d <> m.module_digest then - error ("compiled module "^(string_of_dirpath caller)^ - " makes inconsistent assumptions over module " +and intern_mandatory_library caller (dir,d) = + let m = intern_absolute_library_from dir in + if d <> m.library_digest then + error ("compiled library "^(string_of_dirpath caller)^ + " makes inconsistent assumptions over library " ^(string_of_dirpath dir)) -and intern_absolute_module_from dir = +and intern_absolute_library_from dir = try - intern_module (locate_absolute_library dir) + intern_library (locate_absolute_library dir) with | LibUnmappedDir -> let prefix, dir = fst (split_dirpath dir), string_of_dirpath dir in - errorlabstrm "load_absolute_module_from" + errorlabstrm "load_absolute_library_from" (str ("Cannot load "^dir^":") ++ spc () ++ str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ()) | LibNotFound -> - errorlabstrm "load_absolute_module_from" - (str"Cannot find module " ++ pr_dirpath dir ++ str" in loadpath") + errorlabstrm "load_absolute_library_from" + (str"Cannot find library " ++ pr_dirpath dir ++ str" in loadpath") | e -> raise e -let rec_intern_module mref = let _ = intern_module mref in () +let rec_intern_library mref = let _ = intern_library mref in () -let check_module_short_name f dir = function +let check_library_short_name f dir = function | Some id when id <> snd (split_dirpath dir) -> - errorlabstrm "check_module_short_name" - (str ("The file " ^ f ^ " contains module") ++ spc () ++ - pr_dirpath dir ++ spc () ++ str "and not module" ++ spc () ++ + errorlabstrm "check_library_short_name" + (str ("The file " ^ f ^ " contains library") ++ spc () ++ + pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++ pr_id id) | _ -> () let rec_intern_by_filename_only id f = let m = intern_from_file f in (* Only the base name is expected to match *) - check_module_short_name f m.module_name id; - (* We check no other file containing same module is loaded *) + check_library_short_name f m.library_name id; + (* We check no other file containing same library is loaded *) try - let m' = CompUnitmap.find m.module_name !modules_table in + let m' = CompilingModulemap.find m.library_name !libraries_table in Options.if_verbose warning - ((string_of_dirpath m.module_name)^" is already loaded from file "^ - m'.module_filename); - m.module_name + ((string_of_dirpath m.library_name)^" is already loaded from file "^ + m'.library_filename); + m.library_name with Not_found -> - compunit_cache := CompUnitmap.add m.module_name m !compunit_cache; - List.iter (intern_mandatory_module m.module_name) m.module_deps; - m.module_name + compunit_cache := CompilingModulemap.add m.library_name m !compunit_cache; + List.iter (intern_mandatory_library m.library_name) m.library_deps; + m.library_name let locate_qualified_library qid = (* Look if loaded in current environment *) try let dir = Nametab.locate_loaded_library qid in - (LibLoaded, dir, module_full_filename dir) + (LibLoaded, dir, library_full_filename dir) with Not_found -> (* Look if in loadpath *) try @@ -438,7 +429,7 @@ let locate_qualified_library qid = let rec_intern_qualified_library (loc,qid) = try let (_,dir,f) = locate_qualified_library qid in - rec_intern_module (dir,f); + rec_intern_library (dir,f); dir with | LibUnmappedDir -> @@ -449,42 +440,79 @@ let rec_intern_qualified_library (loc,qid) = fnl ()) | LibNotFound -> user_err_loc (loc, "rec_intern_qualified_library", - str"Cannot find module " ++ pr_qualid qid ++ str" in loadpath") + str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath") -let rec_intern_module_from_file idopt f = - (* A name is specified, we have to check it contains module id *) +let rec_intern_library_from_file idopt f = + (* A name is specified, we have to check it contains library id *) let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in rec_intern_by_filename_only idopt f -(*s [require_module] loads and opens a module. This is a synchronized - operation. *) +(**********************************************************************) +(*s [require_library] loads and opens a library. This is a synchronized + operation. It is performed as follows: + + preparation phase: (functions require_library* ) the library and its + dependencies are read from to disk to the compunit_cache + (using intern_* ) -type module_reference = dir_path list * bool option + execution phase: (through add_leaf and cache_require) + the library is loaded in the environment and Nametab, the objects are + registered etc, using functions from Declaremods (via load_library, + which recursively loads its dependencies) -let string_of_module (_,dir,_) = string_of_id (List.hd (repr_dirpath dir)) + + The [read_library] operation is very similar, but has does not "open" + the library +*) + +type library_reference = dir_path list * bool option + +let string_of_library (_,dir,_) = string_of_id (List.hd (repr_dirpath dir)) + +let rec load_library dir = + try + (* Look if loaded in current env (and consequently its dependencies) *) + CompilingModulemap.find dir !libraries_table + with Not_found -> + (* [dir] is an absolute name matching [f] which must be in loadpath *) + let m = + try CompilingModulemap.find dir !compunit_cache + with Not_found -> + anomaly ((string_of_dirpath dir)^" should be in cache") + in + List.iter (fun (dir,_) -> ignore (load_library dir)) m.library_deps; + Declaremods.register_library + m.library_name + m.library_compiled + m.library_objects + m.library_digest; + register_loaded_library m; + m let cache_require (_,(modl,export)) = - let ml = list_map_left load_module modl in + let ml = list_map_left load_library modl in match export with | None -> () - | Some export -> open_modules export ml + | Some export -> open_libraries export ml + +let load_require _ (_,(modl,_)) = + ignore(list_map_left load_library modl) (* keeps the require marker for closed section replay but removes OS dependent fields from .vo files for cross-platform compatibility *) let export_require (l,e) = Some (l,e) let (in_require, out_require) = - declare_object - ("REQUIRE", - { cache_function = cache_require; - load_function = (fun _ -> ()); - open_function = (fun _ -> ()); - export_function = export_require }) + declare_object {(default_object "REQUIRE") with + cache_function = cache_require; + load_function = load_require; + export_function = export_require; + classify_function = (fun (_,o) -> Anticipate o) } -let require_module spec qidl export = +let require_library spec qidl export = (* if sections_are_opened () && Options.verbose () then - warning ("Objets of "^(string_of_module modref)^ + warning ("Objets of "^(string_of_library modref)^ " not surviving sections (e.g. Grammar \nand Hints)\n"^ "will be removed at the end of the section"); *) @@ -492,53 +520,67 @@ let require_module spec qidl export = add_anonymous_leaf (in_require (modrefl,Some export)); add_frozen_state () -let require_module_from_file spec idopt file export = - let modref = rec_intern_module_from_file idopt file in +let require_library_from_file spec idopt file export = + let modref = rec_intern_library_from_file idopt file in add_anonymous_leaf (in_require ([modref],Some export)); add_frozen_state () -let import_module export (loc,qid) = - let modref = - try - Nametab.locate_loaded_library qid - with Not_found -> - user_err_loc - (loc,"import_module", - str ((Nametab.string_of_qualid qid)^" not loaded")) in - add_anonymous_leaf (in_require ([modref],Some export)) - -let read_module qid = +let export_library (loc,qid) = + try + match Nametab.locate_module qid with + MPfile dir -> + add_anonymous_leaf (in_require ([dir],Some true)) + | _ -> + raise Not_found + with + Not_found -> + user_err_loc + (loc,"export_library", + str ((string_of_qualid qid)^" is not a loaded library")) + +let read_library qid = let modref = rec_intern_qualified_library qid in add_anonymous_leaf (in_require ([modref],None)); add_frozen_state () -let read_module_from_file f = +let read_library_from_file f = let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in let modref = rec_intern_by_filename_only None f in add_anonymous_leaf (in_require ([modref],None)); add_frozen_state () -let reload_module (modrefl, export) = +let reload_library (modrefl, export) = add_anonymous_leaf (in_require (modrefl,export)); add_frozen_state () -(*s [save_module s] saves the module [m] to the disk. *) + +(***********************************************************************) +(*s [save_library s] saves the library [m] to the disk. *) + +let start_library f = + let _,longf = + System.find_file_in_path (get_load_path ()) (f^".v") in + let ldir0 = find_logical_path (Filename.dirname longf) in + let id = id_of_string (Filename.basename f) in + let ldir = extend_dirpath ldir0 id in + Declaremods.start_library ldir; + ldir,longf let current_deps () = - List.map (fun m -> (m.module_name, m.module_digest)) !modules_loaded_list + List.map (fun m -> (m.library_name, m.library_digest)) !libraries_loaded_list let current_reexports () = - List.map (fun m -> m.module_name) !modules_exports_list + List.map (fun m -> m.library_name) !libraries_exports_list -let save_module_to s f = - let seg = export_module s in +let save_library_to s f = + let cenv, seg = Declaremods.export_library s in let md = { md_name = s; - md_compiled_env = Global.export s; - md_declarations = seg; + md_compiled = cenv; + md_objects = seg; md_deps = current_deps (); md_imports = current_reexports () } in - let (f',ch) = raw_extern_module f in + let (f',ch) = raw_extern_library f in try System.marshal_out ch md; flush ch; @@ -547,62 +589,38 @@ let save_module_to s f = close_out ch with e -> (warning ("Removed file "^f');close_out ch; Sys.remove f'; raise e) -(*s Iterators. *) - -let fold_all_segments insec f x = - let rec apply acc = function - | sp, Leaf o -> f acc sp o - | _, ClosedSection (_,_,seg) -> - if insec then List.fold_left apply acc seg else acc - | _ -> acc - in - let acc' = - CompUnitmap.fold - (fun _ m acc -> List.fold_left apply acc m.module_declarations) - !modules_table x - in - List.fold_left apply acc' (Lib.contents_after None) - -let iter_all_segments insec f = - let rec apply = function - | sp, Leaf o -> f sp o - | _, ClosedSection (_,_,seg) -> if insec then List.iter apply seg - | _ -> () - in - CompUnitmap.iter - (fun _ m -> List.iter apply m.module_declarations) !modules_table; - List.iter apply (Lib.contents_after None) - -(*s Pretty-printing of modules state. *) - -let fmt_modules_state () = - let opened = opened_modules () - and loaded = loaded_modules () in +(*s Pretty-printing of libraries state. *) + +let fmt_libraries_state () = + let opened = opened_libraries () + and loaded = loaded_libraries () in (str "Imported (open) Modules: " ++ prlist_with_sep pr_spc pr_dirpath opened ++ fnl () ++ str "Loaded Modules: " ++ prlist_with_sep pr_spc pr_dirpath loaded ++ fnl ()) + (*s For tactics/commands requiring vernacular libraries *) -let check_required_module d = +let check_required_library d = let d' = List.map id_of_string d in let dir = make_dirpath (List.rev d') in - if not (module_is_loaded dir) then + if not (library_is_loaded dir) then (* Loading silently ... let m, prefix = list_sep_last d' in - read_module + read_library (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m) *) (* or failing ...*) - error ("Module "^(list_last d)^" has to be required first") + error ("Library "^(list_last d)^" has to be required first") + -(*s Display the memory use of a module. *) +(*s Display the memory use of a library. *) open Printf let mem s = - let m = find_module s in + let m = find_library s in h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)" - (size_kb m) (size_kb m.module_compiled_env) - (size_kb m.module_declarations))) + (size_kb m) (size_kb m.library_compiled) + (size_kb m.library_objects))) |