From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- library/library.ml | 88 ++++++++++++++++++++++++++++++++---------------------- 1 file changed, 52 insertions(+), 36 deletions(-) (limited to 'library/library.ml') diff --git a/library/library.ml b/library/library.ml index 3a3328ad..2904edc2 100644 --- a/library/library.ml +++ b/library/library.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: library.ml 9525 2007-01-24 08:43:01Z herbelin $ *) +(* $Id: library.ml 11181 2008-06-27 07:35:45Z notin $ *) open Pp open Util @@ -86,10 +86,10 @@ let add_load_path (phys_path,coq_path) = begin (* 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) - ^("\nIt is remapped to "^(string_of_dirpath coq_path))); - flush_all ()); + Flags.if_warn msg_warning + (str phys_path ++ strbrk " was previously bound to " ++ + pr_dirpath dir ++ strbrk "; it is remapped to " ++ + pr_dirpath coq_path); remove_load_path phys_path; load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths) end @@ -122,7 +122,6 @@ type library_disk = { 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; @@ -138,10 +137,15 @@ module LibraryOrdered = end module LibraryMap = Map.Make(LibraryOrdered) +module LibraryFilenameMap = Map.Make(LibraryOrdered) (* This is a map from names to loaded libraries *) let libraries_table = ref LibraryMap.empty +(* This is the map of loaded libraries filename *) +(* (not synchronized so as not to be caught in the states on disk) *) +let libraries_filename_table = ref LibraryFilenameMap.empty + (* These are the _ordered_ sets of loaded, imported and exported libraries *) let libraries_loaded_list = ref [] let libraries_imports_list = ref [] @@ -183,7 +187,15 @@ let try_find_library dir = with Not_found -> error ("Unknown library " ^ (string_of_dirpath dir)) -let library_full_filename dir = (find_library dir).library_filename +let register_library_filename dir f = + (* Not synchronized: overwrite the previous binding if one existed *) + (* from a previous play of the session *) + libraries_filename_table := + LibraryFilenameMap.add dir f !libraries_filename_table + +let library_full_filename dir = + try LibraryFilenameMap.find dir !libraries_filename_table + with Not_found -> "" let library_is_loaded dir = try let _ = find_library dir in true @@ -300,7 +312,7 @@ let (in_import, out_import) = (*s Loading from disk to cache (preparation phase) *) -let vo_magic_number = 080992 (* V8.1 beta2 *) +let vo_magic_number = 08193 (* v8.2beta3 *) let (raw_extern_library, raw_intern_library) = System.raw_extern_intern vo_magic_number ".vo" @@ -309,7 +321,7 @@ let with_magic_number_check f a = try f a with System.Bad_magic_number fname -> errorlabstrm "with_magic_number_check" - (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++ + (str"File " ++ str fname ++ spc () ++ str"has bad magic number." ++ spc () ++ str"It is corrupted" ++ spc () ++ str"or was compiled with another version of Coq.") @@ -331,9 +343,9 @@ let locate_absolute_library dir = (dir, file) with Not_found -> (* Last chance, removed from the file system but still in memory *) - try + if library_is_loaded dir then (dir, library_full_filename dir) - with Not_found -> + else raise LibNotFound let locate_qualified_library qid = @@ -351,10 +363,9 @@ let locate_qualified_library qid = let path, file = System.where_in_path loadpath name in let dir = extend_dirpath (find_logical_path path) base in (* Look if loaded *) - try - (LibLoaded, dir, library_full_filename dir) - with Not_found -> - (LibInPath, dir, file) + if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir) + (* Otherwise, look for it in the file system *) + else (LibInPath, dir, file) with Not_found -> raise LibNotFound let explain_locate_library_error qid = function @@ -386,11 +397,10 @@ let try_locate_qualified_library (loc,qid) = (* Internalise libraries *) let lighten_library m = - if !Options.dont_load_proofs then lighten_library m else m + if !Flags.dont_load_proofs then lighten_library m else m -let mk_library md f digest = { +let mk_library md digest = { library_name = md.md_name; - library_filename = f; library_compiled = lighten_library md.md_compiled; library_objects = md.md_objects; library_deps = md.md_deps; @@ -402,7 +412,8 @@ let intern_from_file f = let md = System.marshal_in ch in let digest = System.marshal_in ch in close_in ch; - mk_library md f digest + register_library_filename md.md_name f; + mk_library md digest let rec intern_library needed (dir, f) = (* Look if in the current logical environment *) @@ -426,9 +437,9 @@ and intern_library_deps needed dir m = and intern_mandatory_library caller needed (dir,d) = let m,needed = intern_library needed (try_locate_absolute_library dir) in if d <> m.library_digest then - error ("compiled library "^(string_of_dirpath caller)^ - " makes inconsistent assumptions over library " - ^(string_of_dirpath dir)); + errorlabstrm "" (strbrk ("Compiled library "^(string_of_dirpath caller)^ + ".vo makes inconsistent assumptions over library " + ^(string_of_dirpath dir))); needed let rec_intern_library needed mref = @@ -443,17 +454,18 @@ let check_library_short_name f dir = function | _ -> () let rec_intern_by_filename_only id f = - let m = intern_from_file f in + let m = try intern_from_file f with Sys_error s -> error s in (* Only the base name is expected to match *) check_library_short_name f m.library_name id; (* We check no other file containing same library is loaded *) - try - let m' = find_library m.library_name in - Options.if_verbose warning - ((string_of_dirpath m.library_name)^" is already loaded from file "^ - m'.library_filename); - m.library_name, [] - with Not_found -> + if library_is_loaded m.library_name then + begin + Flags.if_verbose warning + ((string_of_dirpath m.library_name)^" is already loaded from file "^ + library_full_filename m.library_name); + m.library_name, [] + end + else let needed = intern_library_deps [] m.library_name m in m.library_name, needed @@ -496,7 +508,7 @@ let register_library (dir,m) = (* [needed] is the ordered list of libraries not already loaded *) let cache_require (_,(needed,modl,export)) = List.iter register_library needed; - option_iter (fun exp -> open_libraries exp (List.map find_library modl)) + Option.iter (fun exp -> open_libraries exp (List.map find_library modl)) export let load_require _ (_,(needed,modl,_)) = @@ -530,13 +542,17 @@ let require_library qidl export = let modrefl = List.map fst modrefl in if Lib.is_modtype () || Lib.is_module () then begin add_anonymous_leaf (in_require (needed,modrefl,None)); - option_iter (fun exp -> + Option.iter (fun exp -> List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl) export end else add_anonymous_leaf (in_require (needed,modrefl,export)); - if !Options.xml_export then List.iter !xml_require modrefl; + if !Flags.dump then List.iter2 (fun (loc, _) dp -> + Flags.dump_string (Printf.sprintf "R%d %s <> <> %s\n" + (fst (unloc loc)) (string_of_dirpath dp) "lib")) + qidl modrefl; + if !Flags.xml_export then List.iter !xml_require modrefl; add_frozen_state () let require_library_from_file idopt file export = @@ -544,12 +560,12 @@ let require_library_from_file idopt file export = let needed = List.rev needed in if Lib.is_modtype () || Lib.is_module () 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 (modref,exp))) export end else add_anonymous_leaf (in_require (needed,[modref],export)); - if !Options.xml_export then !xml_require modref; + if !Flags.xml_export then !xml_require modref; add_frozen_state () (* the function called by Vernacentries.vernac_import *) @@ -614,7 +630,7 @@ let save_library_to dir f = let di = Digest.file f' in System.marshal_out ch di; close_out ch - with e -> (warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e) + with e -> warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e (************************************************************************) (*s Display the memory use of a library. *) -- cgit v1.2.3