From 75e394770b534994830f6d80e649734275de5006 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 29 Mar 2020 18:02:46 +0200 Subject: Implement a name-based representation for vo files. See CEP#44 for futher details. --- checker/check.ml | 62 ++++++------ checker/votour.ml | 92 +++++++++++++----- config/coq_config.mli | 2 +- configure.ml | 3 +- lib/system.ml | 259 +++++++++++++++++++++++++++++++++++++++++++------- lib/system.mli | 36 +++++-- vernac/library.ml | 63 ++++++------ 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, enters the -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 -- cgit v1.2.3 From 3dc9ec53041b4b34a601c2d454d0e47005561b30 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 15 Apr 2020 19:09:34 +0200 Subject: Move the ObjFile module to its own file. --- checker/check.ml | 20 ++--- lib/lib.mllib | 1 + lib/objFile.ml | 229 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/objFile.mli | 34 ++++++++ lib/system.ml | 214 -------------------------------------------------- lib/system.mli | 30 ------- vernac/library.ml | 46 +++++------ 7 files changed, 297 insertions(+), 277 deletions(-) create mode 100644 lib/objFile.ml create mode 100644 lib/objFile.mli diff --git a/checker/check.ml b/checker/check.ml index 8881e05ab6..8554c5a677 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.ObjFile.open_in ~file:f + ObjFile.open_in ~file:f (************************************************************************) (* Internalise libraries *) @@ -295,13 +295,13 @@ type intern_mode = Rec | Root | Dep (* Rec = standard, Root = -norec, Dep = depe let depgraph = ref LibraryMap.empty let marshal_in_segment ~validate ~value ~segment f ch = - let () = LargeFile.seek_in ch segment.System.ObjFile.pos in + let () = LargeFile.seek_in ch segment.ObjFile.pos in if validate then let v = try let v = Analyze.parse_channel ch in let digest = Digest.input ch in - let () = if not (String.equal digest segment.System.ObjFile.hash) then raise Exit in + let () = if not (String.equal digest segment.ObjFile.hash) then raise Exit in v with _ -> user_err (str "Corrupted file " ++ quote (str f)) @@ -326,12 +326,12 @@ let intern_from_file ~intern_mode (dir, f) = try (* First pass to read the metadata of the file *) let ch = System.with_magic_number_check raw_intern_library f 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 + let seg_sd = ObjFile.get_segment ch ~segment:"summary" in + let seg_md = ObjFile.get_segment ch ~segment:"library" in + let seg_univs = ObjFile.get_segment ch ~segment:"universes" in + let seg_tasks = ObjFile.get_segment ch ~segment:"tasks" in + let seg_opaque = ObjFile.get_segment ch ~segment:"opaques" in + let () = ObjFile.close_in ch in (* Actually read the data *) let ch = open_in f in @@ -360,7 +360,7 @@ let intern_from_file ~intern_mode (dir, f) = end; Flags.if_verbose chk_pp (str" done]" ++ fnl ()); let digest = - let open System.ObjFile in + let open 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 diff --git a/lib/lib.mllib b/lib/lib.mllib index 2db59712b9..4e08e87084 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -14,6 +14,7 @@ CWarnings AcyclicGraph Rtree System +ObjFile Explore CProfile Future diff --git a/lib/objFile.ml b/lib/objFile.ml new file mode 100644 index 0000000000..190b1833bd --- /dev/null +++ b/lib/objFile.ml @@ -0,0 +1,229 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* + CErrors.user_err ~hdr:"System.open" (str "Can't open " ++ str name) + +(* + +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 diff --git a/lib/objFile.mli b/lib/objFile.mli new file mode 100644 index 0000000000..36db7f4208 --- /dev/null +++ b/lib/objFile.mli @@ -0,0 +1,34 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* 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. *) diff --git a/lib/system.ml b/lib/system.ml index 32e5a53821..4e98651d6e 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -240,220 +240,6 @@ let with_magic_number_check f a = 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 7e02b76203..4a8c35b6ea 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -88,36 +88,6 @@ val with_magic_number_check : ('a -> 'b) -> 'a -> 'b val marshal_out : out_channel -> 'a -> unit val marshal_in : string -> in_channel -> 'a -module ObjFile : -sig - -val magic_number : int32 - -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.} *) type time diff --git a/vernac/library.ml b/vernac/library.ml index 9a5d6fedcb..8a10891dfb 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.ObjFile.open_out ~file:f + ObjFile.open_out ~file:f let raw_intern_library f = System.with_magic_number_check - (fun file -> System.ObjFile.open_in ~file) 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 -> System.ObjFile.in_handle -> segment:string -> 'a delayed * Digest.t +val in_delayed : string -> ObjFile.in_handle -> segment:string -> 'a delayed * Digest.t val fetch_delayed : 'a delayed -> 'a end = @@ -48,9 +48,9 @@ type 'a delayed = { } 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 + 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]. *) @@ -242,11 +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.ObjFile.marshal_in_segment ch ~segment:"summary" in + 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 = System.ObjFile.marshal_in_segment ch ~segment:"universes" 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 - System.ObjFile.close_in ch; + 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 @@ -296,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), digest_lmd = System.ObjFile.marshal_in_segment ch ~segment:"summary" in + let (lmd : seg_sum), digest_lmd = ObjFile.marshal_in_segment ch ~segment:"summary" in Nativecode.mod_uid_of_dirpath lmd.md_name (**********************************************************************) @@ -391,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.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; + 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"); @@ -432,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.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 + 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 - System.ObjFile.close_out ch; + ObjFile.close_out ch; Feedback.msg_warning (str "Removed file " ++ str f); Sys.remove f; Exninfo.iraise reraise -- cgit v1.2.3 From e16aab42641f0b79827c4598bf065b1607a08c43 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 15 Apr 2020 19:16:16 +0200 Subject: Tweak a comment on the low-level objfile API. --- lib/objFile.mli | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/lib/objFile.mli b/lib/objFile.mli index 36db7f4208..b15b04ee54 100644 --- a/lib/objFile.mli +++ b/lib/objFile.mli @@ -30,5 +30,8 @@ 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. *) +(** [marshal_out_binary oh segment] is a low level, stateful, API returning + [oc, stop]. Once called no other API can be used on the same [oh] and only + [Stdlib.output_*] APIs should be used on [oc]. [stop ()] must be invoked in + order to signal that all data was written to [oc] (which should not be used + afterwards). Only after calling [stop] the other API can be used on [oh]. *) -- cgit v1.2.3 From 0520fa60a855b4c5f7b9d9298607cfd9e346c0e3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 26 Apr 2020 14:25:22 +0200 Subject: Open object files in binary mode. --- checker/check.ml | 2 +- lib/objFile.ml | 4 ++-- vernac/library.ml | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/checker/check.ml b/checker/check.ml index 8554c5a677..31bfebc3d5 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -333,7 +333,7 @@ let intern_from_file ~intern_mode (dir, f) = let seg_opaque = ObjFile.get_segment ch ~segment:"opaques" in let () = ObjFile.close_in ch in (* Actually read the data *) - let ch = open_in f in + let ch = open_in_bin 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 diff --git a/lib/objFile.ml b/lib/objFile.ml index 190b1833bd..96db51a010 100644 --- a/lib/objFile.ml +++ b/lib/objFile.ml @@ -143,7 +143,7 @@ let marshal_out_segment h ~segment v = 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 in_ch = open_in_bin 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 @@ -163,7 +163,7 @@ let marshal_out_binary h ~segment = 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 in_ch = open_in_bin 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 diff --git a/vernac/library.ml b/vernac/library.ml index 8a10891dfb..35b2a18871 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -58,7 +58,7 @@ let in_delayed f ch ~segment = let fetch_delayed del = let { del_digest = digest; del_file = f; del_off = pos; } = del in try - let ch = open_in f 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 -- cgit v1.2.3