selective join/export of the safe_environment

This generalizes the BuildVi flag and lets one choose which
opaque proofs are done and which not.

10 files changed, 50 insertions, 45 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index e13fb4f08..cf0f715be 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -292,11 +292,6 @@ let hcons_mind mib =
 
 (** {6 Stm machinery } *)
 
-let join_constant_body otab cb =
-  match cb.const_body with
-  | OpaqueDef o -> Opaqueproof.join_opaque otab o
-  | _ -> ()
-
 let string_of_side_effect = function
   | SEsubproof (c,_,_) -> Names.string_of_con c
   | SEscheme (cl,_) ->
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 497856676..ad3e8be4f 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -75,8 +75,6 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 
 val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body
 
-val join_constant_body : Opaqueproof.opaquetab -> constant_body -> unit
-
 (** {6 Hash-consing} *)
 
 (** Here, strictly speaking, we don't perform true hash-consing
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 585b38a08..d91505f89 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -611,21 +611,31 @@ let clean_bounded_mod_expr sign =
   if is_functor sign then collect_mbid MBIset.empty sign else sign
 
 (** {6 Stm machinery } *)
-
-let rec join_module otab mb =
-  implem_iter (join_signature otab) (join_expression otab) mb.mod_expr;
-  Option.iter (join_expression otab) mb.mod_type_alg;
-  join_signature otab mb.mod_type
-and join_modtype otab mt =
-  Option.iter (join_expression otab) mt.typ_expr_alg;
-  join_signature otab mt.typ_expr
-and join_field otab (l,body) = match body with
-  |SFBconst sb -> join_constant_body otab sb
-  |SFBmind _ -> ()
-  |SFBmodule m -> join_module otab m
-  |SFBmodtype m -> join_modtype otab m
-and join_structure otab struc = List.iter (join_field otab) struc
-and join_signature otab sign =
-  functor_iter (join_modtype otab) (join_structure otab) sign
-and join_expression otab me = functor_iter (join_modtype otab) (fun _ -> ()) me
+let join_constant_body except otab cb =
+  match cb.const_body with
+  | OpaqueDef o ->
+      (match Opaqueproof.uuid_opaque otab o with
+      | Some uuid when not(Future.UUIDSet.mem uuid except) ->
+          Opaqueproof.join_opaque otab o
+      | _ -> ())
+  | _ -> ()
+
+let join_structure except otab s =
+  let rec join_module mb =
+    implem_iter join_signature join_expression mb.mod_expr;
+    Option.iter join_expression mb.mod_type_alg;
+    join_signature mb.mod_type
+  and join_modtype mt =
+    Option.iter join_expression mt.typ_expr_alg;
+    join_signature mt.typ_expr
+  and join_field (l,body) = match body with
+    |SFBconst sb -> join_constant_body except otab sb
+    |SFBmind _ -> ()
+    |SFBmodule m -> join_module m
+    |SFBmodtype m -> join_modtype m
+  and join_structure struc = List.iter join_field struc
+  and join_signature sign =
+    functor_iter join_modtype join_structure sign
+  and join_expression me = functor_iter join_modtype (fun _ -> ()) me in
+  join_structure s
 
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 0009b859c..c3f3f2d58 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -80,7 +80,8 @@ val clean_bounded_mod_expr : module_signature -> module_signature
 
 (** {6 Stm machinery } *)
 
-val join_structure : Opaqueproof.opaquetab -> structure_body -> unit
+val join_structure :
+  Future.UUIDSet.t -> Opaqueproof.opaquetab -> structure_body -> unit
 
 (** {6 Errors } *)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 11079d25b..bef72340c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -238,10 +238,12 @@ let push_context ctx = add_constraints (Now (Univ.UContext.constraints ctx))
 let is_curmod_library senv =
   match senv.modvariant with LIBRARY -> true | _ -> false
 
-let join_safe_environment e =
-  Modops.join_structure (Environ.opaque_tables e.env) e.revstruct;
+let join_safe_environment ?(except=Future.UUIDSet.empty) e =
+  Modops.join_structure except (Environ.opaque_tables e.env) e.revstruct;
   List.fold_left
-    (fun e fc -> add_constraints (Now (Future.join fc)) e)
+    (fun e fc ->
+       if Future.UUIDSet.mem (Future.uuid fc) except then e
+       else add_constraints (Now (Future.join fc)) e)
     {e with future_cst = []} e.future_cst
 
 (** {6 Various checks } *)
@@ -745,11 +747,9 @@ let start_library dir senv =
     modvariant = LIBRARY;
     imports = senv.imports }
 
-let export compilation_mode senv dir =
+let export ?except senv dir =
   let senv =
-    try
-      if compilation_mode = Flags.BuildVi then { senv with future_cst = [] }
-      else join_safe_environment senv
+    try join_safe_environment ?except senv
     with e ->
       let e = Errors.push e in
       Errors.errorlabstrm "export" (Errors.print e)
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 6edea363b..943cf3df8 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -48,7 +48,8 @@ val is_curmod_library : safe_environment -> bool
 
 (* safe_environment has functional data affected by lazy computations,
  * thus this function returns a new safe_environment *)
-val join_safe_environment : safe_environment -> safe_environment
+val join_safe_environment :
+  ?except:Future.UUIDSet.t -> safe_environment -> safe_environment
 
 (** {6 Enriching a safe environment } *)
 
@@ -138,7 +139,7 @@ type native_library = Nativecode.global list
 val start_library : DirPath.t -> module_path safe_transformer
 
 val export :
-  Flags.compilation_mode ->
+  ?except:Future.UUIDSet.t ->
   safe_environment -> DirPath.t ->
     module_path * compiled_library * native_library
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index bf6fe9f0d..30cac7771 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -873,9 +873,9 @@ let start_library dir =
   Lib.start_compilation dir mp;
   Lib.add_frozen_state ()
 
-let end_library dir =
+let end_library ?except dir =
   let oname = Lib.end_compilation_checks dir in
-  let mp,cenv,ast = Global.export dir in
+  let mp,cenv,ast = Global.export ?except dir in
   let prefix, lib_stack = Lib.end_compilation oname in
   assert (ModPath.equal mp (MPfile dir));
   let substitute, keep, _ = Lib.classify_segment lib_stack in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index c5dc5a7f5..34d79087d 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -80,7 +80,7 @@ val get_library_symbols_tbl : library_name -> Nativecode.symbol array
 val start_library : library_name -> unit
 
 val end_library :
-  library_name ->
+  ?except:Future.UUIDSet.t -> library_name ->
     Safe_typing.compiled_library * library_objects * Safe_typing.native_library
 
 (** [really_import_module mp] opens the module [mp] (in a Caml sense).
diff --git a/library/global.ml b/library/global.ml
index 49f78e495..68fb1c46f 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -16,15 +16,14 @@ module GlobalSafeEnv : sig
 
   val safe_env : unit -> Safe_typing.safe_environment
   val set_safe_env : Safe_typing.safe_environment -> unit
-  val join_safe_environment : unit -> unit
+  val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit
 
 end = struct
 
 let global_env = ref Safe_typing.empty_environment
 
-let join_safe_environment () =
-  if !Flags.compilation_mode <> Flags.BuildVi then
-    global_env := Safe_typing.join_safe_environment !global_env
+let join_safe_environment ?except () =
+  global_env := Safe_typing.join_safe_environment ?except !global_env
 
 let () =
   Summary.declare_summary "Global environment"
@@ -47,7 +46,8 @@ let set_safe_env e = global_env := e
 end
 
 let safe_env = GlobalSafeEnv.safe_env
-let join_safe_environment = GlobalSafeEnv.join_safe_environment
+let join_safe_environment ?except () =
+  GlobalSafeEnv.join_safe_environment ?except ()
 
 let env () = Safe_typing.env_of_safe_env (safe_env ())
 
@@ -140,7 +140,7 @@ let mind_of_delta_kn kn =
 (** Operations on libraries *)
 
 let start_library dir = globalize (Safe_typing.start_library dir)
-let export s = Safe_typing.export !Flags.compilation_mode (safe_env ()) s
+let export ?except s = Safe_typing.export ?except (safe_env ()) s
 let import c u d = globalize (Safe_typing.import c u d)
 
 
diff --git a/library/global.mli b/library/global.mli
index 8ae77a9e4..348f0be99 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -98,7 +98,7 @@ val universes_of_constant_body :
 (** {6 Compiled libraries } *)
 
 val start_library : DirPath.t -> module_path
-val export : DirPath.t ->
+val export : ?except:Future.UUIDSet.t -> DirPath.t ->
   module_path * Safe_typing.compiled_library * Safe_typing.native_library
 val import :
   Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest ->
@@ -111,7 +111,7 @@ val import :
 
 val env_of_context : Environ.named_context_val -> Environ.env
 
-val join_safe_environment : unit -> unit
+val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit
 
 val is_polymorphic : Globnames.global_reference -> bool
 val is_template_polymorphic : Globnames.global_reference -> bool