From e6b0ab5079186b7dba643a04e6222a4260de96ff Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sun, 5 Jun 2016 12:41:16 +0200 Subject: Fix incorrect checking of library checksums. Since d09def34, only the summary of libraries was included in the checksum, not the actual content of the library. This quick fix performs the checking of the checksum immediately, even if the loading is delayed. --- library/library.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'library/library.ml') diff --git a/library/library.ml b/library/library.ml index ccda57c2c..e34d38d15 100644 --- a/library/library.ml +++ b/library/library.ml @@ -35,7 +35,7 @@ module Delayed : sig type 'a delayed -val in_delayed : string -> in_channel -> 'a delayed +val in_delayed : string -> in_channel -> 'a delayed * Digest.t val fetch_delayed : 'a delayed -> 'a end = @@ -50,7 +50,7 @@ type 'a delayed = { 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; } + ({ del_file = f; del_digest = digest; del_off = pos; }, digest) (** Fetching a table of opaque terms at position [pos] in file [f], expecting to find first a copy of [digest]. *) @@ -437,23 +437,23 @@ 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) = in_delayed 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 _ = System.skip_in_segment f ch in - let (del_opaque : seg_proofs delayed) = in_delayed f ch in + let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in close_in ch; register_library_filename lsd.md_name f; add_opaque_table lsd.md_name (ToFetch del_opaque); let open Safe_typing in match univs with - | None -> mk_library lsd lmd (Dvo_or_vi digest_lsd) Univ.ContextSet.empty + | None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty | Some (utab,uall,true) -> add_univ_table lsd.md_name (Fetched utab); - mk_library lsd lmd (Dvivo (digest_lsd,digest_u)) uall + mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall | Some (utab,_,false) -> add_univ_table lsd.md_name (Fetched utab); - mk_library lsd lmd (Dvo_or_vi digest_lsd) Univ.ContextSet.empty + mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty module DPMap = Map.Make(DirPath) -- cgit v1.2.3