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. --- lib/system.ml | 259 +++++++++++++++++++++++++++++++++++++++++++++++++-------- lib/system.mli | 36 ++++++-- 2 files changed, 254 insertions(+), 41 deletions(-) (limited to 'lib') 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.} *) -- 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. --- lib/lib.mllib | 1 + lib/objFile.ml | 229 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/objFile.mli | 34 +++++++++ lib/system.ml | 214 ---------------------------------------------------- lib/system.mli | 30 -------- 5 files changed, 264 insertions(+), 244 deletions(-) create mode 100644 lib/objFile.ml create mode 100644 lib/objFile.mli (limited to 'lib') 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 -- 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(-) (limited to 'lib') 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. --- lib/objFile.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib') 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 -- cgit v1.2.3