Imported Upstream version 8.5~beta3+dfsg

1 files changed, 77 insertions, 108 deletions

diff --git a/library/library.ml b/library/library.ml
index b4261309..024ac9e6 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -19,10 +19,12 @@ open Lib
 (************************************************************************)
 (*s Low-level interning/externing of libraries to files *)
 
-(*s Loading from disk to cache (preparation phase) *)
+let raw_extern_library f =
+  System.raw_extern_state Coq_config.vo_magic_number f
 
-let (raw_extern_library, raw_intern_library) =
-  System.raw_extern_intern Coq_config.vo_magic_number
+let raw_intern_library f =
+  System.with_magic_number_check
+    (System.raw_intern_state Coq_config.vo_magic_number) f
 
 (************************************************************************)
 (** Serialized objects loaded on-the-fly *)
@@ -56,7 +58,7 @@ let in_delayed f ch =
 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 ch = 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
@@ -76,19 +78,22 @@ open Delayed
 type compilation_unit_name = DirPath.t
 
 type library_disk = {
-  md_name : compilation_unit_name;
   md_compiled : Safe_typing.compiled_library;
   md_objects : Declaremods.library_objects;
+}
+
+type summary_disk = {
+  md_name : compilation_unit_name;
+  md_imports : compilation_unit_name array;
   md_deps : (compilation_unit_name * Safe_typing.vodigest) array;
-  md_imports : compilation_unit_name array }
+}
 
 (*s Modules loaded in memory contain the following informations. They are
     kept in the global table [libraries_table]. *)
 
 type library_t = {
   library_name : compilation_unit_name;
-  library_compiled : Safe_typing.compiled_library;
-  library_objects : Declaremods.library_objects;
+  library_data : library_disk delayed;
   library_deps : (compilation_unit_name * Safe_typing.vodigest) array;
   library_imports : compilation_unit_name array;
   library_digests : Safe_typing.vodigest;
@@ -126,7 +131,8 @@ let find_library dir =
 let try_find_library dir =
   try find_library dir
   with Not_found ->
-    error ("Unknown library " ^ (DirPath.to_string dir))
+    errorlabstrm "Library.find_library"
+      (str "Unknown library " ++ str (DirPath.to_string dir))
 
 let register_library_filename dir f =
   (* Not synchronized: overwrite the previous binding if one existed *)
@@ -165,8 +171,9 @@ 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
-    if not !Flags.no_native_compiler then
-      Nativelib.link_library ~prefix ~dirname ~basename:f
+    (* This will not produce errors or warnings if the native compiler was
+       not enabled *)
+    Nativelib.link_library ~prefix ~dirname ~basename:f
   in
   let rec aux = function
     | [] -> link m; [libname]
@@ -374,14 +381,14 @@ let access_table what tables dp i =
     | Fetched t -> 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);
+      Flags.if_verbose 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")
+          errorlabstrm "Library.access_table"
+            (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++
+             str ") is inaccessible or corrupted,\ncannot load some " ++
+             str what ++ str " in it.\n")
       in
       tables := LibraryMap.add dp (Fetched t) !tables;
       t
@@ -405,19 +412,19 @@ let () =
 (************************************************************************)
 (* Internalise libraries *)
 
+type seg_sum = summary_disk
 type seg_lib = library_disk
 type seg_univ = (* true = vivo, false = vi *)
   Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool
 type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = Term.constr Future.computation array
 
-let mk_library md digests univs =
+let mk_library sd md digests univs =
   {
-    library_name     = md.md_name;
-    library_compiled = md.md_compiled;
-    library_objects  = md.md_objects;
-    library_deps     = md.md_deps;
-    library_imports  = md.md_imports;
+    library_name     = sd.md_name;
+    library_data     = md;
+    library_deps     = sd.md_deps;
+    library_imports  = sd.md_imports;
     library_digests  = digests;
     library_extra_univs = univs;
   }
@@ -429,24 +436,25 @@ let mk_summary m = {
 }
 
 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 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 (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
   close_in ch;
-  register_library_filename lmd.md_name f;
-  add_opaque_table lmd.md_name (ToFetch del_opaque);
+  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 lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
+  | None -> mk_library lsd lmd (Dvo_or_vi digest_lsd) Univ.ContextSet.empty
   | Some (utab,uall,true) ->
-      add_univ_table lmd.md_name (Fetched utab);
-      mk_library lmd (Dvivo (digest_lmd,digest_u)) uall
+      add_univ_table lsd.md_name (Fetched utab);
+      mk_library lsd lmd (Dvivo (digest_lsd,digest_u)) uall
   | Some (utab,_,false) ->
-      add_univ_table lmd.md_name (Fetched utab);
-      mk_library lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
+      add_univ_table lsd.md_name (Fetched utab);
+      mk_library lsd lmd (Dvo_or_vi digest_lsd) Univ.ContextSet.empty
 
 module DPMap = Map.Make(DirPath)
 
@@ -462,7 +470,7 @@ let rec intern_library (needed, contents) (dir, f) from =
   let m = intern_from_file f in
   if not (DirPath.equal dir m.library_name) then
     errorlabstrm "load_physical_library"
-      (str ("The file " ^ f ^ " contains library") ++ spc () ++
+      (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));
@@ -475,52 +483,18 @@ and intern_library_deps libs dir m from =
 and intern_mandatory_library caller from libs (dir,d) =
   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));
+    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
   libs
 
-let check_library_short_name f dir = function
-  | Some id when not (Id.equal id (snd (split_dirpath dir))) ->
-      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 = 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 *)
-  if library_is_loaded m.library_name then
-    begin
-      msg_warning
-	(pr_dirpath m.library_name ++ str " is already loaded from file " ++
-	str (library_full_filename m.library_name));
-      m.library_name, []
-    end
- else
-    let needed, contents = intern_library_deps ([], DPMap.empty) m.library_name m (Some f) in
-    let needed = List.map (fun dir -> dir, DPMap.find dir contents) needed in
-    m.library_name, needed
-
 let native_name_from_filename 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 ch = raw_intern_library f in
+  let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in
   Nativecode.mod_uid_of_dirpath lmd.md_name
 
-let rec_intern_library_from_file idopt f =
-  (* A name is specified, we have to check it contains library id *)
-  let paths = Loadpath.get_paths () in
-  let _, f =
-    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in
-  rec_intern_by_filename_only idopt f
-
 (**********************************************************************)
 (*s [require_library] loads and possibly opens a library. This is a
     synchronized operation. It is performed as follows:
@@ -539,10 +513,11 @@ let rec_intern_library_from_file idopt f =
 *)
 
 let register_library m =
+  let l = fetch_delayed m.library_data in
   Declaremods.register_library
     m.library_name
-    m.library_compiled
-    m.library_objects
+    l.md_compiled
+    l.md_objects
     m.library_digests
     m.library_extra_univs;
   register_loaded_library (mk_summary m)
@@ -595,25 +570,13 @@ let require_library_from_dirpath modrefl export =
       add_anonymous_leaf (in_require (needed,modrefl,export));
   add_frozen_state ()
 
-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_library ([modref],exp)))
-      export
-  end
-  else
-    add_anonymous_leaf (in_require (needed,[modref],export));
-  add_frozen_state ()
-
 (* the function called by Vernacentries.vernac_import *)
 
 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"))
+      (loc,"import_library", str (string_of_qualid qid) ++ str " is not a module")
 
 let import_module export modl =
   (* Optimization: libraries in a raw in the list are imported
@@ -638,7 +601,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)^" is not a module")))
+                str (string_of_qualid dir) ++ str " is not a module"))
     | [] -> flush acc
   in aux [] modl
 
@@ -650,8 +613,8 @@ let check_coq_overwriting p id =
   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
     errorlabstrm ""
-      (strbrk ("Cannot build module "^DirPath.to_string p^"."^Id.to_string id^
-      ": it starts with prefix \"Coq\" which is reserved for the Coq library."))
+      (str "Cannot build module " ++ str (DirPath.to_string 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
    others caracters than letters, digits, or `_` *)
@@ -673,29 +636,28 @@ let check_module_name s =
     | c -> err c
 
 let start_library f =
-  let paths = Loadpath.get_paths () in
-  let _, longf =
-    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+  let () = if not (Sys.file_exists f) then
+    errorlabstrm "" (hov 0 (str "Can't find file" ++ spc () ++ str f))
+  in
   let ldir0 =
     try
-      let lp = Loadpath.find_load_path (Filename.dirname longf) in
+      let lp = Loadpath.find_load_path (Filename.dirname f) in
       Loadpath.logical lp
     with Not_found -> Nameops.default_root_prefix
   in
-  let file = Filename.basename f in
+  let file = Filename.chop_extension (Filename.basename f) in
   let id = Id.of_string file in
   check_module_name file;
   check_coq_overwriting ldir0 id;
   let ldir = add_dirpath_suffix ldir0 id in
   Declaremods.start_library ldir;
-  ldir,longf
+  ldir
 
 let load_library_todo f =
-  let paths = Loadpath.get_paths () in
-  let _, longf =
-    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+  let longf = Loadpath.locate_file (f^".v") in
   let f = longf^"io" in
-  let ch = System.with_magic_number_check raw_intern_library f in
+  let ch = raw_intern_library f in
+  let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in
   let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in
   let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in
   let (s3 : seg_discharge option), _, _ = System.marshal_in_segment f ch in
@@ -706,7 +668,7 @@ let load_library_todo f =
   if s2 = None then errorlabstrm "restart" (str"not a .vio file");
   if s3 = None then errorlabstrm "restart" (str"not a .vio file");
   if pi3 (Option.get s2) then errorlabstrm "restart" (str"not a .vio file");
-  longf, s1, Option.get s2, Option.get s3, Option.get tasks, s5
+  longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5
 
 (************************************************************************)
 (*s [save_library dir] ends library [dir] and save it to the disk. *)
@@ -770,18 +732,23 @@ let save_library_to ?todo dir f otab =
     if not(is_done_or_todo i x) then Errors.errorlabstrm "library"
       Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
     opaque_table;
-  let md = {
+  let sd = {
     md_name = dir;
+    md_deps = Array.of_list (current_deps ());
+    md_imports = Array.of_list (current_reexports ());
+  } in
+  let md = {
     md_compiled = cenv;
     md_objects = seg;
-    md_deps = Array.of_list (current_deps ());
-    md_imports = Array.of_list (current_reexports ()) } in
-  if Array.exists (fun (d,_) -> DirPath.equal d dir) md.md_deps then
+  } in
+  if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then
     error_recursively_dependent_library dir;
   (* Open the vo file and write the magic number *)
-  let (f',ch) = raw_extern_library f in
+  let f' = f in
+  let ch = raw_extern_library f' in
   try
     (* Writing vo payload *)
+    System.marshal_out_segment f' ch (sd           : seg_sum);
     System.marshal_out_segment f' ch (md           : seg_lib);
     System.marshal_out_segment f' ch (utab         : seg_univ option);
     System.marshal_out_segment f' ch (dtab         : seg_discharge option);
@@ -789,19 +756,21 @@ let save_library_to ?todo dir f otab =
     System.marshal_out_segment f' ch (opaque_table : seg_proofs);
     close_out ch;
     (* Writing native code files *)
-    if not !Flags.no_native_compiler then
+    if !Flags.native_compiler then
       let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
       if not (Nativelib.compile_library dir ast fn) then
-        msg_error (str"Could not compile the library to native code. Skipping.")
+	error "Could not compile the library to native code."
    with reraise ->
     let reraise = Errors.push reraise in
-    let () = msg_warning (str ("Removed file "^f')) in
+    let () = msg_warning (str "Removed file " ++ str f') in
     let () = close_out ch in
     let () = Sys.remove f' in
     iraise reraise
 
-let save_library_raw f lib univs proofs =
-  let (f',ch) = raw_extern_library (f^"o") in
+let save_library_raw f sum lib univs proofs =
+  let f' = f^"o" in
+  let ch = raw_extern_library f' in
+  System.marshal_out_segment f' ch (sum        : seg_sum);
   System.marshal_out_segment f' ch (lib        : seg_lib);
   System.marshal_out_segment f' ch (Some univs : seg_univ option);
   System.marshal_out_segment f' ch (None       : seg_discharge option);