Implement a name-based representation for vo files.

See CEP#44 for futher details.

7 files changed, 387 insertions, 130 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 4212aac6ea..8881e05ab6 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -255,7 +255,7 @@ let try_locate_qualified_library lib = match lib with
 (*s Low-level interning of libraries from files *)
 
 let raw_intern_library f =
-  System.raw_intern_state Coq_config.vo_magic_number f
+  System.ObjFile.open_in ~file:f
 
 (************************************************************************)
 (* Internalise libraries *)
@@ -294,57 +294,56 @@ type intern_mode = Rec | Root | Dep (* Rec = standard, Root = -norec, Dep = depe
 (* Dependency graph *)
 let depgraph = ref LibraryMap.empty
 
-let marshal_in_segment ~validate ~value f ch =
+let marshal_in_segment ~validate ~value ~segment f ch =
+  let () = LargeFile.seek_in ch segment.System.ObjFile.pos in
   if validate then
-    let v, stop, digest =
+    let v =
       try
-        let stop = input_binary_int ch in
         let v = Analyze.parse_channel ch in
         let digest = Digest.input ch in
-        v, stop, digest
+        let () = if not (String.equal digest segment.System.ObjFile.hash) then raise Exit in
+        v
       with _ ->
         user_err (str "Corrupted file " ++ quote (str f))
     in
     let () = Validate.validate value v in
     let v = Analyze.instantiate v in
-    Obj.obj v, stop, digest
+    Obj.obj v
   else
-    System.marshal_in_segment f ch
+    System.marshal_in f ch
 
-let skip_in_segment f ch =
-  try
-    let stop = (input_binary_int ch : int) in
-    seek_in ch stop;
-    let digest = Digest.input ch in
-    stop, digest
-  with _ ->
-    user_err (str "Corrupted file " ++ quote (str f))
-
-let marshal_or_skip ~validate ~value f ch =
+let marshal_or_skip ~validate ~value ~segment f ch =
   if validate then
-    let v, pos, digest = marshal_in_segment ~validate ~value f ch in
-    Some v, pos, digest
+    let v = marshal_in_segment ~validate:true ~value ~segment f ch in
+    Some v
   else
-    let pos, digest = skip_in_segment f ch in
-    None, pos, digest
+    None
 
 let intern_from_file ~intern_mode (dir, f) =
   let validate = intern_mode <> Dep in
   Flags.if_verbose chk_pp (str"[intern "++str f++str" ...");
   let (sd,md,table,opaque_csts,digest) =
     try
+      (* First pass to read the metadata of the file *)
       let ch = System.with_magic_number_check raw_intern_library f in
-      let (sd:summary_disk), _, digest = marshal_in_segment ~validate ~value:Values.v_libsum f ch in
-      let (md:library_disk), _, digest = marshal_in_segment ~validate ~value:Values.v_lib f ch in
-      let (opaque_csts:seg_univ option), _, udg = marshal_in_segment ~validate ~value:Values.v_univopaques f ch in
-      let (tasks:'a option), _, _ = marshal_in_segment ~validate ~value:Values.(Opt Any) f ch in
-      let (table:seg_proofs option), pos, checksum =
-        marshal_or_skip ~validate ~value:Values.v_opaquetable f ch in
+      let seg_sd = System.ObjFile.get_segment ch ~segment:"summary" in
+      let seg_md = System.ObjFile.get_segment ch ~segment:"library" in
+      let seg_univs = System.ObjFile.get_segment ch ~segment:"universes" in
+      let seg_tasks = System.ObjFile.get_segment ch ~segment:"tasks" in
+      let seg_opaque = System.ObjFile.get_segment ch ~segment:"opaques" in
+      let () = System.ObjFile.close_in ch in
+      (* Actually read the data *)
+      let ch = open_in f in
+
+      let (sd:summary_disk) = marshal_in_segment ~validate ~value:Values.v_libsum ~segment:seg_sd f ch in
+      let (md:library_disk) = marshal_in_segment ~validate ~value:Values.v_lib ~segment:seg_md f ch in
+      let (opaque_csts:seg_univ option) = marshal_in_segment ~validate ~value:Values.v_univopaques ~segment:seg_univs f ch in
+      let (tasks:'a option) = marshal_in_segment ~validate ~value:Values.(Opt Any) ~segment:seg_tasks f ch in
+      let (table:seg_proofs option) =
+        marshal_or_skip ~validate ~value:Values.v_opaquetable ~segment:seg_opaque f ch in
       (* Verification of the final checksum *)
       let () = close_in ch in
       let ch = open_in_bin f in
-      if not (String.equal (Digest.channel ch pos) checksum) then
-        user_err ~hdr:"intern_from_file" (str "Checksum mismatch");
       let () = close_in ch in
       if dir <> sd.md_name then
         user_err ~hdr:"intern_from_file"
@@ -361,8 +360,9 @@ let intern_from_file ~intern_mode (dir, f) =
       end;
       Flags.if_verbose chk_pp (str" done]" ++ fnl ());
       let digest =
-        if opaque_csts <> None then Safe_typing.Dvivo (digest,udg)
-        else (Safe_typing.Dvo_or_vi digest) in
+        let open System.ObjFile in
+        if opaque_csts <> None then Safe_typing.Dvivo (seg_md.hash, seg_univs.hash)
+        else (Safe_typing.Dvo_or_vi seg_md.hash) in
       sd,md,table,opaque_csts,digest
     with e -> Flags.if_verbose chk_pp (str" failed!]" ++ fnl ()); raise e in
   depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph;
diff --git a/checker/votour.ml b/checker/votour.ml
index a83ba20dd6..3fb3ccadf4 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -349,14 +349,63 @@ let parse_header chan =
   let size64 = input_binary_int chan in
   { magic; length; size32; size64; objects }
 
+module ObjFile =
+struct
+
 type segment = {
   name : string;
-  mutable pos : int;
-  typ : Values.value;
+  pos : int64;
+  len : int64;
+  hash : Digest.t;
   mutable header : header;
 }
 
-let make_seg name typ = { name; typ; pos = 0; header = dummy_header }
+let input_int32 ch =
+  let accu = ref 0l in
+  for _i = 0 to 3 do
+    let c = input_byte ch in
+    accu := Int32.add (Int32.shift_left !accu 8) (Int32.of_int c)
+  done;
+  !accu
+
+let input_int64 ch =
+  let accu = ref 0L in
+  for _i = 0 to 7 do
+    let c = input_byte ch in
+    accu := Int64.add (Int64.shift_left !accu 8) (Int64.of_int c)
+  done;
+  !accu
+
+let input_segment_summary ch =
+  let nlen = input_int32 ch in
+  let name = really_input_string ch (Int32.to_int nlen) in
+  let pos = input_int64 ch in
+  let len = input_int64 ch in
+  let hash = Digest.input ch in
+  { name; pos; len; hash; header = dummy_header }
+
+let rec input_segment_summaries ch n accu =
+  if Int32.equal n 0l then Array.of_list (List.rev accu)
+  else
+    let s = input_segment_summary ch in
+    let accu = s :: accu in
+    input_segment_summaries ch (Int32.pred n) accu
+
+let parse_segments ch =
+  let magic = input_int32 ch in
+  let version = input_int32 ch in
+  let summary_pos = input_int64 ch in
+  let () = LargeFile.seek_in ch summary_pos in
+  let nsum = input_int32 ch in
+  let seg = input_segment_summaries ch nsum [] in
+  for i = 0 to Array.length seg - 1 do
+    let () = LargeFile.seek_in ch seg.(i).pos in
+    let header = parse_header ch in
+    seg.(i).header <- header
+  done;
+  (magic, version, seg)
+
+end
 
 let visit_vo f =
   Printf.printf "\nWelcome to votour !\n";
@@ -364,13 +413,13 @@ let visit_vo f =
   Printf.printf "Object sizes are in words (%d bits)\n" Sys.word_size;
   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 "STM tasks" (Opt Values.v_stm_seg);
-    make_seg "opaque proofs" Values.v_opaquetable;
-  |] in
+  let known_segments = [
+    "summary", Values.v_libsum;
+    "library", Values.v_lib;
+    "universes", Values.v_univopaques;
+    "tasks", (Opt Values.v_stm_seg);
+    "opaques", Values.v_opaquetable;
+  ] in
   let repr =
     if Sys.word_size = 64 then (module ReprMem : S) else (module ReprObj : S)
     (* On 32-bit machines, representation may exceed the max size of arrays *)
@@ -379,28 +428,23 @@ let visit_vo f =
   let module Visit = Visit(Repr) in
   while true do
     let ch = open_in_bin f in
-    let magic = input_binary_int ch in
-    Printf.printf "File format: %d\n%!" magic;
-    for i=0 to Array.length segments - 1 do
-      let pos = input_binary_int ch in
-      segments.(i).pos <- pos_in ch;
-      let header = parse_header ch in
-      segments.(i).header <- header;
-      seek_in ch pos;
-      ignore(Digest.input ch);
-    done;
+    let (_magic, version, segments) = ObjFile.parse_segments ch in
+    Printf.printf "File format: %ld\n%!" version;
     Printf.printf "The file has %d segments, choose the one to visit:\n"
       (Array.length segments);
-    Array.iteri (fun i { name; pos; header } ->
+    Array.iteri (fun i ObjFile.{ name; pos; header } ->
       let size = if Sys.word_size = 64 then header.size64 else header.size32 in
-      Printf.printf "  %d: %s, starting at byte %d (size %iw)\n" i name pos size)
+      Printf.printf "  %d: %s, starting at byte %Ld (size %iw)\n" i name pos size)
       segments;
     match read_num (Array.length segments) with
     | Some seg ->
-       seek_in ch segments.(seg).pos;
+       let seg = segments.(seg) in
+       let open ObjFile in
+       LargeFile.seek_in ch seg.pos;
        let o = Repr.input ch in
        let () = Visit.init () in
-       Visit.visit segments.(seg).typ o []
+       let typ = try List.assoc seg.name known_segments with Not_found -> Any in
+       Visit.visit typ o []
     | None -> ()
   done
 
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 6ed4bf9b8e..12856cb6e6 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -35,7 +35,7 @@ val caml_version : string    (* OCaml version used to compile Coq *)
 val caml_version_nums : int list    (* OCaml version used to compile Coq by components *)
 val date : string       (* release date *)
 val compile_date : string (* compile date *)
-val vo_magic_number : int
+val vo_version : int32
 val state_magic_number : int
 
 val all_src_dirs : string list
diff --git a/configure.ml b/configure.ml
index 282b40db27..0eff70999d 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1059,6 +1059,7 @@ let write_configml f =
   let pr_s = pr "let %s = %S\n" in
   let pr_b = pr "let %s = %B\n" in
   let pr_i = pr "let %s = %d\n" in
+  let pr_i32 = pr "let %s = %dl\n" in
   let pr_p s o = pr "let %s = %S\n" s
     (match o with Relative s -> s | Absolute s -> s) in
   let pr_li n l = pr "let %s = [%s]\n" n (String.concat ";" (List.map string_of_int l)) in
@@ -1086,7 +1087,7 @@ let write_configml f =
   pr_s "exec_extension" exe;
   pr "let gtk_platform = `%s\n" !idearchdef;
   pr_b "has_natdynlink" hasnatdynlink;
-  pr_i "vo_magic_number" vo_magic;
+  pr_i32 "vo_version" vo_magic;
   pr_i "state_magic_number" state_magic;
   pr_s "browser" browser;
   pr_s "wwwcoq" !prefs.coqwebsite;
diff --git a/lib/system.ml b/lib/system.ml
index d7f5fa26ab..32e5a53821 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -182,36 +182,9 @@ let marshal_in filename ch =
   | End_of_file -> error_corrupted filename "premature end of file"
   | Failure s -> error_corrupted filename s
 
-let digest_out = Digest.output
-let digest_in filename ch =
-  try Digest.input ch
-  with
-  | End_of_file -> error_corrupted filename "premature end of file"
-  | Failure s -> error_corrupted filename s
-
-let marshal_out_segment f ch v =
-  let start = pos_out ch in
-  output_binary_int ch 0;  (* dummy value for stop *)
-  marshal_out ch v;
-  let stop = pos_out ch in
-  seek_out ch start;
-  output_binary_int ch stop;
-  seek_out ch stop;
-  digest_out ch (Digest.file f)
-
-let marshal_in_segment f ch =
-  let stop = (input_binary_int f ch : int) in
-  let v = marshal_in f ch in
-  let digest = digest_in f ch in
-  v, stop, digest
-
-let skip_in_segment f ch =
-  let stop = (input_binary_int f ch : int) in
-  seek_in ch stop;
-  stop, digest_in f ch
-
-type magic_number_error = {filename: string; actual: int; expected: int}
+type magic_number_error = {filename: string; actual: int32; expected: int32}
 exception Bad_magic_number of magic_number_error
+exception Bad_version_number of magic_number_error
 
 let raw_extern_state magic filename =
   let channel = open_trapping_failure filename in
@@ -225,8 +198,8 @@ let raw_intern_state magic filename =
     if not (Int.equal actual_magic magic) then
         raise (Bad_magic_number {
             filename=filename;
-            actual=actual_magic;
-            expected=magic});
+            actual=Int32.of_int actual_magic;
+            expected=Int32.of_int magic});
     channel
   with
   | End_of_file -> error_corrupted filename "premature end of file"
@@ -256,13 +229,231 @@ let intern_state magic filename =
 
 let with_magic_number_check f a =
   try f a
-  with Bad_magic_number {filename=fname;actual=actual;expected=expected} ->
+  with
+  | Bad_magic_number {filename=fname; _} ->
+    CErrors.user_err ~hdr:"with_magic_number_check"
+    (str"File " ++ str fname ++ strbrk" is corrupted.")
+  | Bad_version_number {filename=fname;actual=actual;expected=expected} ->
     CErrors.user_err ~hdr:"with_magic_number_check"
-    (str"File " ++ str fname ++ strbrk" has bad magic number " ++
-    int actual ++ str" (expected " ++ int expected ++ str")." ++
+    (str"File " ++ str fname ++ strbrk" has bad version number " ++
+    (str @@ Int32.to_string actual) ++ str" (expected " ++ (str @@ Int32.to_string expected) ++ str")." ++
     spc () ++
     strbrk "It is corrupted or was compiled with another version of Coq.")
 
+module ObjFile =
+struct
+
+let magic_number = 0x436F7121l (* "Coq!" *)
+
+(*
+
+int32: big-endian, 4 bytes
+int64: big-endian, 8 bytes
+
+-- string --
+int32 | length of the next field
+data  |
+
+-- segment summary --
+string | name
+int64  | absolute position
+int64  | length (without hash)
+hash   | MD5 (16 bytes)
+
+-- segment --
+...  | binary data
+hash | MD5 (16 bytes)
+
+-- summary --
+int32 | number of segment summaries
+s1    |
+...   | segment summaries
+sn    |
+
+-- vo --
+int32   | magic number
+int32   | Coq version
+int64   | absolute position of the summary
+...     | segments
+summary |
+
+*)
+
+type segment = {
+  name : string;
+  pos : int64;
+  len : int64;
+  hash : Digest.t;
+}
+
+type in_handle = {
+  in_filename : string;
+  in_channel : in_channel;
+  in_segments : segment CString.Map.t;
+}
+
+type out_handle = {
+  out_filename : string;
+  out_channel : out_channel;
+  mutable out_segments : segment CString.Map.t;
+}
+
+let input_int32 ch =
+  let accu = ref 0l in
+  for _i = 0 to 3 do
+    let c = input_byte ch in
+    accu := Int32.add (Int32.shift_left !accu 8) (Int32.of_int c)
+  done;
+  !accu
+
+let input_int64 ch =
+  let accu = ref 0L in
+  for _i = 0 to 7 do
+    let c = input_byte ch in
+    accu := Int64.add (Int64.shift_left !accu 8) (Int64.of_int c)
+  done;
+  !accu
+
+let output_int32 ch n =
+  for i = 0 to 3 do
+    output_byte ch (Int32.to_int (Int32.shift_right_logical n (24 - 8 * i)))
+  done
+
+let output_int64 ch n =
+  for i = 0 to 7 do
+    output_byte ch (Int64.to_int (Int64.shift_right_logical n (56 - 8 * i)))
+  done
+
+let input_segment_summary ch =
+  let nlen = input_int32 ch in
+  let name = really_input_string ch (Int32.to_int nlen) in
+  let pos = input_int64 ch in
+  let len = input_int64 ch in
+  let hash = Digest.input ch in
+  { name; pos; len; hash }
+
+let output_segment_summary ch seg =
+  let nlen = Int32.of_int (String.length seg.name) in
+  let () = output_int32 ch nlen in
+  let () = output_string ch seg.name in
+  let () = output_int64 ch seg.pos in
+  let () = output_int64 ch seg.len in
+  let () = Digest.output ch seg.hash in
+  ()
+
+let rec input_segment_summaries ch n accu =
+  if Int32.equal n 0l then accu
+  else
+    let s = input_segment_summary ch in
+    let accu = CString.Map.add s.name s accu in
+    input_segment_summaries ch (Int32.pred n) accu
+
+let marshal_in_segment (type a) h ~segment : a * Digest.t =
+  let { in_channel = ch } = h in
+  let s = CString.Map.find segment h.in_segments in
+  let () = LargeFile.seek_in ch s.pos in
+  let (v : a) = marshal_in h.in_filename ch in
+  let () = assert (Int64.equal (LargeFile.pos_in ch) (Int64.add s.pos s.len)) in
+  let h = Digest.input ch in
+  let () = assert (String.equal h s.hash) in
+  (v, s.hash)
+
+let marshal_out_segment h ~segment v =
+  let { out_channel = ch } = h in
+  let () = assert (not (CString.Map.mem segment h.out_segments)) in
+  let pos = LargeFile.pos_out ch in
+  let () = Marshal.to_channel ch v [] in
+  let () = flush ch in
+  let pos' = LargeFile.pos_out ch in
+  let len = Int64.sub pos' pos in
+  let hash =
+    let in_ch = open_in h.out_filename in
+    let () = LargeFile.seek_in in_ch pos in
+    let digest = Digest.channel in_ch (Int64.to_int len) in
+    let () = close_in in_ch in
+    digest
+  in
+  let () = Digest.output ch hash in
+  let s = { name = segment; pos; len; hash } in
+  let () = h.out_segments <- CString.Map.add segment s h.out_segments in
+  ()
+
+let marshal_out_binary h ~segment =
+  let { out_channel = ch } = h in
+  let () = assert (not (CString.Map.mem segment h.out_segments)) in
+  let pos = LargeFile.pos_out ch in
+  let finish () =
+    let () = flush ch in
+    let pos' = LargeFile.pos_out ch in
+    let len = Int64.sub pos' pos in
+    let hash =
+      let in_ch = open_in h.out_filename in
+      let () = LargeFile.seek_in in_ch pos in
+      let digest = Digest.channel in_ch (Int64.to_int len) in
+      let () = close_in in_ch in
+      digest
+    in
+    let () = Digest.output ch hash in
+    let s = { name = segment; pos; len; hash } in
+    h.out_segments <- CString.Map.add segment s h.out_segments
+  in
+  ch, finish
+
+let open_in ~file =
+  try
+    let ch = open_in_bin file in
+    let magic = input_int32 ch in
+    let version = input_int32 ch in
+    let () =
+      if not (Int32.equal magic magic_number) then
+        let e = { filename = file; actual = version; expected = magic_number } in
+        raise (Bad_magic_number e)
+    in
+    let () =
+      let expected = Coq_config.vo_version in
+      if not (Int32.equal version expected) then
+        let e = { filename = file; actual = version; expected } in
+        raise (Bad_version_number e)
+    in
+    let summary_pos = input_int64 ch in
+    let () = LargeFile.seek_in ch summary_pos in
+    let nsum = input_int32 ch in
+    let seg = input_segment_summaries ch nsum CString.Map.empty in
+    { in_filename = file; in_channel = ch; in_segments = seg }
+  with
+  | End_of_file -> error_corrupted file "premature end of file"
+  | Failure s | Sys_error s -> error_corrupted file s
+
+let close_in ch =
+  close_in ch.in_channel
+
+let get_segment ch ~segment =
+  CString.Map.find segment ch.in_segments
+
+let segments ch = ch.in_segments
+
+let open_out ~file =
+  let ch = open_trapping_failure file in
+  let () = output_int32 ch magic_number in
+  let () = output_int32 ch Coq_config.vo_version in
+  let () = output_int64 ch 0L (* placeholder *) in
+  { out_channel = ch; out_segments = CString.Map.empty; out_filename = file }
+
+let close_out { out_channel = ch; out_segments = seg } =
+  let () = flush ch in
+  let pos = LargeFile.pos_out ch in
+  (* Write the segment summary *)
+  let () = output_int32 ch (Int32.of_int (CString.Map.cardinal seg)) in
+  let iter _ s = output_segment_summary ch s in
+  let () = CString.Map.iter iter seg in
+  (* Overwrite the position place holder *)
+  let () = LargeFile.seek_out ch 8L in
+  let () = output_int64 ch pos in
+  let () = flush ch in
+  close_out ch
+
+end
+
 (* Time stamps. *)
 
 type time = float * float * float
diff --git a/lib/system.mli b/lib/system.mli
index 00701379bd..7e02b76203 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -68,8 +68,9 @@ val file_exists_respecting_case : string -> string -> bool
   when the check fails, with the full file name and expected/observed magic
   numbers. *)
 
-type magic_number_error = {filename: string; actual: int; expected: int}
+type magic_number_error = {filename: string; actual: int32; expected: int32}
 exception Bad_magic_number of magic_number_error
+exception Bad_version_number of magic_number_error
 
 val raw_extern_state : int -> string -> out_channel
 
@@ -87,14 +88,35 @@ val with_magic_number_check : ('a -> 'b) -> 'a -> 'b
 val marshal_out : out_channel -> 'a -> unit
 val marshal_in : string -> in_channel -> 'a
 
-(** Clones of Digest.output and Digest.input (with nice error message) *)
+module ObjFile :
+sig
 
-val digest_out : out_channel -> Digest.t -> unit
-val digest_in : string -> in_channel -> Digest.t
+val magic_number : int32
 
-val marshal_out_segment : string -> out_channel -> 'a -> unit
-val marshal_in_segment : string -> in_channel -> 'a * int * Digest.t
-val skip_in_segment : string -> in_channel -> int * Digest.t
+type segment = {
+  name : string;
+  pos : int64;
+  len : int64;
+  hash : Digest.t;
+}
+
+type in_handle
+type out_handle
+
+val open_in : file:string -> in_handle
+val close_in : in_handle -> unit
+val marshal_in_segment : in_handle -> segment:string -> 'a * Digest.t
+val get_segment : in_handle -> segment:string -> segment
+val segments : in_handle -> segment CString.Map.t
+
+val open_out : file:string -> out_handle
+val close_out : out_handle -> unit
+val marshal_out_segment : out_handle -> segment:string -> 'a -> unit
+val marshal_out_binary : out_handle -> segment:string -> out_channel * (unit -> unit)
+(** Low-level API. This function returns a channel and a closure. The channel
+    should only be written to, and once done, the closure should be invoked. *)
+
+end
 
 (** {6 Time stamps.} *)
 
diff --git a/vernac/library.ml b/vernac/library.ml
index 01f5101764..9a5d6fedcb 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
+  System.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 -> System.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 -> System.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 = System.ObjFile.get_segment ch ~segment in
+  let digest = seg.System.ObjFile.hash in
+  { del_file = f; del_digest = digest; del_off = seg.System.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 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 = System.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 = System.ObjFile.marshal_in_segment ch ~segment:"universes" in
+  let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch ~segment:"opaques" in
+  System.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 = System.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), _ = System.ObjFile.marshal_in_segment ch ~segment:"summary" in
+  let (s1 : seg_lib), _ = System.ObjFile.marshal_in_segment ch ~segment:"library" in
+  let (s2 : seg_univ option), _ = System.ObjFile.marshal_in_segment ch ~segment:"universes" in
+  let tasks, _ = System.ObjFile.marshal_in_segment ch ~segment:"tasks" in
+  let (s4 : seg_proofs), _ = System.ObjFile.marshal_in_segment ch ~segment:"opaques" in
+  System.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
+    System.ObjFile.marshal_out_segment ch ~segment:"summary" (sum    : seg_sum);
+    System.ObjFile.marshal_out_segment ch ~segment:"library" (lib    : seg_lib);
+    System.ObjFile.marshal_out_segment ch ~segment:"universes" (univs  : seg_univ option);
+    System.ObjFile.marshal_out_segment ch ~segment:"tasks" (tasks  : 'tasks option);
+    System.ObjFile.marshal_out_segment ch ~segment:"opaques" (proofs : seg_proofs);
+    System.ObjFile.close_out ch
   with reraise ->
     let reraise = Exninfo.capture reraise in
-    close_out ch;
+    System.ObjFile.close_out ch;
     Feedback.msg_warning (str "Removed file " ++ str f);
     Sys.remove f;
     Exninfo.iraise reraise