Merge PR #9220: Move shallow state logic to the function preparing state for workers

9 files changed, 40 insertions, 44 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index d20775a0d7..8699583cdf 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -845,7 +845,7 @@ end
 (** {6 Module operations handling summary freeze/unfreeze} *)
 
 let protect_summaries f =
-  let fs = Summary.freeze_summaries ~marshallable:`No in
+  let fs = Summary.freeze_summaries ~marshallable:false in
   try f fs
   with reraise ->
     (* Something wrong: undo the whole process *)
diff --git a/library/global.ml b/library/global.ml
index 67b00cf411..84d2a37170 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -36,10 +36,9 @@ let is_joined_environment () =
 
 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
-        | `Shallow -> !global_env);
+    { Summary.freeze_function = (fun ~marshallable -> if marshallable then
+        (join_safe_environment (); !global_env)
+        else !global_env);
       unfreeze_function = (fun fr -> global_env := fr);
       init_function = (fun () -> global_env := Safe_typing.empty_environment) }
 
diff --git a/library/goptions.ml b/library/goptions.ml
index 340d74151b..1b907fd966 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -235,7 +235,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
   let default = read() in
   let change =
       let _ = Summary.declare_summary (nickname key)
-        { Summary.freeze_function = (fun _ -> read ());
+        { Summary.freeze_function = (fun ~marshallable -> read ());
           Summary.unfreeze_function = write;
           Summary.init_function = (fun () -> write default) } in
       let cache_options (_,(l,m,v)) =
diff --git a/library/lib.ml b/library/lib.ml
index cce5feeb4a..d4381a6923 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -571,7 +571,7 @@ let open_section id =
   let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
   if Nametab.exists_section obj_dir then
     user_err ~hdr:"open_section" (Id.print id ++ str " already exists.");
-  let fs = Summary.freeze_summaries ~marshallable:`No in
+  let fs = Summary.freeze_summaries ~marshallable:false in
   add_entry (make_foname id) (OpenedSection (prefix, fs));
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
   Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix));
@@ -608,24 +608,21 @@ let close_section () =
 
 type frozen = lib_state
 
-let freeze ~marshallable =
-  match marshallable with
-  | `Shallow ->
-    (* TASSI: we should do something more sensible here *)
-    let lib_stk =
-      CList.map_filter (function
+let freeze ~marshallable = !lib_state
+
+let unfreeze st = lib_state := st
+
+let drop_objects st =
+  let lib_stk =
+    CList.map_filter (function
         | _, Leaf _ -> None
         | n, (CompilingLibrary _ as x) -> Some (n,x)
         | n, OpenedModule (it,e,op,_) ->
-               Some(n,OpenedModule(it,e,op,Summary.empty_frozen))
+          Some(n,OpenedModule(it,e,op,Summary.empty_frozen))
         | n, OpenedSection (op, _) ->
-               Some(n,OpenedSection(op,Summary.empty_frozen)))
-      !lib_state.lib_stk in
-    { !lib_state with lib_stk }
-  | _ ->
-    !lib_state
-
-let unfreeze st = lib_state := st
+          Some(n,OpenedSection(op,Summary.empty_frozen)))
+      st.lib_stk in
+  { st with lib_stk }
 
 let init () =
   unfreeze initial_lib_state;
diff --git a/library/lib.mli b/library/lib.mli
index d1b4977dd5..30569197bc 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -148,9 +148,12 @@ val close_section : unit -> unit
 
 type frozen
 
-val freeze : marshallable:Summary.marshallable -> frozen
+val freeze : marshallable:bool -> frozen
 val unfreeze : frozen -> unit
 
+(** Keep only the libobject structure, not the objects themselves *)
+val drop_objects : frozen -> frozen
+
 val init : unit -> unit
 
 (** {6 Section management for discharge } *)
diff --git a/library/states.ml b/library/states.ml
index ae45b18b9c..92bdc410a3 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -13,8 +13,10 @@ open System
 
 type state = Lib.frozen * Summary.frozen
 
+let lib_of_state = fst
 let summary_of_state = snd
-let replace_summary (lib,_) s = lib, s
+let replace_summary (lib,_) st = lib, st
+let replace_lib (_,st) lib = lib, st
 
 let freeze ~marshallable =
   (Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable)
@@ -24,7 +26,7 @@ let unfreeze (fl,fs) =
   Summary.unfreeze_summaries fs
 
 let extern_state s =
-  System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:`Yes)
+  System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:true)
 
 let intern_state s =
   unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s);
@@ -33,7 +35,7 @@ let intern_state s =
 (* Rollback. *)
 
 let with_state_protection f x =
-  let st = freeze ~marshallable:`No in
+  let st = freeze ~marshallable:false in
   try
     let a = f x in unfreeze st; a
   with reraise ->
diff --git a/library/states.mli b/library/states.mli
index 1e0361ea4f..52feb95222 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -19,11 +19,13 @@ val intern_state : string -> unit
 val extern_state : string -> unit
 
 type state
-val freeze : marshallable:Summary.marshallable -> state
+val freeze : marshallable:bool -> state
 val unfreeze : state -> unit
 
 val summary_of_state : state -> Summary.frozen
+val lib_of_state : state -> Lib.frozen
 val replace_summary : state -> Summary.frozen -> state
+val replace_lib : state -> Lib.frozen -> state
 
 (** {6 Rollback } *)
 
diff --git a/library/summary.ml b/library/summary.ml
index b68f1fb01b..8fbca44353 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -14,10 +14,8 @@ open Util
 
 module Dyn = Dyn.Make ()
 
-type marshallable = [ `Yes | `No | `Shallow ]
-
 type 'a summary_declaration = {
-  freeze_function : marshallable -> 'a;
+  freeze_function : marshallable:bool -> 'a;
   unfreeze_function : 'a -> unit;
   init_function : unit -> unit }
 
@@ -31,7 +29,7 @@ let ml_modules = "ML-MODULES"
 
 let internal_declare_summary fadd sumname sdecl =
   let infun, outfun, tag = Dyn.Easy.make_dyn_tag (mangle sumname) in
-  let dyn_freeze b = infun (sdecl.freeze_function b)
+  let dyn_freeze ~marshallable = infun (sdecl.freeze_function ~marshallable)
   and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
   and dyn_init = sdecl.init_function in
   let ddecl = {
@@ -70,9 +68,9 @@ type frozen = {
 let empty_frozen = { summaries = String.Map.empty; ml_module = None }
 
 let freeze_summaries ~marshallable : frozen =
-  let smap decl = decl.freeze_function marshallable in
+  let smap decl = decl.freeze_function ~marshallable in
   { summaries = String.Map.map smap !sum_map;
-    ml_module = Option.map (fun decl -> decl.freeze_function marshallable) !sum_mod;
+    ml_module = Option.map (fun decl -> decl.freeze_function ~marshallable) !sum_mod;
   }
 
 let warn_summary_out_of_scope =
@@ -130,10 +128,10 @@ let remove_from_summary st tag =
 
 (** All-in-one reference declaration + registration *)
 
-let ref_tag ?(freeze=fun _ r -> r) ~name x =
+let ref_tag ?(freeze=fun ~marshallable r -> r) ~name x =
   let r = ref x in
   let tag = declare_summary_tag name
-    { freeze_function = (fun b -> freeze b !r);
+    { freeze_function = (fun ~marshallable -> freeze ~marshallable !r);
       unfreeze_function = ((:=) r);
       init_function = (fun () -> r := x) } in
   r, tag
@@ -157,7 +155,7 @@ let (!) r =
 let ref ?(freeze=fun x -> x) ~name init =
   let r = Pervasives.ref (CEphemeron.create init, name) in
   declare_summary name
-    { freeze_function = (fun _ -> freeze !r);
+    { freeze_function = (fun ~marshallable -> freeze !r);
       unfreeze_function = ((:=) r);
       init_function = (fun () -> r := init) };
   r
diff --git a/library/summary.mli b/library/summary.mli
index 64222761ba..0d77d725ac 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -11,15 +11,10 @@
 (** This module registers the declaration of global tables, which will be kept
    in synchronization during the various backtracks of the system. *)
 
-type marshallable =
-  [ `Yes       (* Full data will be marshalled to disk                        *)
-  | `No        (* Full data will be store in memory, e.g. for Undo            *)
-  | `Shallow ] (* Only part of the data will be marshalled to a slave process *)
-
 (** Types of global Coq states. The ['a] type should be pure and marshallable by
     the standard OCaml marshalling function. *)
 type 'a summary_declaration = {
-  freeze_function : marshallable -> 'a;
+  freeze_function : marshallable:bool -> 'a;
   (** freeze_function [true] is for marshalling to disk.
    *  e.g. lazy must be forced *)
   unfreeze_function : 'a -> unit;
@@ -50,8 +45,8 @@ val declare_summary_tag : string -> 'a summary_declaration -> 'a Dyn.tag
     The [init_function] restores the reference to its initial value.
     The [freeze_function] can be overridden *)
 
-val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref
-val ref_tag : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref * 'a Dyn.tag
+val ref : ?freeze:(marshallable:bool -> 'a -> 'a) -> name:string -> 'a -> 'a ref
+val ref_tag : ?freeze:(marshallable:bool -> 'a -> 'a) -> name:string -> 'a -> 'a ref * 'a Dyn.tag
 
 (* As [ref] but the value is local to a process, i.e. not sent to, say, proof
  * workers.  It is useful to implement a local cache for example. *)
@@ -81,7 +76,7 @@ val nop : unit -> unit
 type frozen
 
 val empty_frozen : frozen
-val freeze_summaries : marshallable:marshallable -> frozen
+val freeze_summaries : marshallable:bool -> frozen
 val unfreeze_summaries : ?partial:bool -> frozen -> unit
 val init_summaries : unit -> unit