Merge PR #12092: Implement a name-based representation for vo files.

Reviewed-by: ejgallego
Ack-by: gares

1 files changed, 31 insertions, 32 deletions

diff --git a/vernac/library.ml b/vernac/library.ml
index 01f5101764..35b2a18871 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -20,11 +20,11 @@ open Libobject
 (*s Low-level interning/externing of libraries to files *)
 
 let raw_extern_library f =
-  System.raw_extern_state Coq_config.vo_magic_number f
+  ObjFile.open_out ~file:f
 
 let raw_intern_library f =
   System.with_magic_number_check
-    (System.raw_intern_state Coq_config.vo_magic_number) f
+    (fun file -> ObjFile.open_in ~file) f
 
 (************************************************************************)
 (** Serialized objects loaded on-the-fly *)
@@ -35,7 +35,7 @@ module Delayed :
 sig
 
 type 'a delayed
-val in_delayed : string -> in_channel -> 'a delayed * Digest.t
+val in_delayed : string -> ObjFile.in_handle -> segment:string -> 'a delayed * Digest.t
 val fetch_delayed : 'a delayed -> 'a
 
 end =
@@ -43,14 +43,14 @@ struct
 
 type 'a delayed = {
   del_file : string;
-  del_off : int;
+  del_off : int64;
   del_digest : Digest.t;
 }
 
-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; }, digest)
+let in_delayed f ch ~segment =
+  let seg = ObjFile.get_segment ch ~segment in
+  let digest = seg.ObjFile.hash in
+  { del_file = f; del_digest = digest; del_off = seg.ObjFile.pos; }, digest
 
 (** Fetching a table of opaque terms at position [pos] in file [f],
     expecting to find first a copy of [digest]. *)
@@ -58,10 +58,10 @@ let in_delayed f ch =
 let fetch_delayed del =
   let { del_digest = digest; del_file = f; del_off = pos; } = del in
   try
-    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
+    let ch = open_in_bin f in
+    let () = LargeFile.seek_in ch pos in
+    let obj = System.marshal_in f ch in
+    let digest' = Digest.input ch in
     if not (String.equal digest digest') then raise (Faulty f);
     obj
   with e when CErrors.noncritical e -> raise (Faulty f)
@@ -242,12 +242,11 @@ 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), 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 ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in
-  close_in ch;
+  let (lsd : seg_sum), digest_lsd = ObjFile.marshal_in_segment ch ~segment:"summary" in
+  let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch ~segment:"library" in
+  let (univs : seg_univ option), digest_u = ObjFile.marshal_in_segment ch ~segment:"universes" in
+  let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch ~segment:"opaques" in
+  ObjFile.close_in ch;
   register_library_filename lsd.md_name f;
   add_opaque_table lsd.md_name (ToFetch del_opaque);
   let open Safe_typing in
@@ -297,7 +296,7 @@ let rec_intern_library ~lib_resolver libs (dir, f) =
 
 let native_name_from_filename f =
   let ch = raw_intern_library f in
-  let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in
+  let (lmd : seg_sum), digest_lmd = ObjFile.marshal_in_segment ch ~segment:"summary" in
   Nativecode.mod_uid_of_dirpath lmd.md_name
 
 (**********************************************************************)
@@ -392,12 +391,12 @@ let require_library_from_dirpath ~lib_resolver modrefl export =
 
 let load_library_todo f =
   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 tasks, _, _ = System.marshal_in_segment f ch in
-  let (s4 : seg_proofs), _, _ = System.marshal_in_segment f ch in
-  close_in ch;
+  let (s0 : seg_sum), _ = ObjFile.marshal_in_segment ch ~segment:"summary" in
+  let (s1 : seg_lib), _ = ObjFile.marshal_in_segment ch ~segment:"library" in
+  let (s2 : seg_univ option), _ = ObjFile.marshal_in_segment ch ~segment:"universes" in
+  let tasks, _ = ObjFile.marshal_in_segment ch ~segment:"tasks" in
+  let (s4 : seg_proofs), _ = ObjFile.marshal_in_segment ch ~segment:"opaques" in
+  ObjFile.close_in ch;
   if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
   if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
   if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
@@ -433,15 +432,15 @@ let error_recursively_dependent_library dir =
 let save_library_base f sum lib univs tasks proofs =
   let ch = raw_extern_library f in
   try
-    System.marshal_out_segment f ch (sum    : seg_sum);
-    System.marshal_out_segment f ch (lib    : seg_lib);
-    System.marshal_out_segment f ch (univs  : seg_univ option);
-    System.marshal_out_segment f ch (tasks  : 'tasks option);
-    System.marshal_out_segment f ch (proofs : seg_proofs);
-    close_out ch
+    ObjFile.marshal_out_segment ch ~segment:"summary" (sum    : seg_sum);
+    ObjFile.marshal_out_segment ch ~segment:"library" (lib    : seg_lib);
+    ObjFile.marshal_out_segment ch ~segment:"universes" (univs  : seg_univ option);
+    ObjFile.marshal_out_segment ch ~segment:"tasks" (tasks  : 'tasks option);
+    ObjFile.marshal_out_segment ch ~segment:"opaques" (proofs : seg_proofs);
+    ObjFile.close_out ch
   with reraise ->
     let reraise = Exninfo.capture reraise in
-    close_out ch;
+    ObjFile.close_out ch;
     Feedback.msg_warning (str "Removed file " ++ str f);
     Sys.remove f;
     Exninfo.iraise reraise