diff options
| author | Pierre-Marie Pédrot | 2020-04-27 17:15:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-27 17:28:29 +0200 |
| commit | 6334ab72d55cb93a877933bd3f56a90d859d518d (patch) | |
| tree | 13125ecba082ddd432420dc6ef51ac265333c4ba | |
| parent | e0d7b05789d7c6d341d3001c227d99a278743fd1 (diff) | |
Do not delay the loading of the library_disk field when requiring libraries.
The reason for which the code was written this way is probably historical. In
the current implementation, we read the marshalled data exactly once by library,
thus there is no gain from delaying.
| -rw-r--r-- | vernac/library.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/library.ml b/vernac/library.ml index 35b2a18871..afadbd704d 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -92,7 +92,7 @@ type summary_disk = { type library_t = { library_name : compilation_unit_name; - library_data : library_disk delayed; + library_data : library_disk; library_deps : (compilation_unit_name * Safe_typing.vodigest) array; library_digests : Safe_typing.vodigest; library_extra_univs : Univ.ContextSet.t; @@ -243,7 +243,7 @@ let mk_summary m = { let intern_from_file f = let ch = raw_intern_library f 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 ((lmd : seg_lib), digest_lmd) = ObjFile.marshal_in_segment ch ~segment:"library" in let (univs : seg_univ option), digest_u = ObjFile.marshal_in_segment ch ~segment:"universes" in let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch ~segment:"opaques" in ObjFile.close_in ch; @@ -317,7 +317,7 @@ let native_name_from_filename f = *) let register_library m = - let l = fetch_delayed m.library_data in + let l = m.library_data in Declaremods.register_library m.library_name l.md_compiled |