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.

8 files changed, 66 insertions, 43 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 3e22c4b18..0a5b5eb88 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -291,12 +291,12 @@ let with_magic_number_check f a =
 
 open Cic
 
-let mk_library md f table digest cst = {
-  library_name = md.md_name;
+let mk_library sd md f table digest cst = {
+  library_name = sd.md_name;
   library_filename = f;
   library_compiled = md.md_compiled;
   library_opaques = table;
-  library_deps = md.md_deps;
+  library_deps = sd.md_deps;
   library_digest = digest;
   library_extra_univs = cst }
 
@@ -310,9 +310,10 @@ let depgraph = ref LibraryMap.empty
 
 let intern_from_file (dir, f) =
   Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush ();
-  let (md,table,opaque_csts,digest) =
+  let (sd,md,table,opaque_csts,digest) =
     try
       let ch = with_magic_number_check raw_intern_library f in
+      let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in
       let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in
       let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in
       let (discharging:'a option), _, _ = System.marshal_in_segment f ch in
@@ -325,9 +326,9 @@ let intern_from_file (dir, f) =
       if not (String.equal (Digest.channel ch pos) checksum) then
         errorlabstrm "intern_from_file" (str "Checksum mismatch");
       let () = close_in ch in
-      if dir <> md.md_name then
+      if dir <> sd.md_name then
         errorlabstrm "intern_from_file"
-          (name_clash_message dir md.md_name f);
+          (name_clash_message dir sd.md_name f);
       if tasks <> None || discharging <> None then
         errorlabstrm "intern_from_file"
           (str "The file "++str f++str " contains unfinished tasks");
@@ -340,25 +341,26 @@ let intern_from_file (dir, f) =
       Validate.validate !Flags.debug Values.v_univopaques opaque_csts;
       end;
       (* Verification of the unmarshalled values *)
+      Validate.validate !Flags.debug Values.v_libsum sd;
       Validate.validate !Flags.debug Values.v_lib md;
       Validate.validate !Flags.debug Values.v_opaques table;
       Flags.if_verbose ppnl (str" done]"); pp_flush ();
       let digest =
         if opaque_csts <> None then Cic.Dviovo (digest,udg)
         else (Cic.Dvo digest) in
-      md,table,opaque_csts,digest
+      sd,md,table,opaque_csts,digest
     with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in
-  depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
-  opaque_tables := LibraryMap.add md.md_name table !opaque_tables;
+  depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph;
+  opaque_tables := LibraryMap.add sd.md_name table !opaque_tables;
   Option.iter (fun (opaque_csts,_,_) ->
     opaque_univ_tables :=
-      LibraryMap.add md.md_name opaque_csts !opaque_univ_tables)
+      LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables)
     opaque_csts;
   let extra_cst =
     Option.default Univ.empty_constraint
       (Option.map (fun (_,cs,_) ->
          Univ.ContextSet.constraints cs) opaque_csts) in
-  mk_library md f table digest extra_cst
+  mk_library sd md f table digest extra_cst
 
 let get_deps (dir, f) =
   try LibraryMap.find dir !depgraph
diff --git a/checker/cic.mli b/checker/cic.mli
index 90a0e9feb..e875e40f0 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -417,12 +417,16 @@ type compiled_library = {
 
 type library_objects
 
-type library_disk = {
+type summary_disk = {
   md_name : compilation_unit_name;
+  md_imports : compilation_unit_name array;
+  md_deps : library_deps;
+}
+
+type library_disk = {
   md_compiled : compiled_library;
   md_objects : library_objects;
-  md_deps : library_deps;
-  md_imports : compilation_unit_name array }
+}
 
 type opaque_table = constr Future.computation array
 type univ_table =
diff --git a/checker/values.ml b/checker/values.ml
index cf93466b0..b2d74821d 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 0a174243f8b06535c9eecbbe8d339fe1 checker/cic.mli
+MD5 f5fd749af797e08efee22122742bc740 checker/cic.mli
 
 *)
 
@@ -350,8 +350,11 @@ let v_stm_seg = v_pair v_tasks v_counters
 
 (** Toplevel structures in a vo (see Cic.mli) *)
 
+let v_libsum =
+  Tuple ("summary", [|v_dp;Array v_dp;v_deps|])
+
 let v_lib =
-  Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps;Array v_dp|])
+  Tuple ("library",[|v_compiled_lib;v_libraryobjs|])
 
 let v_opaques = Array (v_computation v_constr)
 let v_univopaques =
diff --git a/checker/votour.ml b/checker/votour.ml
index 01965bb4b..bb8e06702 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -249,6 +249,7 @@ let visit_vo f =
   Printf.printf
     "At prompt, <n> enters the <n>-th child, u goes up 1 level, x exits\n\n%!";
   let segments = [|
+    make_seg "summary" Values.v_libsum;
     make_seg "library" Values.v_lib;
     make_seg "univ constraints of opaque proofs" Values.v_univopaques;
     make_seg "discharging info" (Opt Any);
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 } *)
 
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index b20722211..4df9603dc 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -10,7 +10,7 @@ open Util
 
 let check_vio (ts,f) =
   Dumpglob.noglob ();
-  let long_f_dot_v, _, _, _, tasks, _ = Library.load_library_todo f in
+  let long_f_dot_v, _, _, _, _, tasks, _ = Library.load_library_todo f in
   Stm.set_compilation_hints long_f_dot_v;
   List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
 
@@ -30,7 +30,7 @@ let schedule_vio_checking j fs =
     let f =
       if Filename.check_suffix f ".vio" then Filename.chop_extension f
       else f in
-    let long_f_dot_v, _,_,_, tasks, _ = Library.load_library_todo f in
+    let long_f_dot_v, _,_,_,_, tasks, _ = Library.load_library_todo f in
     Stm.set_compilation_hints long_f_dot_v;
     let infos = Stm.info_tasks tasks in
     let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7d84ecf6c..bc8aa2fff 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -344,10 +344,10 @@ let compile verbosely f =
       let open Library in
       Dumpglob.noglob ();
       let f = if check_suffix f ".vio" then chop_extension f else f in
-      let lfdv, lib, univs, disch, tasks, proofs = load_library_todo f in
+      let lfdv, sum, lib, univs, disch, tasks, proofs = load_library_todo f in
       Stm.set_compilation_hints lfdv;
       let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
-      Library.save_library_raw lfdv lib univs proofs
+      Library.save_library_raw lfdv sum lib univs proofs
 
 let compile v f = 
   ignore(CoqworkmgrApi.get 1);