aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check.ml24
-rw-r--r--checker/cic.mli10
-rw-r--r--checker/values.ml7
-rw-r--r--checker/votour.ml1
-rw-r--r--library/library.ml54
-rw-r--r--library/library.mli5
-rw-r--r--stm/vio_checking.ml4
-rw-r--r--toplevel/vernac.ml4
8 files changed, 66 insertions, 43 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 3e22c4b18..0a5b5eb88 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -291,12 +291,12 @@ let with_magic_number_check f a =
open Cic
-let mk_library md f table digest cst = {
- library_name = md.md_name;
+let mk_library sd md f table digest cst = {
+ library_name = sd.md_name;
library_filename = f;
library_compiled = md.md_compiled;
library_opaques = table;
- library_deps = md.md_deps;
+ library_deps = sd.md_deps;
library_digest = digest;
library_extra_univs = cst }
@@ -310,9 +310,10 @@ let depgraph = ref LibraryMap.empty
let intern_from_file (dir, f) =
Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush ();
- let (md,table,opaque_csts,digest) =
+ let (sd,md,table,opaque_csts,digest) =
try
let ch = with_magic_number_check raw_intern_library f in
+ let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in
let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in
let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in
let (discharging:'a option), _, _ = System.marshal_in_segment f ch in
@@ -325,9 +326,9 @@ let intern_from_file (dir, f) =
if not (String.equal (Digest.channel ch pos) checksum) then
errorlabstrm "intern_from_file" (str "Checksum mismatch");
let () = close_in ch in
- if dir <> md.md_name then
+ if dir <> sd.md_name then
errorlabstrm "intern_from_file"
- (name_clash_message dir md.md_name f);
+ (name_clash_message dir sd.md_name f);
if tasks <> None || discharging <> None then
errorlabstrm "intern_from_file"
(str "The file "++str f++str " contains unfinished tasks");
@@ -340,25 +341,26 @@ let intern_from_file (dir, f) =
Validate.validate !Flags.debug Values.v_univopaques opaque_csts;
end;
(* Verification of the unmarshalled values *)
+ Validate.validate !Flags.debug Values.v_libsum sd;
Validate.validate !Flags.debug Values.v_lib md;
Validate.validate !Flags.debug Values.v_opaques table;
Flags.if_verbose ppnl (str" done]"); pp_flush ();
let digest =
if opaque_csts <> None then Cic.Dviovo (digest,udg)
else (Cic.Dvo digest) in
- md,table,opaque_csts,digest
+ sd,md,table,opaque_csts,digest
with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in
- depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
- opaque_tables := LibraryMap.add md.md_name table !opaque_tables;
+ depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph;
+ opaque_tables := LibraryMap.add sd.md_name table !opaque_tables;
Option.iter (fun (opaque_csts,_,_) ->
opaque_univ_tables :=
- LibraryMap.add md.md_name opaque_csts !opaque_univ_tables)
+ LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables)
opaque_csts;
let extra_cst =
Option.default Univ.empty_constraint
(Option.map (fun (_,cs,_) ->
Univ.ContextSet.constraints cs) opaque_csts) in
- mk_library md f table digest extra_cst
+ mk_library sd md f table digest extra_cst
let get_deps (dir, f) =
try LibraryMap.find dir !depgraph
diff --git a/checker/cic.mli b/checker/cic.mli
index 90a0e9feb..e875e40f0 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -417,12 +417,16 @@ type compiled_library = {
type library_objects
-type library_disk = {
+type summary_disk = {
md_name : compilation_unit_name;
+ md_imports : compilation_unit_name array;
+ md_deps : library_deps;
+}
+
+type library_disk = {
md_compiled : compiled_library;
md_objects : library_objects;
- md_deps : library_deps;
- md_imports : compilation_unit_name array }
+}
type opaque_table = constr Future.computation array
type univ_table =
diff --git a/checker/values.ml b/checker/values.ml
index cf93466b0..b2d74821d 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 0a174243f8b06535c9eecbbe8d339fe1 checker/cic.mli
+MD5 f5fd749af797e08efee22122742bc740 checker/cic.mli
*)
@@ -350,8 +350,11 @@ let v_stm_seg = v_pair v_tasks v_counters
(** Toplevel structures in a vo (see Cic.mli) *)
+let v_libsum =
+ Tuple ("summary", [|v_dp;Array v_dp;v_deps|])
+
let v_lib =
- Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps;Array v_dp|])
+ Tuple ("library",[|v_compiled_lib;v_libraryobjs|])
let v_opaques = Array (v_computation v_constr)
let v_univopaques =
diff --git a/checker/votour.ml b/checker/votour.ml
index 01965bb4b..bb8e06702 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -249,6 +249,7 @@ let visit_vo f =
Printf.printf
"At prompt, <n> enters the <n>-th child, u goes up 1 level, x exits\n\n%!";
let segments = [|
+ make_seg "summary" Values.v_libsum;
make_seg "library" Values.v_lib;
make_seg "univ constraints of opaque proofs" Values.v_univopaques;
make_seg "discharging info" (Opt Any);
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 } *)
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index b20722211..4df9603dc 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -10,7 +10,7 @@ open Util
let check_vio (ts,f) =
Dumpglob.noglob ();
- let long_f_dot_v, _, _, _, tasks, _ = Library.load_library_todo f in
+ let long_f_dot_v, _, _, _, _, tasks, _ = Library.load_library_todo f in
Stm.set_compilation_hints long_f_dot_v;
List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
@@ -30,7 +30,7 @@ let schedule_vio_checking j fs =
let f =
if Filename.check_suffix f ".vio" then Filename.chop_extension f
else f in
- let long_f_dot_v, _,_,_, tasks, _ = Library.load_library_todo f in
+ let long_f_dot_v, _,_,_,_, tasks, _ = Library.load_library_todo f in
Stm.set_compilation_hints long_f_dot_v;
let infos = Stm.info_tasks tasks in
let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7d84ecf6c..bc8aa2fff 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -344,10 +344,10 @@ let compile verbosely f =
let open Library in
Dumpglob.noglob ();
let f = if check_suffix f ".vio" then chop_extension f else f in
- let lfdv, lib, univs, disch, tasks, proofs = load_library_todo f in
+ let lfdv, sum, lib, univs, disch, tasks, proofs = load_library_todo f in
Stm.set_compilation_hints lfdv;
let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
- Library.save_library_raw lfdv lib univs proofs
+ Library.save_library_raw lfdv sum lib univs proofs
let compile v f =
ignore(CoqworkmgrApi.get 1);
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 01:47:30 +0000