diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 23 | ||||
| -rw-r--r-- | library/lib.ml | 9 | ||||
| -rw-r--r-- | library/lib.mli | 5 | ||||
| -rw-r--r-- | library/library.ml | 187 | ||||
| -rw-r--r-- | library/library.mli | 15 |
5 files changed, 182 insertions, 57 deletions
diff --git a/library/declare.ml b/library/declare.ml index 3bd4cdd3f..477e96bd8 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -117,7 +117,13 @@ let open_constant i ((sp,kn), obj) = if obj.cst_locl then () else let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Exactly i) sp (ConstRef con) + Nametab.push (Nametab.Exactly i) sp (ConstRef con); + match (Global.lookup_constant con).const_body with + | (Def _ | Undef _) -> () + | OpaqueDef lc -> + match Lazyconstr.get_opaque_future_constraints lc with + | Some f when Future.is_val f -> Global.add_constraints (Future.force f) + | _ -> () let exists_name id = variable_exists id || Global.exists_objlabel (Label.of_id id) @@ -144,12 +150,12 @@ let discharged_hyps kn sechyps = let discharge_constant ((sp, kn), obj) = let con = constant_of_kn kn in - let cb = Global.lookup_constant con in - let repl = replacement_context () in - let sechyps = section_segment_of_constant con in - let recipe = { d_from=cb; d_modlist=repl; d_abstract=named_of_variable_context sechyps } in - let new_hyps = (discharged_hyps kn sechyps) @ obj.cst_hyps in - let new_decl = GlobalRecipe recipe in + let from = Global.lookup_constant con in + let modlist = replacement_context () in + let hyps = section_segment_of_constant con in + let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in + let abstract = named_of_variable_context hyps in + let new_decl = GlobalRecipe{ from; info = { Lazyconstr.modlist; abstract }} in Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) @@ -192,8 +198,7 @@ let declare_sideff se = let pt_opaque_of cb = match cb with | { const_body = Def sc } -> Lazyconstr.force sc, false - | { const_body = OpaqueDef fc } -> - Lazyconstr.force_opaque (Future.force fc), true + | { const_body = OpaqueDef fc } -> Lazyconstr.force_opaque fc, true | { const_body = Undef _ } -> anomaly(str"Undefined side effect") in let ty_of cb = diff --git a/library/lib.ml b/library/lib.ml index eef8171cc..ee89bb997 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -385,7 +385,7 @@ type abstr_list = variable_context Names.Cmap.t * variable_context Names.Mindmap let sectab = Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind) list * - Cooking.work_list * abstr_list) list) + Lazyconstr.work_list * abstr_list) list) ~name:"section-context" let add_section () = @@ -455,6 +455,13 @@ let section_instance = function let is_in_section ref = try ignore (section_instance ref); true with Not_found -> false +let full_replacement_context () = List.map pi2 !sectab +let full_section_segment_of_constant con = + List.map (fun (vars,_,(x,_)) -> fun hyps -> + named_of_variable_context + (try Names.Cmap.find con x + with Not_found -> extract_hyps (vars, hyps))) !sectab + (*************) (* Sections. *) diff --git a/library/lib.mli b/library/lib.mli index fa3bd3f48..787dc969e 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -186,4 +186,9 @@ val discharge_con : Names.constant -> Names.constant val discharge_global : Globnames.global_reference -> Globnames.global_reference val discharge_inductive : Names.inductive -> Names.inductive +(* discharging a constant in one go *) +val full_replacement_context : unit -> Lazyconstr.work_list list +val full_section_segment_of_constant : + Names.constant -> (Context.named_context -> Context.named_context) list + diff --git a/library/library.ml b/library/library.ml index 1088bcb16..c40f9d204 100644 --- a/library/library.ml +++ b/library/library.ml @@ -299,12 +299,10 @@ exception Faulty (** Fetching a table of opaque terms at position [pos] in file [f], expecting to find first a copy of [digest]. *) -let fetch_opaque_table dp (f,pos,digest) = - if !Flags.load_proofs == Flags.Dont then - error "Not accessing an opaque term due to option -dont-load-proofs."; +let fetch_table what dp (f,pos,digest) = let dir_path = Names.DirPath.to_string dp in try - Pp.msg_info (Pp.str "Fetching opaque terms from disk for " ++ str dir_path); + msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); let ch = System.with_magic_number_check raw_intern_library f in let () = seek_in ch pos in if not (String.equal (System.digest_in f ch) digest) then raise Faulty; @@ -316,64 +314,129 @@ let fetch_opaque_table dp (f,pos,digest) = table with e when Errors.noncritical e -> error - ("The file "^f^" (bound to " ^ dir_path ^ ") is inaccessible or corrupted,\n" - ^ "cannot load some opaque constant bodies in it.\n") + ("The file "^f^" (bound to " ^ dir_path ^ + ") is inaccessible or corrupted,\n" ^ + "cannot load some "^what^" in it.\n") (** Delayed / available tables of opaque terms *) -type opaque_table_status = +type 'a table_status = | ToFetch of string * int * Digest.t - | Fetched of Term.constr array + | Fetched of 'a Future.computation array -let opaque_tables = ref (LibraryMap.empty : opaque_table_status LibraryMap.t) +let opaque_tables = + ref (LibraryMap.empty : (Term.constr table_status) LibraryMap.t) +let univ_tables = + ref (LibraryMap.empty : (Univ.constraints table_status) LibraryMap.t) let add_opaque_table dp st = opaque_tables := LibraryMap.add dp st !opaque_tables +let add_univ_table dp st = + univ_tables := LibraryMap.add dp st !univ_tables -let access_opaque_table dp i = - let t = match LibraryMap.find dp !opaque_tables with +let access_table fetch_table add_table tables dp i = + let t = match LibraryMap.find dp tables with | Fetched t -> t | ToFetch (f,pos,digest) -> - let t = fetch_opaque_table dp (f,pos,digest) in - add_opaque_table dp (Fetched t); + let t = fetch_table dp (f,pos,digest) in + add_table dp (Fetched t); t in assert (i < Array.length t); t.(i) +let access_opaque_table dp i = + if !Flags.load_proofs == Flags.Dont then + error "Not accessing an opaque term due to option -dont-load-proofs."; + access_table + (fetch_table "opaque proofs") + add_opaque_table !opaque_tables dp i +let access_univ_table dp i = + access_table + (fetch_table "universe constraints of opaque proofs") + add_univ_table !univ_tables dp i + (** Table of opaque terms from the library currently being compiled *) module OpaqueTables = struct - let a_constr = Term.mkRel 1 + let a_constr = Future.from_val (Term.mkRel 1) + let a_univ = Future.from_val Univ.empty_constraint + let a_discharge : Lazyconstr.cooking_info list = [] - let local_table = ref (Array.make 100 a_constr) + let local_opaque_table = ref (Array.make 100 a_constr) + let local_univ_table = ref (Array.make 100 a_univ) + let local_discharge_table = ref (Array.make 100 a_discharge) let local_index = ref 0 - let get dp i = + module FMap = Map.Make(Future.UUID) + let f2t = ref FMap.empty + + let get_opaque_nolib _ i = (!local_opaque_table).(i) + + let get_opaque dp i = if DirPath.equal dp (Lib.library_dp ()) - then (!local_table).(i) + then (!local_opaque_table).(i) else access_opaque_table dp i + + let join_local_opaque dp i = + if DirPath.equal dp (Lib.library_dp ()) then + Future.sink (!local_opaque_table).(i) - let store c = + let join_local_univ dp i = + if DirPath.equal dp (Lib.library_dp ()) then + Future.sink (!local_univ_table).(i) + + let get_univ_nolib _ i = Some (!local_univ_table).(i) + + let get_univ dp i = + if DirPath.equal dp (Lib.library_dp ()) + then Some (!local_univ_table).(i) + else try Some (access_univ_table dp i) with Not_found -> None + + let store (d,cu) = let n = !local_index in incr local_index; - if Int.equal n (Array.length !local_table) then begin + if Int.equal n (Array.length !local_opaque_table) then begin let t = Array.make (2*n) a_constr in - Array.blit !local_table 0 t 0 n; - local_table := t + Array.blit !local_opaque_table 0 t 0 n; + local_opaque_table := t; + let t = Array.make (2*n) a_univ in + Array.blit !local_univ_table 0 t 0 n; + local_univ_table := t; + let t = Array.make (2*n) a_discharge in + Array.blit !local_discharge_table 0 t 0 n; + local_discharge_table := t end; - (!local_table).(n) <- c; + let c, u = Future.split2 ~greedy:true cu in + if Future.is_val u then ignore(Future.join u); + if Future.is_val c then ignore(Future.join c); + (!local_opaque_table).(n) <- c; + (!local_univ_table).(n) <- u; + (!local_discharge_table).(n) <- d; + f2t := FMap.add (Future.uuid cu) n !f2t; Some (Lib.library_dp (), n) - let dump () = Array.sub !local_table 0 !local_index + let dump () = + Array.sub !local_opaque_table 0 !local_index, + Array.sub !local_univ_table 0 !local_index, + Array.sub !local_discharge_table 0 !local_index, + FMap.bindings !f2t end -let _ = Lazyconstr.set_indirect_opaque_accessor OpaqueTables.get +let _ = Lazyconstr.set_indirect_opaque_accessor OpaqueTables.get_opaque +let _ = Lazyconstr.set_indirect_univ_accessor OpaqueTables.get_univ +let _ = Lazyconstr.set_join_indirect_local_opaque OpaqueTables.join_local_opaque +let _ = Lazyconstr.set_join_indirect_local_univ OpaqueTables.join_local_univ (************************************************************************) (* Internalise libraries *) +type seg_lib = library_disk +type seg_univ = Univ.constraints Future.computation array +type seg_discharge = Lazyconstr.cooking_info list array +type seg_proofs = Term.constr Future.computation array + let mk_library md digest = { library_name = md.md_name; @@ -386,7 +449,10 @@ let mk_library md digest = let intern_from_file f = let ch = System.with_magic_number_check raw_intern_library f in - let lmd, _, digest_lmd = System.marshal_in_segment f ch 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 _ = System.skip_in_segment f ch in let pos, digest = System.skip_in_segment f ch in register_library_filename lmd.md_name f; add_opaque_table lmd.md_name (ToFetch (f,pos,digest)); @@ -394,18 +460,6 @@ let intern_from_file f = close_in ch; library -let load_library_todo f = - let paths = Loadpath.get_paths () in - let _, longf = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in - let f = longf^"i" in - let ch = System.with_magic_number_check raw_intern_library f in - let _ = System.skip_in_segment f ch in - let tasks, _, _ = System.marshal_in_segment f ch in - match tasks with - | Some a -> a, longf - | None -> errorlabstrm "load_library_todo" (str"not a .vi file") - let rec intern_library needed (dir, f) = (* Look if in the current logical environment *) try find_library dir, needed @@ -604,10 +658,27 @@ let start_library f = let id = Id.of_string (Filename.basename f) in check_coq_overwriting ldir0 id; let ldir = add_dirpath_suffix ldir0 id in - Lazyconstr.set_indirect_opaque_creator OpaqueTables.store; + Lazyconstr.set_indirect_creator OpaqueTables.store; Declaremods.start_library ldir; ldir,longf +let load_library_todo f = + let paths = Loadpath.get_paths () in + let _, longf = + System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in + let f = longf^"i" in + let ch = System.with_magic_number_check raw_intern_library f 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 + let tasks, _, _ = System.marshal_in_segment f ch in + let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in + close_in ch; + 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"); + 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. *) @@ -635,10 +706,25 @@ let error_recursively_dependent_library dir = writing the content and computing the checksum... *) let save_library_to ?todo dir f = - let f = if todo = None then f ^ "o" else f ^ "i" in - Lazyconstr.reset_indirect_opaque_creator (); + let f, todo, utab, dtab = + match todo with + | None -> + assert(!Flags.compilation_mode = Flags.BuildVo); + 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 + Lazyconstr.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 + * accessors use Lib. Hence *) + Lazyconstr.set_indirect_opaque_accessor OpaqueTables.get_opaque_nolib; + Lazyconstr.set_indirect_univ_accessor OpaqueTables.get_univ_nolib; let cenv, seg, ast = Declaremods.end_library dir in - let table = OpaqueTables.dump () in + let opaque_table, univ_table, disch_table, f2t_map = + OpaqueTables.dump () in + assert(!Flags.compilation_mode = Flags.BuildVi || + Array.for_all Future.is_val opaque_table); let md = { md_name = dir; md_compiled = cenv; @@ -651,9 +737,11 @@ let save_library_to ?todo dir f = let (f',ch) = raw_extern_library f in try (* Writing vo payload *) - System.marshal_out_segment f' ch md; (* env + objs *) - System.marshal_out_segment f' ch todo; (* STM tasks *) - System.marshal_out_segment f' ch table; (* opaques *) + System.marshal_out_segment f' ch (md : seg_lib); + System.marshal_out_segment f' ch (utab univ_table : seg_univ option); + System.marshal_out_segment f' ch (dtab disch_table : seg_discharge option); + System.marshal_out_segment f' ch (todo f2t_map : 'tasks option); + System.marshal_out_segment f' ch (opaque_table : seg_proofs); close_out ch; (* Writing native code files *) if not !Flags.no_native_compiler then @@ -662,7 +750,7 @@ let save_library_to ?todo dir f = let lp = List.map map_path lp in let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in if not (Int.equal (Nativelibrary.compile_library dir ast lp fn) 0) then - msg_error (str "Could not compile the library to native code. Skipping.") + msg_error (str"Could not compile the library to native code. Skipping.") with reraise -> let reraise = Errors.push reraise in let () = msg_warning (str ("Removed file "^f')) in @@ -670,6 +758,15 @@ let save_library_to ?todo dir f = let () = Sys.remove f' in raise reraise +let save_library_raw f lib univs proofs = + let (f',ch) = raw_extern_library (f^"o") in + 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); + System.marshal_out_segment f' ch (None : 'tasks option); + System.marshal_out_segment f' ch (proofs : seg_proofs); + close_out ch + (************************************************************************) (*s Display the memory use of a library. *) diff --git a/library/library.mli b/library/library.mli index 647138483..ec39059e9 100644 --- a/library/library.mli +++ b/library/library.mli @@ -29,6 +29,13 @@ val require_library_from_file : Id.t option -> CUnix.physical_path -> bool option -> unit (** {6 ... } *) + +(** Segments of a library *) +type seg_lib +type seg_univ = Univ.constraints Future.computation array +type seg_discharge = Lazyconstr.cooking_info list array +type seg_proofs = Term.constr Future.computation array + (** Open a module (or a library); if the boolean is true then it's also an export otherwise just a simple import *) val import_module : bool -> qualid located -> unit @@ -37,8 +44,12 @@ val import_module : bool -> qualid located -> unit val start_library : string -> DirPath.t * string (** {6 End the compilation of a library and save it to a ".vo" file } *) -val save_library_to : ?todo:'a -> DirPath.t -> string -> unit -val load_library_todo : string -> 'a * string +val save_library_to : ?todo:((Future.UUID.t * int) list -> 'tasks) -> + DirPath.t -> string -> 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 (** {6 Interrogate the status of libraries } *) |