From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- library/library.ml | 119 +++++++++++++++++++++++++---------------------------- 1 file changed, 57 insertions(+), 62 deletions(-) (limited to 'library/library.ml') diff --git a/library/library.ml b/library/library.ml index 79e5792c..d44f796a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names @@ -35,7 +35,7 @@ module Delayed : sig type 'a delayed -val in_delayed : string -> in_channel -> 'a delayed +val in_delayed : string -> in_channel -> 'a delayed * Digest.t val fetch_delayed : 'a delayed -> 'a end = @@ -50,7 +50,7 @@ type 'a delayed = { 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; } + ({ del_file = f; del_digest = digest; del_off = pos; }, digest) (** Fetching a table of opaque terms at position [pos] in file [f], expecting to find first a copy of [digest]. *) @@ -64,7 +64,7 @@ let fetch_delayed del = 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) + with e when CErrors.noncritical e -> raise (Faulty f) end @@ -132,7 +132,7 @@ let try_find_library dir = try find_library dir with Not_found -> errorlabstrm "Library.find_library" - (str "Unknown library " ++ str (DirPath.to_string dir)) + (str "Unknown library " ++ pr_dirpath dir) let register_library_filename dir f = (* Not synchronized: overwrite the previous binding if one existed *) @@ -171,9 +171,8 @@ let register_loaded_library m = let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in let f = prefix ^ "cmo" in let f = Dynlink.adapt_filename f in - (* This will not produce errors or warnings if the native compiler was - not enabled *) - Nativelib.link_library ~prefix ~dirname ~basename:f + if not Coq_config.no_native_compiler then + Nativelib.link_library ~prefix ~dirname ~basename:f in let rec aux = function | [] -> link m; [libname] @@ -272,6 +271,12 @@ exception LibUnmappedDir exception LibNotFound type library_location = LibLoaded | LibInPath +let warn_several_object_files = + CWarnings.create ~name:"several-object-files" ~category:"require" + (fun (vi, vo) -> str"Loading" ++ spc () ++ str vi ++ + strbrk " instead of " ++ str vo ++ + strbrk " because it is more recent") + let locate_absolute_library dir = (* Search in loadpath *) let pref, base = split_dirpath dir in @@ -286,28 +291,17 @@ 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 + warn_several_object_files (vi, vo); + vi + | [vo;vi] -> vo | _ -> assert false let locate_qualified_library ?root ?(warn = true) qid = (* Search library in loadpath *) let dir, base = repr_qualid qid 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 loadpath = Loadpath.expand_path ?root dir in let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in let find ext = try @@ -322,8 +316,7 @@ let locate_qualified_library ?root ?(warn = true) qid = | [lpath, file] -> lpath, file | [lpath_vo, vo; lpath_vi, 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"); + warn_several_object_files (vi, vo); lpath_vi, vi | [lpath_vo, vo; _ ] -> lpath_vo, vo | _ -> assert false @@ -381,7 +374,7 @@ let access_table what tables dp i = | Fetched t -> t | ToFetch f -> let dir_path = Names.DirPath.to_string dp in - Flags.if_verbose msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); + Flags.if_verbose Feedback.msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); let t = try fetch_delayed f with Faulty f -> @@ -438,56 +431,59 @@ let mk_summary m = { let intern_from_file f = let ch = raw_intern_library f in let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in - let (lmd : seg_lib delayed) = in_delayed f ch in + let ((lmd : seg_lib delayed), digest_lmd) = in_delayed 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 _ = System.skip_in_segment f ch in - let (del_opaque : seg_proofs delayed) = in_delayed f ch in + let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in close_in ch; register_library_filename lsd.md_name f; add_opaque_table lsd.md_name (ToFetch del_opaque); let open Safe_typing in match univs with - | None -> mk_library lsd lmd (Dvo_or_vi digest_lsd) Univ.ContextSet.empty + | None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty | Some (utab,uall,true) -> add_univ_table lsd.md_name (Fetched utab); - mk_library lsd lmd (Dvivo (digest_lsd,digest_u)) uall + mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall | Some (utab,_,false) -> add_univ_table lsd.md_name (Fetched utab); - mk_library lsd lmd (Dvo_or_vi digest_lsd) Univ.ContextSet.empty + mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty module DPMap = Map.Make(DirPath) 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).libsum_digests, (needed, contents) with Not_found -> (* Look if already listed and consequently its dependencies too *) try (DPMap.find dir contents).library_digests, (needed, contents) with Not_found -> + Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); (* [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" (str "The file " ++ str f ++ str " contains library" ++ spc () ++ pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); - Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f)); - m.library_digests, intern_library_deps (needed, contents) dir m (Some f) + Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f)); + m.library_digests, intern_library_deps (needed, contents) dir m 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 digest, libs = intern_library libs (try_locate_absolute_library dir) from in + let digest, libs = intern_library libs (dir, None) (Some 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)); + errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++ + str " (in file " ++ str from ++ str ") makes inconsistent assumptions \ + over library " ++ pr_dirpath 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 = @@ -557,12 +553,20 @@ let in_require : require_obj -> obj = let (f_xml_require, xml_require) = Hook.make ~default:ignore () +let warn_require_in_module = + CWarnings.create ~name:"require-in-module" ~category:"deprecated" + (fun () -> strbrk "Require inside a module is" ++ + strbrk " deprecated and strongly discouraged. " ++ + strbrk "You can Require a module at toplevel " ++ + strbrk "and optionally Import it inside another one.") + let require_library_from_dirpath modrefl export = let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in let modrefl = List.map fst modrefl in if Lib.is_module_or_modtype () then begin + warn_require_in_module (); add_anonymous_leaf (in_require (needed,modrefl,None)); Option.iter (fun exp -> add_anonymous_leaf (in_import_library (modrefl,exp))) @@ -579,7 +583,7 @@ 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) ++ str " is not a module") + (loc,"import_library", pr_qualid qid ++ str " is not a module") let import_module export modl = (* Optimization: libraries in a raw in the list are imported @@ -604,7 +608,7 @@ let import_module export modl = try Declaremods.import_module export mp; aux [] l with Not_found -> user_err_loc (loc,"import_library", - str (string_of_qualid dir) ++ str " is not a module")) + pr_qualid dir ++ str " is not a module")) | [] -> flush acc in aux [] modl @@ -614,9 +618,9 @@ let import_module export modl = let check_coq_overwriting p id = let l = DirPath.repr p in let is_empty = match l with [] -> true | _ -> false in - if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then + if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then errorlabstrm "" - (str "Cannot build module " ++ str (DirPath.to_string p) ++ str "." ++ pr_id id ++ str "." ++ spc () ++ + (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++ str "it starts with prefix \"Coq\" which is reserved for the Coq library.") (* Verifies that a string starts by a letter and do not contain @@ -638,17 +642,14 @@ let check_module_name s = done | c -> err c -let start_library f = - let () = if not (Sys.file_exists f) then - errorlabstrm "" (hov 0 (str "Can't find file" ++ spc () ++ str f)) - in +let start_library fo = let ldir0 = try - let lp = Loadpath.find_load_path (Filename.dirname f) in + let lp = Loadpath.find_load_path (Filename.dirname fo) in Loadpath.logical lp with Not_found -> Nameops.default_root_prefix in - let file = Filename.chop_extension (Filename.basename f) in + let file = Filename.chop_extension (Filename.basename fo) in let id = Id.of_string file in check_module_name file; check_coq_overwriting ldir0 id; @@ -703,12 +704,13 @@ let error_recursively_dependent_library dir = writing the content and computing the checksum... *) let save_library_to ?todo dir f otab = - let f, except = match todo with + let except = match todo with | None -> assert(!Flags.compilation_mode = Flags.BuildVo); - f ^ "o", Future.UUIDSet.empty + assert(Filename.check_suffix f ".vo"); + Future.UUIDSet.empty | Some (l,_) -> - f ^ "io", + assert(Filename.check_suffix f ".vio"); 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 @@ -732,7 +734,7 @@ let save_library_to ?todo dir f otab = 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 -> - if not(is_done_or_todo i x) then Errors.errorlabstrm "library" + if not(is_done_or_todo i x) then CErrors.errorlabstrm "library" Pp.(str"Proof object "++int i++str" is not checked nor to be checked")) opaque_table; let sd = { @@ -764,8 +766,8 @@ let save_library_to ?todo dir f otab = if not (Nativelib.compile_library dir ast fn) then error "Could not compile the library to native code." with reraise -> - let reraise = Errors.push reraise in - let () = msg_warning (str "Removed file " ++ str f') in + let reraise = CErrors.push reraise in + let () = Feedback.msg_warning (str "Removed file " ++ str f') in let () = close_out ch in let () = Sys.remove f' in iraise reraise @@ -781,13 +783,6 @@ let save_library_raw f sum lib univs proofs = System.marshal_out_segment f' ch (proofs : seg_proofs); close_out ch -(************************************************************************) -(*s Display the memory use of a library. *) - -open Printf - -let mem s = Pp.mt () - module StringOrd = struct type t = string let compare = String.compare end module StringSet = Set.Make(StringOrd) -- cgit v1.2.3