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

5 files changed, 15 insertions, 6 deletions

diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 790b62c9d0..4e79b50b79 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1359,7 +1359,7 @@ let inNotation : notation_obj -> obj =
 (**********************************************************************)
 
 let with_lib_stk_protection f x =
-  let fs = Lib.freeze ~marshallable:`No in
+  let fs = Lib.freeze ~marshallable:false in
   try let a = f x in Lib.unfreeze fs; a
   with reraise ->
     let reraise = CErrors.push reraise in
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 3620e177fe..8d6268753e 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -394,7 +394,7 @@ let unfreeze_ml_modules x =
 
 let _ =
   Summary.declare_ml_modules_summary
-    { Summary.freeze_function = (fun _ -> get_loaded_modules ());
+    { Summary.freeze_function = (fun ~marshallable -> get_loaded_modules ());
       Summary.unfreeze_function = unfreeze_ml_modules;
       Summary.init_function = reset_loaded_modules }
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ecfe39de09..e6e3db4beb 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2436,7 +2436,7 @@ let interp ?verbosely ?proof ~st cmd =
   Vernacstate.unfreeze_interp_state st;
   try
     interp ?verbosely ?proof ~st cmd;
-    Vernacstate.freeze_interp_state `No
+    Vernacstate.freeze_interp_state ~marshallable:false
   with exn ->
     let exn = CErrors.push exn in
     Vernacstate.invalidate_cache ();
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index aa8bcdc328..b40bccf27e 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -33,11 +33,18 @@ let do_if_not_cached rf f v =
   | Some _ ->
     ()
 
-let freeze_interp_state marshallable =
+let freeze_interp_state ~marshallable =
   { system = update_cache s_cache (States.freeze ~marshallable);
     proof  = update_cache s_proof (Proof_global.freeze ~marshallable);
-    shallow = marshallable = `Shallow }
+    shallow = marshallable }
 
 let unfreeze_interp_state { system; proof } =
   do_if_not_cached s_cache States.unfreeze system;
   do_if_not_cached s_proof Proof_global.unfreeze proof
+
+let make_shallow st =
+  let lib = States.lib_of_state st.system in
+  { st with
+    system = States.replace_lib st.system @@ Lib.drop_objects lib;
+    shallow = true;
+  }
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index b4d478d12d..ed20cb935a 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -14,8 +14,10 @@ type t = {
   shallow : bool                 (* is the state trimmed down (libstack) *)
 }
 
-val freeze_interp_state : Summary.marshallable -> t
+val freeze_interp_state : marshallable:bool -> t
 val unfreeze_interp_state : t -> unit
 
+val make_shallow : t -> t
+
 (* WARNING: Do not use, it will go away in future releases *)
 val invalidate_cache : unit -> unit