aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check.ml29
-rw-r--r--checker/cic.mli9
-rw-r--r--checker/environ.ml2
-rw-r--r--checker/environ.mli6
-rw-r--r--checker/mod_checking.ml3
-rw-r--r--checker/safe_typing.ml14
-rw-r--r--checker/safe_typing.mli4
-rw-r--r--checker/values.ml6
-rw-r--r--kernel/safe_typing.ml31
-rw-r--r--kernel/safe_typing.mli11
-rw-r--r--library/declaremods.ml4
-rw-r--r--library/declaremods.mli3
-rw-r--r--library/global.ml2
-rw-r--r--library/global.mli3
-rw-r--r--library/library.ml49
-rw-r--r--library/library.mli3
-rw-r--r--toplevel/stm.ml20
-rw-r--r--toplevel/stm.mli2
-rw-r--r--toplevel/vernac.ml2
19 files changed, 128 insertions, 75 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 85324ec44..668ee3705 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -45,7 +45,8 @@ type library_t = {
library_compiled : Cic.compiled_library;
library_opaques : Cic.opaque_table;
library_deps : Cic.library_deps;
- library_digest : Digest.t }
+ library_digest : Cic.vodigest;
+ library_extra_univs : Univ.constraints }
module LibraryOrdered =
struct
@@ -112,11 +113,11 @@ let check_one_lib admit (dir,m) =
if LibrarySet.mem dir admit then
(Flags.if_verbose ppnl
(str "Admitting library: " ++ pr_dirpath dir);
- Safe_typing.unsafe_import file md dig)
+ Safe_typing.unsafe_import file md m.library_extra_univs dig)
else
(Flags.if_verbose ppnl
(str "Checking library: " ++ pr_dirpath dir);
- Safe_typing.import file md dig);
+ Safe_typing.import file md m.library_extra_univs dig);
Flags.if_verbose pp (fnl());
pp_flush ();
register_loaded_library m
@@ -290,13 +291,14 @@ let with_magic_number_check f a =
open Cic
-let mk_library md f table digest = {
+let mk_library md f table digest cst = {
library_name = md.md_name;
library_filename = f;
library_compiled = md.md_compiled;
library_opaques = table;
library_deps = md.md_deps;
- library_digest = digest }
+ library_digest = digest;
+ library_extra_univs = cst }
let name_clash_message dir mdir f =
str ("The file " ^ f ^ " contains library") ++ spc () ++
@@ -312,7 +314,7 @@ let intern_from_file (dir, f) =
try
let ch = with_magic_number_check raw_intern_library f in
let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in
- let (opaque_csts:'a option), _, _ = 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
let (tasks:'a option), _, _ = System.marshal_in_segment f ch in
let (table:Cic.opaque_table), pos, checksum =
@@ -331,21 +333,30 @@ let intern_from_file (dir, f) =
(str "The file "++str f++str " contains unfinished tasks");
if opaque_csts <> None then begin
pp (str " (was a vi file) ");
- Validate.validate !Flags.debug Values.v_univopaques opaque_csts
+ Option.iter (fun (_,_,b) -> if not b then
+ errorlabstrm "intern_from_file"
+ (str "The file "++str f++str " is still a .vi"))
+ opaque_csts;
+ Validate.validate !Flags.debug Values.v_univopaques opaque_csts;
end;
(* Verification of the unmarshalled values *)
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.Dvivo (digest,udg)
+ else (Cic.Dvo digest) in
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;
- Option.iter (fun opaque_csts ->
+ Option.iter (fun (opaque_csts,_,_) ->
opaque_univ_tables :=
LibraryMap.add md.md_name opaque_csts !opaque_univ_tables)
opaque_csts;
- mk_library md f table digest
+ let extra_cst =
+ Option.default Univ.empty_constraint (Option.map pi2 opaque_csts) in
+ mk_library 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 8e6c5580d..bfea85327 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -362,7 +362,11 @@ type nativecode_symb_array
type compilation_unit_name = DirPath.t
-type library_info = compilation_unit_name * Digest.t
+type vodigest =
+ | Dvo of Digest.t (* The digest of the seg_lib part *)
+ | Dvivo of Digest.t * Digest.t (* The digest of the seg_lib + seg_univ part *)
+
+type library_info = compilation_unit_name * vodigest
type library_deps = library_info array
@@ -388,7 +392,8 @@ type library_disk = {
md_imports : compilation_unit_name array }
type opaque_table = constr Future.computation array
-type univ_table = Univ.constraints Future.computation array option
+type univ_table =
+ (Univ.constraints Future.computation array * Univ.constraints * bool) option
(** A .vo file is currently made of :
diff --git a/checker/environ.ml b/checker/environ.ml
index 1485d6bf0..be6bdec11 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -22,7 +22,7 @@ type env = {
env_globals : globals;
env_rel_context : rel_context;
env_stratification : stratification;
- env_imports : Digest.t MPmap.t }
+ env_imports : Cic.vodigest MPmap.t }
let empty_env = {
env_globals =
diff --git a/checker/environ.mli b/checker/environ.mli
index a4162d67f..46b390d0a 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -17,7 +17,7 @@ type env = {
env_globals : globals;
env_rel_context : rel_context;
env_stratification : stratification;
- env_imports : Digest.t MPmap.t;
+ env_imports : Cic.vodigest MPmap.t;
}
val empty_env : env
@@ -26,8 +26,8 @@ val engagement : env -> Cic.engagement option
val set_engagement : Cic.engagement -> env -> env
(* Digests *)
-val add_digest : env -> DirPath.t -> Digest.t -> env
-val lookup_digest : env -> DirPath.t -> Digest.t
+val add_digest : env -> DirPath.t -> Cic.vodigest -> env
+val lookup_digest : env -> DirPath.t -> Cic.vodigest
(* de Bruijn variables *)
val rel_context : env -> rel_context
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index ec0014175..add993581 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -26,9 +26,6 @@ let refresh_arity ar =
let check_constant_declaration env kn cb =
Flags.if_verbose ppnl (str " checking cst: " ++ prcon kn);
(* let env = add_constraints cb.const_constraints env in*)
- (* Constraints of an opauqe proof are not in the module *)
- let env =
- add_constraints (Declarations.force_lazy_constr_univs cb.const_body) env in
(match cb.const_type with
NonPolymorphicType ty ->
let ty, cu = refresh_arity ty in
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 7fcd749f5..0d7364ce6 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -25,9 +25,10 @@ let set_engagement c =
genv := set_engagement c !genv
(* full_add_module adds module with universes and constraints *)
-let full_add_module dp mb digest =
+let full_add_module dp mb univs digest =
let env = !genv in
let env = add_constraints mb.mod_constraints env in
+ let env = add_constraints univs env in
let env = Modops.add_module mb env in
genv := add_digest env dp digest
@@ -68,19 +69,20 @@ let stamp_library file digest = ()
(* When the module is checked, digests do not need to match, but a
warning is issued in case of mismatch *)
-let import file clib digest =
+let import file clib univs digest =
let env = !genv in
check_imports msg_warning clib.comp_name env clib.comp_deps;
check_engagement env clib.comp_enga;
let mb = clib.comp_mod in
Mod_checking.check_module
- (add_constraints mb.mod_constraints env) mb.mod_mp mb;
+ (add_constraints univs
+ (add_constraints mb.mod_constraints env)) mb.mod_mp mb;
stamp_library file digest;
- full_add_module clib.comp_name mb digest
+ full_add_module clib.comp_name mb univs digest
(* When the module is admitted, digests *must* match *)
-let unsafe_import file clib digest =
+let unsafe_import file clib univs digest =
let env = !genv in
check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps;
check_engagement env clib.comp_enga;
- full_add_module clib.comp_name clib.comp_mod digest
+ full_add_module clib.comp_name clib.comp_mod univs digest
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index 59d95c36d..e2aad1d93 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -15,6 +15,6 @@ val get_env : unit -> env
val set_engagement : engagement -> unit
val import :
- CUnix.physical_path -> compiled_library -> Digest.t -> unit
+ CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit
val unsafe_import :
- CUnix.physical_path -> compiled_library -> Digest.t -> unit
+ CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit
diff --git a/checker/values.ml b/checker/values.ml
index 0a2e53799..f73f83d16 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -284,7 +284,8 @@ and v_modtype =
(** kernel/safe_typing *)
-let v_deps = Array (v_tuple "dep" [|v_dp;String|])
+let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |])
+let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|])
let v_compiled_lib =
v_tuple "compiled" [|v_dp;v_module;v_deps;Opt v_engagement;Any|]
@@ -301,7 +302,8 @@ let v_lib =
Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps;Array v_dp|])
let v_opaques = Array (v_computation v_constr)
-let v_univopaques = Opt (Array (v_computation v_cstrs))
+let v_univopaques =
+ Opt (Tuple ("univopaques",[|Array (v_computation v_cstrs);v_cstrs;v_bool|]))
(** Registering dynamic values *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 867705c47..8ff01a755 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -91,7 +91,18 @@ open Declarations
*)
-type library_info = DirPath.t * Digest.t
+type vodigest =
+ | Dvo_or_vi of Digest.t (* The digest of the seg_lib part *)
+ | Dvivo of Digest.t * Digest.t (* The digest of the seg_lib + seg_univ part *)
+
+let digest_match ~actual ~required =
+ match actual, required with
+ | Dvo_or_vi d1, Dvo_or_vi d2
+ | Dvivo (d1,_), Dvo_or_vi d2 -> String.equal d1 d2
+ | Dvivo (d1,e1), Dvivo (d2,e2) -> String.equal d1 d2 && String.equal e1 e2
+ | Dvo_or_vi _, Dvivo _ -> false
+
+type library_info = DirPath.t * vodigest
(** Functor and funsig parameters, most recent first *)
type module_parameters = (MBId.t * module_type_body) list
@@ -252,11 +263,11 @@ let check_initial senv = assert (is_initial senv)
with the correct digests. *)
let check_imports current_libs needed =
- let check (id,stamp) =
+ let check (id,required) =
try
- let actual_stamp = List.assoc_f DirPath.equal id current_libs in
- if not (String.equal stamp actual_stamp) then
- Errors.error
+ let actual = List.assoc_f DirPath.equal id current_libs in
+ if not(digest_match ~actual ~required) then
+ Errors.error
("Inconsistent assumptions over module "^(DirPath.to_string id)^".")
with Not_found ->
Errors.error ("Reference to unknown module "^(DirPath.to_string id)^".")
@@ -661,8 +672,6 @@ type compiled_library = {
type native_library = Nativecode.global list
-let join_compiled_library l = Modops.join_module l.comp_mod
-
let start_library dir senv =
check_initial senv;
assert (not (DirPath.is_empty dir));
@@ -709,12 +718,15 @@ let export compilation_mode senv dir =
in
mp, lib, ast
-let import lib digest senv =
+(* cst are the constraints that were computed by the vi2vo step and hence are
+ * not part of the mb.mod_constraints field (but morally should be) *)
+let import lib cst vodigest senv =
check_imports senv.imports lib.comp_deps;
check_engagement senv.env lib.comp_enga;
let mp = MPfile lib.comp_name in
let mb = lib.comp_mod in
let env = Environ.add_constraints mb.mod_constraints senv.env in
+ let env = Environ.add_constraints cst env in
(mp, lib.comp_natsymbs),
{ senv with
env =
@@ -723,10 +735,9 @@ let import lib digest senv =
in
Modops.add_linked_module mb linkinfo env);
modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver;
- imports = (lib.comp_name,digest)::senv.imports;
+ imports = (lib.comp_name,vodigest)::senv.imports;
loads = (mp,mb)::senv.loads }
-
(** {6 Safe typing } *)
type judgment = Environ.unsafe_judgment
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index e2d1e37e9..d70d7d8be 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -8,6 +8,12 @@
open Names
+type vodigest =
+ | Dvo_or_vi of Digest.t (* The digest of the seg_lib part *)
+ | Dvivo of Digest.t * Digest.t (* The digest of the seg_lib + seg_univ part *)
+
+val digest_match : actual:vodigest -> required:vodigest -> bool
+
(** {6 Safe environments } *)
(** Since we are now able to type terms, we can define an abstract type
@@ -120,11 +126,10 @@ val export :
safe_environment -> DirPath.t ->
module_path * compiled_library * native_library
-val import : compiled_library -> Digest.t ->
+(* Constraints are non empty iff the file is a vi2vo *)
+val import : compiled_library -> Univ.constraints -> vodigest ->
(module_path * Nativecode.symbol array) safe_transformer
-val join_compiled_library : compiled_library -> unit
-
(** {6 Safe typing judgments } *)
type judgment
diff --git a/library/declaremods.ml b/library/declaremods.ml
index c60e008d1..2b917587c 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 89bcccef3..5ff471e69 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 9515ff1a8..f75c8e592 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 856956a17..e11e1c017 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 a1760cdf1..b75329a22 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 afcce7f6c..16664d880 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
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 8c1c6b02b..9cb5e9511 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -641,7 +641,7 @@ module Slaves : sig
val finish_task :
string ->
Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
- tasks -> int -> unit
+ tasks -> int -> Library.seg_univ
val cancel_worker : int -> unit
@@ -878,7 +878,7 @@ end = struct (* {{{ *)
Pp.msg_error (str"unable to print error message: " ++
str (Printexc.to_string e))); None
- let finish_task name u d p l i =
+ let finish_task name (u,cst,_) d p l i =
let bucket =
match List.nth l i with ReqBuildProof (_,_,_,_,bucket,_) -> bucket in
match check_task_aux (Printf.sprintf ", bucket %d" bucket) name l i with
@@ -898,9 +898,10 @@ end = struct (* {{{ *)
let pr = Future.chain ~greedy:true ~pure:true pr discharge in
let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in
Future.sink pr;
- Future.sink uc;
+ let extra = Future.join uc in
u.(bucket) <- uc;
- p.(bucket) <- pr
+ p.(bucket) <- pr;
+ u, Univ.union_constraints cst extra, false
| _ -> assert false
let check_task name l i =
@@ -1611,12 +1612,15 @@ let check_task name (tasks,_) i =
let info_tasks (tasks,_) = Slaves.info_tasks tasks
let finish_tasks name u d p (t,rcbackup as tasks) =
RemoteCounter.restore rcbackup;
- let finish_task (_,_,i) =
+ let finish_task u (_,_,i) =
let vcs = VCS.backup () in
- Future.purify (Slaves.finish_task name u d p t) i;
+ let u = Future.purify (Slaves.finish_task name u d p t) i in
Pp.pperr_flush ();
- VCS.restore vcs in
- try List.iter finish_task (info_tasks tasks)
+ VCS.restore vcs;
+ u in
+ try
+ let u, a, _ = List.fold_left finish_task u (info_tasks tasks) in
+ (u,a,true), p
with e ->
Pp.pperrnl Pp.(str"File " ++ str name ++ str ":" ++ spc () ++ print e);
exit 1
diff --git a/toplevel/stm.mli b/toplevel/stm.mli
index c47bacf65..1eba274ab 100644
--- a/toplevel/stm.mli
+++ b/toplevel/stm.mli
@@ -50,7 +50,7 @@ val check_task : string -> tasks -> int -> bool
val info_tasks : tasks -> (string * float * int) list
val finish_tasks : string ->
Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
- tasks -> unit
+ tasks -> Library.seg_univ * Library.seg_proofs
(* Id of the tip of the current branch *)
val get_current_state : unit -> Stateid.t
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 4ea9c2236..11cb726c7 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -348,6 +348,6 @@ let compile verbosely f =
let f = if check_suffix f ".vi" then chop_extension f else f in
let lfdv, lib, univs, disch, tasks, proofs = load_library_todo f in
Stm.set_compilation_hints (Aux_file.load_aux_file_for lfdv);
- Stm.finish_tasks lfdv univs disch proofs tasks;
+ let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
Library.save_library_raw lfdv lib univs proofs
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 21:05:34 +0000