[summary] Adapt STM to the new Summary API.

We need to a partial restore. I think that we could design a better
API, but further work on the toplevel state should improve it
progressively.

4 files changed, 13 insertions, 8 deletions

diff --git a/library/global.ml b/library/global.ml
index 03d7612a4..ce37dfecf 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -20,6 +20,7 @@ module GlobalSafeEnv : sig
   val set_safe_env : Safe_typing.safe_environment -> unit
   val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit
   val is_joined_environment : unit -> bool
+  val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag
 
 end = struct
 
@@ -30,9 +31,9 @@ let join_safe_environment ?except () =
 
 let is_joined_environment () =
   Safe_typing.is_joined_environment !global_env
-  
-let () =
-  Summary.declare_summary global_env_summary_name
+
+let global_env_summary_tag =
+  Summary.declare_summary_tag global_env_summary_name
     { Summary.freeze_function = (function
         | `Yes -> join_safe_environment (); !global_env
         | `No -> !global_env
@@ -51,6 +52,8 @@ let set_safe_env e = global_env := e
 
 end
 
+let global_env_summary_tag = GlobalSafeEnv.global_env_summary_tag
+
 let safe_env = GlobalSafeEnv.safe_env
 let join_safe_environment ?except () =
   GlobalSafeEnv.join_safe_environment ?except ()
diff --git a/library/global.mli b/library/global.mli
index 1d68d1082..79c8525c6 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -159,4 +159,4 @@ val current_dirpath : unit -> DirPath.t
 
 val with_global : (Environ.env -> DirPath.t -> 'a Univ.in_universe_context_set) -> 'a
 
-val global_env_summary_name : string
+val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag
diff --git a/library/summary.ml b/library/summary.ml
index 5fe3160e1..6df17476b 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -87,7 +87,7 @@ let unfreeze_single name state =
       Pp.(seq [str "Error unfreezing summary "; str name; fnl (); CErrors.iprint e]);
     iraise e
 
-let unfreeze_summaries { summaries; ml_module } =
+let unfreeze_summaries ?(partial=false) { summaries; ml_module } =
   (* The unfreezing of [ml_modules_summary] has to be anticipated since it
    * may modify the content of [summaries] by loading new ML modules *)
   begin match !sum_mod with
@@ -98,8 +98,10 @@ let unfreeze_summaries { summaries; ml_module } =
   let ufz name decl =
     try decl.unfreeze_function String.Map.(find name summaries)
     with Not_found ->
-      Feedback.msg_warning Pp.(str "Summary was captured out of module scope for entry " ++ str name);
-      decl.init_function ()
+      if not partial then begin
+        Feedback.msg_warning Pp.(str "Summary was captured out of module scope for entry " ++ str name);
+        decl.init_function ()
+      end;
   in
   (* String.Map.iter unfreeze_single !sum_map *)
   String.Map.iter ufz !sum_map
diff --git a/library/summary.mli b/library/summary.mli
index 9fc6df6ad..09447199e 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -80,7 +80,7 @@ type frozen
 
 val empty_frozen : frozen
 val freeze_summaries : marshallable:marshallable -> frozen
-val unfreeze_summaries : frozen -> unit
+val unfreeze_summaries : ?partial:bool -> frozen -> unit
 val init_summaries : unit -> unit
 
 (** Typed projection of the summary. Experimental API, use with CARE *)