diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/library.ml | 54 | ||||
| -rw-r--r-- | library/library.mli | 5 |
2 files changed, 36 insertions, 23 deletions
diff --git a/library/library.ml b/library/library.ml index 0296d7b90..19c8c92f8 100644 --- a/library/library.ml +++ b/library/library.ml @@ -76,11 +76,15 @@ open Delayed type compilation_unit_name = DirPath.t type library_disk = { - md_name : compilation_unit_name; md_compiled : Safe_typing.compiled_library; md_objects : Declaremods.library_objects; +} + +type summary_disk = { + md_name : compilation_unit_name; + md_imports : compilation_unit_name array; md_deps : (compilation_unit_name * Safe_typing.vodigest) array; - md_imports : compilation_unit_name array } +} (*s Modules loaded in memory contain the following informations. They are kept in the global table [libraries_table]. *) @@ -406,19 +410,20 @@ let () = (************************************************************************) (* Internalise libraries *) +type seg_sum = summary_disk type seg_lib = library_disk type seg_univ = (* true = vivo, false = vi *) Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool type seg_discharge = Opaqueproof.cooking_info list array type seg_proofs = Term.constr Future.computation array -let mk_library md digests univs = +let mk_library sd md digests univs = { - library_name = md.md_name; + library_name = sd.md_name; library_compiled = md.md_compiled; library_objects = md.md_objects; - library_deps = md.md_deps; - library_imports = md.md_imports; + library_deps = sd.md_deps; + library_imports = sd.md_imports; library_digests = digests; library_extra_univs = univs; } @@ -431,23 +436,24 @@ let mk_summary m = { let intern_from_file f = let ch = System.with_magic_number_check raw_intern_library f in - let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment f ch in + let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in + let (lmd : seg_lib), _, digest_lmd = System.marshal_in_segment 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 close_in ch; - register_library_filename lmd.md_name f; - add_opaque_table lmd.md_name (ToFetch del_opaque); + 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 lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty + | None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty | Some (utab,uall,true) -> - add_univ_table lmd.md_name (Fetched utab); - mk_library lmd (Dvivo (digest_lmd,digest_u)) uall + add_univ_table lsd.md_name (Fetched utab); + mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall | Some (utab,_,false) -> - add_univ_table lmd.md_name (Fetched utab); - mk_library lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty + add_univ_table lsd.md_name (Fetched utab); + mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty module DPMap = Map.Make(DirPath) @@ -510,7 +516,7 @@ let rec_intern_by_filename_only id f = let native_name_from_filename f = let ch = System.with_magic_number_check raw_intern_library f in - let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment f ch in + let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in Nativecode.mod_uid_of_dirpath lmd.md_name let rec_intern_library_from_file idopt f = @@ -695,6 +701,7 @@ let load_library_todo f = System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in let f = longf^"io" in let ch = System.with_magic_number_check 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 (s3 : seg_discharge option), _, _ = System.marshal_in_segment f ch in @@ -705,7 +712,7 @@ let load_library_todo f = if s2 = None then errorlabstrm "restart" (str"not a .vio file"); if s3 = None then errorlabstrm "restart" (str"not a .vio file"); if pi3 (Option.get s2) then errorlabstrm "restart" (str"not a .vio file"); - longf, s1, Option.get s2, Option.get s3, Option.get tasks, s5 + longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5 (************************************************************************) (*s [save_library dir] ends library [dir] and save it to the disk. *) @@ -769,18 +776,22 @@ let save_library_to ?todo dir f otab = if not(is_done_or_todo i x) then Errors.errorlabstrm "library" Pp.(str"Proof object "++int i++str" is not checked nor to be checked")) opaque_table; - let md = { + let sd = { md_name = dir; + md_deps = Array.of_list (current_deps ()); + md_imports = Array.of_list (current_reexports ()); + } in + let md = { md_compiled = cenv; md_objects = seg; - md_deps = Array.of_list (current_deps ()); - md_imports = Array.of_list (current_reexports ()) } in - if Array.exists (fun (d,_) -> DirPath.equal d dir) md.md_deps then + } in + if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then error_recursively_dependent_library dir; (* Open the vo file and write the magic number *) let (f',ch) = raw_extern_library f in try (* Writing vo payload *) + System.marshal_out_segment f' ch (sd : seg_sum); System.marshal_out_segment f' ch (md : seg_lib); System.marshal_out_segment f' ch (utab : seg_univ option); System.marshal_out_segment f' ch (dtab : seg_discharge option); @@ -799,8 +810,9 @@ let save_library_to ?todo dir f otab = let () = Sys.remove f' in iraise reraise -let save_library_raw f lib univs proofs = +let save_library_raw f sum lib univs proofs = let (f',ch) = raw_extern_library (f^"o") in + System.marshal_out_segment f' ch (sum : seg_sum); System.marshal_out_segment f' ch (lib : seg_lib); System.marshal_out_segment f' ch (Some univs : seg_univ option); System.marshal_out_segment f' ch (None : seg_discharge option); diff --git a/library/library.mli b/library/library.mli index 350670680..967a54e4c 100644 --- a/library/library.mli +++ b/library/library.mli @@ -28,6 +28,7 @@ val require_library_from_file : (** {6 ... } *) (** Segments of a library *) +type seg_sum type seg_lib type seg_univ = (* cst, all_cst, finished? *) Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool @@ -47,8 +48,8 @@ val save_library_to : DirPath.t -> string -> Opaqueproof.opaquetab -> unit val load_library_todo : - string -> string * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs -val save_library_raw : string -> seg_lib -> seg_univ -> seg_proofs -> unit + string -> string * seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs +val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit (** {6 Interrogate the status of libraries } *) |