diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 4 | ||||
| -rw-r--r-- | library/declaremods.mli | 3 | ||||
| -rw-r--r-- | library/global.ml | 2 | ||||
| -rw-r--r-- | library/global.mli | 3 | ||||
| -rw-r--r-- | library/library.ml | 49 | ||||
| -rw-r--r-- | library/library.mli | 3 |
6 files changed, 40 insertions, 24 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index c60e008d1c..2b917587c1 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -849,7 +849,7 @@ type library_values = Nativecode.symbol array let library_values = Summary.ref (Dirmap.empty : library_values Dirmap.t) ~name:"LIBVALUES" -let register_library dir cenv (objs:library_objects) digest = +let register_library dir cenv (objs:library_objects) digest univ = let mp = MPfile dir in let () = try @@ -857,7 +857,7 @@ let register_library dir cenv (objs:library_objects) digest = ignore(Global.lookup_module mp); with Not_found -> (* If not, let's do it now ... *) - let mp', values = Global.import cenv digest in + let mp', values = Global.import cenv univ digest in if not (ModPath.equal mp mp') then anomaly (Pp.str "Unexpected disk module name"); library_values := Dirmap.add dir values !library_values diff --git a/library/declaremods.mli b/library/declaremods.mli index 89bcccef34..5ff471e693 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -72,7 +72,8 @@ type library_objects val register_library : library_name -> - Safe_typing.compiled_library -> library_objects -> Digest.t -> unit + Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest -> + Univ.constraints -> unit val get_library_symbols_tbl : library_name -> Nativecode.symbol array diff --git a/library/global.ml b/library/global.ml index 9515ff1a8f..f75c8e5927 100644 --- a/library/global.ml +++ b/library/global.ml @@ -129,7 +129,7 @@ let mind_of_delta_kn kn = let start_library dir = globalize (Safe_typing.start_library dir) let export s = Safe_typing.export !Flags.compilation_mode (safe_env ()) s -let import cenv digest = globalize (Safe_typing.import cenv digest) +let import c u d = globalize (Safe_typing.import c u d) (** Function to get an environment from the constants part of the global diff --git a/library/global.mli b/library/global.mli index 856956a17c..e11e1c0174 100644 --- a/library/global.mli +++ b/library/global.mli @@ -85,7 +85,8 @@ val mind_of_delta_kn : kernel_name -> mutual_inductive val start_library : DirPath.t -> module_path val export : DirPath.t -> module_path * Safe_typing.compiled_library * Safe_typing.native_library -val import : Safe_typing.compiled_library -> Digest.t -> +val import : + Safe_typing.compiled_library -> Univ.constraints -> Safe_typing.vodigest -> module_path * Nativecode.symbol array (** {6 Misc } *) diff --git a/library/library.ml b/library/library.ml index a1760cdf16..b75329a22c 100644 --- a/library/library.ml +++ b/library/library.ml @@ -26,7 +26,7 @@ type library_disk = { md_name : compilation_unit_name; md_compiled : Safe_typing.compiled_library; md_objects : Declaremods.library_objects; - md_deps : (compilation_unit_name * Digest.t) 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 @@ -36,9 +36,11 @@ type library_t = { library_name : compilation_unit_name; library_compiled : Safe_typing.compiled_library; library_objects : Declaremods.library_objects; - library_deps : (compilation_unit_name * Digest.t) array; + library_deps : (compilation_unit_name * Safe_typing.vodigest) array; library_imports : compilation_unit_name array; - library_digest : Digest.t } + library_digests : Safe_typing.vodigest; + library_extra_univs : Univ.constraints; +} module LibraryOrdered = DirPath module LibraryMap = Map.Make(LibraryOrdered) @@ -441,32 +443,40 @@ let () = (* Internalise libraries *) type seg_lib = library_disk -type seg_univ = Univ.constraints Future.computation array +type seg_univ = (* true = vivo, false = vi *) + Univ.constraints Future.computation array * Univ.constraints * bool type seg_discharge = Opaqueproof.cooking_info list array type seg_proofs = Term.constr Future.computation array -let mk_library md digest = +let mk_library md digests univs = { library_name = md.md_name; library_compiled = md.md_compiled; library_objects = md.md_objects; library_deps = md.md_deps; library_imports = md.md_imports; - library_digest = digest + library_digests = digests; + library_extra_univs = univs; } 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 (univs : seg_univ option), _, _ = System.marshal_in_segment f ch in - Option.iter (fun univs -> add_univ_table lmd.md_name (Fetched univs)) univs; + let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in let _ = System.skip_in_segment f ch in let pos, digest = System.skip_in_segment f ch in + close_in ch; register_library_filename lmd.md_name f; add_opaque_table lmd.md_name (ToFetch (f,pos,digest)); - let library = mk_library lmd digest_lmd in - close_in ch; - library + let open Safe_typing in + match univs with + | None -> mk_library lmd (Dvo_or_vi digest_lmd) Univ.empty_constraint + | Some (utab,uall,true) -> + add_univ_table lmd.md_name (Fetched utab); + mk_library 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.empty_constraint let rec intern_library needed (dir, f) = (* Look if in the current logical environment *) @@ -489,10 +499,10 @@ and intern_library_deps needed dir m = and intern_mandatory_library caller needed (dir,d) = let m,needed = intern_library needed (try_locate_absolute_library dir) in - if not (String.equal d m.library_digest) then - errorlabstrm "" (strbrk ("Compiled library "^(DirPath.to_string caller)^ - ".vo makes inconsistent assumptions over library " - ^(DirPath.to_string dir))); + if not (Safe_typing.digest_match ~actual:m.library_digests ~required:d) then + errorlabstrm "" (strbrk ("Compiled library "^ DirPath.to_string caller ^ + ".vo makes inconsistent assumptions over library " ^ + DirPath.to_string dir)); needed let rec_intern_library needed mref = @@ -553,7 +563,8 @@ let register_library m = m.library_name m.library_compiled m.library_objects - m.library_digest; + m.library_digests + m.library_extra_univs; register_loaded_library m (* Follow the semantics of Anticipate object: @@ -686,13 +697,14 @@ let load_library_todo f = if tasks = None then errorlabstrm "restart" (str"not a .vi file"); if s2 = None then errorlabstrm "restart" (str"not a .vi file"); if s3 = None then errorlabstrm "restart" (str"not a .vi file"); + if pi3 (Option.get s2) then errorlabstrm "restart" (str"not a .vi file"); longf, s1, Option.get s2, Option.get s3, Option.get tasks, s5 (************************************************************************) (*s [save_library dir] ends library [dir] and save it to the disk. *) let current_deps () = - List.map (fun m -> (m.library_name, m.library_digest)) !libraries_loaded_list + List.map (fun m -> m.library_name, m.library_digests) !libraries_loaded_list let current_reexports () = List.map (fun m -> m.library_name) !libraries_exports_list @@ -722,7 +734,8 @@ let save_library_to ?todo dir f = f ^ "o", (fun _ -> None), (fun _ -> None), (fun _ -> None) | Some d -> assert(!Flags.compilation_mode = Flags.BuildVi); - f ^ "i", (fun x -> Some (d x)), (fun x -> Some x), (fun x -> Some x) in + f ^ "i", (fun x -> Some (d x)), + (fun x -> Some (x,Univ.empty_constraint,false)), (fun x -> Some x) in Opaqueproof.reset_indirect_creator (); (* HACK: end_library resets Lib and then joins the safe env. To join the * env one needs to access the futures stored in the tables. Standard diff --git a/library/library.mli b/library/library.mli index afcce7f6c0..16664d880e 100644 --- a/library/library.mli +++ b/library/library.mli @@ -30,7 +30,8 @@ val require_library_from_file : (** Segments of a library *) type seg_lib -type seg_univ = Univ.constraints Future.computation array +type seg_univ = (* cst, all_cst, finished? *) + Univ.constraints Future.computation array * Univ.constraints * bool type seg_discharge = Opaqueproof.cooking_info list array type seg_proofs = Term.constr Future.computation array |