Splitting the library representation on disk in two.

The first part only contains the summary of the library, while the second
one contains the effective content of it.

2 files changed, 36 insertions, 23 deletions

diff --git a/library/library.ml b/library/library.ml
index 0296d7b90..19c8c92f8 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -76,11 +76,15 @@ 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]. *)
@@ -406,19 +410,20 @@ 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_name     = sd.md_name;
     library_compiled = md.md_compiled;
     library_objects  = md.md_objects;
-    library_deps     = md.md_deps;
-    library_imports  = md.md_imports;
+    library_deps     = sd.md_deps;
+    library_imports  = sd.md_imports;
     library_digests  = digests;
     library_extra_univs = univs;
   }
@@ -431,23 +436,24 @@ 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 (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in
+  let (lmd : seg_lib), _, 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 _ = 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_lmd) 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_lmd,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_lmd) Univ.ContextSet.empty
 
 module DPMap = Map.Make(DirPath)
 
@@ -510,7 +516,7 @@ let rec_intern_by_filename_only id f =
 
 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 (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 =
@@ -695,6 +701,7 @@ let load_library_todo f =
     System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
   let f = longf^"io" in
   let ch = System.with_magic_number_check 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
@@ -705,7 +712,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. *)
@@ -769,18 +776,22 @@ 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
   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);
@@ -799,8 +810,9 @@ let save_library_to ?todo dir f otab =
     let () = Sys.remove f' in
     iraise reraise
 
-let save_library_raw f lib univs proofs =
+let save_library_raw f sum lib univs proofs =
   let (f',ch) = raw_extern_library (f^"o") 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);
diff --git a/library/library.mli b/library/library.mli
index 350670680..967a54e4c 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -28,6 +28,7 @@ val require_library_from_file :
 (** {6 ... } *)
 
 (** Segments of a library *)
+type seg_sum
 type seg_lib
 type seg_univ = (* cst, all_cst, finished? *)
   Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool
@@ -47,8 +48,8 @@ val save_library_to :
   DirPath.t -> string -> Opaqueproof.opaquetab -> unit
 
 val load_library_todo :
-  string -> string * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
-val save_library_raw : string -> seg_lib -> seg_univ -> seg_proofs -> unit
+  string -> string * seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
+val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit
 
 (** {6 Interrogate the status of libraries } *)