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.

4 files changed, 26 insertions, 16 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);