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

21 files changed, 140 insertions, 129 deletions

diff --git a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh b/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh
new file mode 100644
index 0000000000..efcdd2e97f
--- /dev/null
+++ b/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "9220" ] || [ "$CI_BRANCH" = "stm-shallow-logic" ]; then
+
+    paramcoq_CI_REF=stm-shallow-logic
+    paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq
+
+fi
diff --git a/interp/notation.ml b/interp/notation.ml
index c866929234..b0854de4a3 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1902,7 +1902,7 @@ let pr_visibility prglob = function
 (**********************************************************************)
 (* Synchronisation with reset *)
 
-let freeze _ =
+let freeze ~marshallable =
  (!scope_map, !scope_stack, !uninterp_scope_stack, !arguments_scope,
   !delimiters_map, !notations_key_table, !scope_class_map,
   !prim_token_interp_infos, !prim_token_uninterp_infos,
@@ -1939,7 +1939,7 @@ let _ =
       Summary.init_function = init }
 
 let with_notation_protection f x =
-  let fs = freeze false in
+  let fs = freeze ~marshallable:false in
   try let a = f x in unfreeze fs; a
   with reraise ->
     let reraise = CErrors.push reraise in
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
 
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 923147ba2e..19ae97da77 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -553,7 +553,7 @@ type frozen_t =
   (grammar_entry * GramState.t) list *
   CLexer.keyword_state
 
-let freeze _ : frozen_t =
+let freeze ~marshallable : frozen_t =
   (!grammar_stack, CLexer.get_keyword_state ())
 
 (* We compare the current state of the grammar and the state to unfreeze,
@@ -586,7 +586,7 @@ let parser_summary_tag =
       Summary.init_function = Summary.nop }
 
 let with_grammar_rule_protection f x =
-  let fs = freeze false in
+  let fs = freeze ~marshallable:false in
   try let a = f x in unfreeze fs; a
   with reraise ->
     let reraise = CErrors.push reraise in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 5d0d17ee6b..f9938c0356 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -492,7 +492,7 @@ type tcc_lemma_value =
 
 (* We only "purify" on exceptions. XXX: What is this doing here? *)
 let funind_purify f x =
-  let st = Vernacstate.freeze_interp_state `No in
+  let st = Vernacstate.freeze_interp_state ~marshallable:false in
   try f x
   with e ->
     let e = CErrors.push e in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2027ad4e21..8077da8807 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -462,11 +462,8 @@ module V82 = struct
 end
 
 let freeze ~marshallable =
-  match marshallable with
-  | `Yes ->
-      CErrors.anomaly (Pp.str"full marshalling of proof state not supported.")
-  | `Shallow -> !pstates
-  | `No -> !pstates
+  if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.")
+  else !pstates
 let unfreeze s = pstates := s; update_proof_mode ()
 let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof
 let copy_terminators ~src ~tgt =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index d9c32cf9d5..9e904c57aa 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -135,7 +135,7 @@ module V82 : sig
   Decl_kinds.goal_kind)
 end
 
-val freeze : marshallable:[`Yes | `No | `Shallow] -> t
+val freeze : marshallable:bool -> t
 val unfreeze : t -> unit
 val proof_of_state : t -> Proof.t
 val copy_terminators : src:t -> tgt:t -> t
diff --git a/stm/stm.ml b/stm/stm.ml
index 77fb49625c..ffd13fcb73 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -78,7 +78,7 @@ let async_proofs_is_master opt =
 
 (* Protect against state changes *)
 let stm_purify f x =
-  let st = Vernacstate.freeze_interp_state `No in
+  let st = Vernacstate.freeze_interp_state ~marshallable:false in
   try
     let res = f x in
     Vernacstate.unfreeze_interp_state st;
@@ -343,7 +343,7 @@ module VCS : sig
   val set_ldir : Names.DirPath.t -> unit
   val get_ldir : unit -> Names.DirPath.t
 
-  val is_interactive : unit -> [`Yes | `No | `Shallow]
+  val is_interactive : unit -> bool
   val is_vio_doc : unit -> bool
 
   val current_branch : unit -> Branch.t
@@ -543,8 +543,8 @@ end = struct (* {{{ *)
 
   let is_interactive () =
     match !doc_type with
-    | Interactive _ -> `Yes
-    | _ -> `No
+    | Interactive _ -> true
+    | _ -> false
 
   let is_vio_doc () =
     match !doc_type with
@@ -632,13 +632,20 @@ end = struct (* {{{ *)
                          " to "^Stateid.to_string block_stop^"."))
     in aux block_stop
 
+  (* [slice] copies a slice of the DAG, keeping only the last known valid state.
+     When it copies a state, it drops the libobjects and keeps only the structure. *)
   let slice ~block_start ~block_stop =
     let l = nodes_in_slice ~block_start ~block_stop in
     let copy_info v id =
       Vcs_.set_info v id
         { (get_info id) with state = Empty; vcs_backup = None,None } in
+    let make_shallow = function
+      | Valid st -> Valid (Vernacstate.make_shallow st)
+      | x -> x
+    in
     let copy_info_w_state v id =
-      Vcs_.set_info v id { (get_info id) with vcs_backup = None,None } in
+      let info = get_info id in
+      Vcs_.set_info v id { info with state = make_shallow info.state; vcs_backup = None,None } in
     let copy_proof_blockes v =
       let nodes = Vcs_.Dag.all_nodes (Vcs_.dag v) in
       let props =
@@ -776,14 +783,14 @@ module State : sig
   val define :
     doc:doc ->
     ?safe_id:Stateid.t ->
-    ?redefine:bool -> ?cache:Summary.marshallable ->
+    ?redefine:bool -> ?cache:bool ->
     ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit
 
   val fix_exn_ref : (Exninfo.iexn -> Exninfo.iexn) ref
 
   val install_cached : Stateid.t -> unit
-  val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool
-  val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool
+  val is_cached : ?cache:bool -> Stateid.t -> bool
+  val is_cached_and_valid : ?cache:bool -> Stateid.t -> bool
 
   val exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn
 
@@ -832,16 +839,15 @@ end = struct (* {{{ *)
     Summary.project_from_summary st Util.(pi2 summary_pstate),
     Summary.project_from_summary st Util.(pi3 summary_pstate)
 
-  let freeze marshallable id =
-    VCS.set_state id (Valid (Vernacstate.freeze_interp_state marshallable))
+  let freeze ~marshallable id =
+    VCS.set_state id (Valid (Vernacstate.freeze_interp_state ~marshallable))
 
   let freeze_invalid id iexn = VCS.set_state id (Error iexn)
 
-  let is_cached ?(cache=`No) id only_valid =
+  let is_cached ?(cache=false) id only_valid =
     if Stateid.equal id !cur_id then
       try match VCS.get_info id with
-        | { state = Empty } when cache = `Yes -> freeze `No id; true
-        | { state = Empty } when cache = `Shallow -> freeze `Shallow id; true
+        | { state = Empty } when cache -> freeze ~marshallable:false id; true
         | _ -> true
       with VCS.Expired -> false
     else
@@ -866,7 +872,7 @@ end = struct (* {{{ *)
 
     | _ ->
         (* coqc has a 1 slot cache and only for valid states *)
-        if VCS.is_interactive () = `No && Stateid.equal id !cur_id then ()
+        if not (VCS.is_interactive ()) && Stateid.equal id !cur_id then ()
         else anomaly Pp.(str "installing a non cached state.")
 
   let get_cached id =
@@ -924,7 +930,7 @@ end = struct (* {{{ *)
     let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in
     e1 == e2
 
-  let define ~doc ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
+  let define ~doc ?safe_id ?(redefine=false) ?(cache=false) ?(feedback_processed=true)
         f id
   =
     feedback ~id:id (ProcessingIn !Flags.async_proofs_worker_id);
@@ -933,13 +939,12 @@ end = struct (* {{{ *)
       anomaly Pp.(str"defining state "++str str_id++str" twice.");
     try
       stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^
-        if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
+        if cache then "Y)" else "N)");
       let good_id = match safe_id with None -> !cur_id | Some id -> id in
       fix_exn_ref := exn_on id ~valid:good_id;
       f ();
       fix_exn_ref := (fun x -> x);
-      if cache = `Yes then freeze `No id
-      else if cache = `Shallow then freeze `Shallow id;
+      if cache then freeze ~marshallable:false id;
       stm_prerr_endline (fun () -> "setting cur id to "^str_id);
       cur_id := id;
       if feedback_processed then
@@ -958,14 +963,14 @@ end = struct (* {{{ *)
         | None, Some good_id -> (exn_on id ~valid:good_id (e, info))
         | Some _, None -> (e, info)
         | Some (_,at), Some id -> (e, Stateid.add info ~valid:id at) in
-      if cache = `Yes || cache = `Shallow then freeze_invalid id ie;
+      if cache then freeze_invalid id ie;
       Hooks.(call unreachable_state ~doc id ie);
       Exninfo.iraise ie
 
   let init_state = ref None
 
   let register_root_state () =
-    init_state := Some (Vernacstate.freeze_interp_state `No)
+    init_state := Some (Vernacstate.freeze_interp_state ~marshallable:false)
 
   let restore_root_state () =
     cur_id := Stateid.dummy;
@@ -1178,7 +1183,7 @@ end = struct (* {{{ *)
     | _ -> None
 
   let undo_vernac_classifier v ~doc =
-    if VCS.is_interactive () = `No && !cur_opt.async_proofs_cache <> Some Force
+    if not (VCS.is_interactive ()) && !cur_opt.async_proofs_cache <> Some Force
     then undo_costly_in_batch_mode v;
     try
       match Vernacprop.under_control v with
@@ -1508,9 +1513,7 @@ end = struct (* {{{ *)
   let build_proof_here ~doc ?loc ~drop_pt (id,valid) eop =
     Future.create (State.exn_on id ~valid) (fun () ->
       let wall_clock1 = Unix.gettimeofday () in
-      if VCS.is_interactive () = `No
-      then Reach.known_state ~doc ~cache:`No eop
-      else Reach.known_state ~doc ~cache:`Shallow eop;
+      Reach.known_state ~doc ~cache:(VCS.is_interactive ()) eop;
       let wall_clock2 = Unix.gettimeofday () in
       Aux_file.record_in_aux_at ?loc "proof_build_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
@@ -1532,7 +1535,7 @@ end = struct (* {{{ *)
        * a bad fixpoint *)
       let fix_exn = Future.fix_exn_of future_proof in
       (* STATE: We use the current installed imperative state *)
-      let st = Vernacstate.freeze_interp_state `No in
+      let st = Vernacstate.freeze_interp_state ~marshallable:false in
       if not drop then begin
         let checked_proof = Future.chain future_proof (fun p ->
           let opaque = Proof_global.Opaque in
@@ -1545,7 +1548,7 @@ end = struct (* {{{ *)
           let terminator = (* The one sent by master is an InvalidKey *)
             Lemmas.(standard_proof_terminator []) in
 
-          let st = Vernacstate.freeze_interp_state `No in
+          let st = Vernacstate.freeze_interp_state ~marshallable:false in
           stm_vernac_interp stop
             ~proof:(pobject, terminator) st
             { verbose = false; loc; indentation = 0; strlen = 0;
@@ -1676,7 +1679,7 @@ end = struct (* {{{ *)
         with VCS.Expired -> cur in
       aux stop in
     try
-      Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No stop;
+      Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false stop;
       if drop then
         let _proof = Proof_global.return_proof ~allow_partial:true () in
         `OK_ADMITTED
@@ -1689,14 +1692,14 @@ end = struct (* {{{ *)
         Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
-      Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No start;
+      Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false start;
       (* STATE SPEC:
        * - start: First non-expired state! [This looks very fishy]
        * - end  : start + qed
        * => takes nothing from the itermediate states.
        *)
       (* STATE We use the state resulting from reaching start. *)
-      let st = Vernacstate.freeze_interp_state `No in
+      let st = Vernacstate.freeze_interp_state ~marshallable:false in
       ignore(stm_vernac_interp stop ~proof st
         { verbose = false; loc; indentation = 0; strlen = 0;
           expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) });
@@ -1934,7 +1937,7 @@ end = struct (* {{{ *)
   let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } =
     Option.iter VCS.restore vcs;
     try
-      Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:`No id;
+      Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:false id;
       stm_purify (fun () ->
        let Proof.{sigma=sigma0} = Proof.data (Proof_global.give_me_the_proof ()) in
        let g = Evd.find sigma0 r_goal in
@@ -1955,7 +1958,7 @@ end = struct (* {{{ *)
          * => captures state id in a future closure, which will
            discard execution state but for the proof + univs.
         *)
-        let st = Vernacstate.freeze_interp_state `No in
+        let st = Vernacstate.freeze_interp_state ~marshallable:false in
         ignore(stm_vernac_interp r_state_fb st ast);
         let Proof.{sigma} = Proof.data (Proof_global.give_me_the_proof ()) in
         match Evd.(evar_body (find sigma r_goal)) with
@@ -1994,7 +1997,7 @@ end = struct (* {{{ *)
         | VernacFail e -> find ~time ~batch ~fail:true e
         | e -> e, time, batch, fail in
       find ~time:false ~batch:false ~fail:false e in
-    let st = Vernacstate.freeze_interp_state `No in
+    let st = Vernacstate.freeze_interp_state ~marshallable:false in
     Vernacentries.with_fail st fail (fun () ->
     (if time then System.with_time ~batch else (fun x -> x)) (fun () ->
     ignore(TaskQueue.with_n_workers nworkers (fun queue ->
@@ -2089,9 +2092,9 @@ end = struct (* {{{ *)
   let perform { r_where; r_doc; r_what; r_for } =
     VCS.restore r_doc;
     VCS.print ();
-    Reach.known_state ~doc:dummy_doc (* XXX should be r_doc *) ~cache:`No r_where;
+    Reach.known_state ~doc:dummy_doc (* XXX should be r_doc *) ~cache:false r_where;
     (* STATE *)
-    let st = Vernacstate.freeze_interp_state `No in
+    let st = Vernacstate.freeze_interp_state ~marshallable:false in
     try
       (* STATE SPEC:
        * - start: r_where
@@ -2133,14 +2136,14 @@ end (* }}} *)
 and Reach : sig
 
   val known_state :
-    doc:doc -> ?redefine_qed:bool -> cache:Summary.marshallable ->
+    doc:doc -> ?redefine_qed:bool -> cache:bool ->
       Stateid.t -> unit
 
 end = struct (* {{{ *)
 
 let async_policy () =
-  if Attributes.is_universe_polymorphism () then false
-  else if VCS.is_interactive () = `Yes then
+  if Attributes.is_universe_polymorphism () then false (* FIXME this makes no sense, it is the default value of the attribute *)
+  else if VCS.is_interactive () then
     (async_proofs_is_master !cur_opt || !cur_opt.async_proofs_mode = APonLazy)
   else
     (VCS.is_vio_doc () || !cur_opt.async_proofs_mode <> APoff)
@@ -2322,7 +2325,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                 * - end  : maybe after recovery command.
                *)
                (* STATE: We use an updated state with proof *)
-               let st = Vernacstate.freeze_interp_state `No in
+               let st = Vernacstate.freeze_interp_state ~marshallable:false in
                Option.iter (fun expr -> ignore(stm_vernac_interp id st {
                   verbose = true; loc = None; expr; indentation = 0;
                   strlen = 0 } ))
@@ -2358,11 +2361,11 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
   (* ugly functions to process nested lemmas, i.e. hard to reproduce
    * side effects *)
   let cherry_pick_non_pstate () =
-    let st = Summary.freeze_summaries ~marshallable:`No in
+    let st = Summary.freeze_summaries ~marshallable:false in
     let st = Summary.remove_from_summary st Util.(pi1 summary_pstate) in
     let st = Summary.remove_from_summary st Util.(pi2 summary_pstate) in
     let st = Summary.remove_from_summary st Util.(pi3 summary_pstate) in
-    st, Lib.freeze ~marshallable:`No in
+    st, Lib.freeze ~marshallable:false in
 
   let inject_non_pstate (s,l) =
     Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env ()
@@ -2393,7 +2396,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
       | `Cmd { cast = x; cqueue = `TacQueue (solve,abstract,cancel_switch); cblock } ->
           (fun () ->
             resilient_tactic id cblock (fun () ->
-              reach ~cache:`Shallow view.next;
+              reach ~cache:true view.next;
               Partac.vernac_interp ~solve ~abstract ~cancel_switch
                 !cur_opt.async_proofs_n_tacworkers view.next id x)
           ), cache, true
@@ -2406,39 +2409,39 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
             resilient_tactic id cblock (fun () ->
               reach view.next;
               (* State resulting from reach *)
-              let st = Vernacstate.freeze_interp_state `No in
+              let st = Vernacstate.freeze_interp_state ~marshallable:false in
               ignore(stm_vernac_interp id st x)
             );
 	    if eff then update_global_env ()
-          ), (if eff then `Yes else cache), true
+          ), eff || cache, true
       | `Cmd { cast = x; ceff = eff } -> (fun () ->
           (match !cur_opt.async_proofs_mode with
            | APon | APonLazy ->
              resilient_command reach view.next
            | APoff -> reach view.next);
-          let st = Vernacstate.freeze_interp_state `No in
+          let st = Vernacstate.freeze_interp_state ~marshallable:false in
           ignore(stm_vernac_interp id st x);
           if eff then update_global_env ()
-        ), (if eff then `Yes else cache), true
+        ), eff || cache, true
       | `Fork ((x,_,_,_), None) -> (fun () ->
             resilient_command reach view.next;
-            let st = Vernacstate.freeze_interp_state `No in
+            let st = Vernacstate.freeze_interp_state ~marshallable:false in
             ignore(stm_vernac_interp id st x);
             wall_clock_last_fork := Unix.gettimeofday ()
-          ), `Yes, true
+          ), true, true
       | `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *)
-            reach ~cache:`Shallow prev;
+            reach ~cache:true prev;
             reach view.next;
 
             (try
-               let st = Vernacstate.freeze_interp_state `No in
+               let st = Vernacstate.freeze_interp_state ~marshallable:false in
                ignore(stm_vernac_interp id st x);
             with e when CErrors.noncritical e ->
               let (e, info) = CErrors.push e in
               let info = Stateid.add info ~valid:prev id in
               Exninfo.iraise (e, info));
             wall_clock_last_fork := Unix.gettimeofday ()
-          ), `Yes, true
+          ), true, true
       | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) ->
           let rec aux = function
             | `ASync (block_start, nodes, name, delegate) -> (fun () ->
@@ -2468,7 +2471,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                     State.install_cached id
                 | { VCS.kind = `Proof _ }, Some _ -> assert false
                 | { VCS.kind = `Proof _ }, None ->
-                    reach ~cache:`Shallow block_start;
+                    reach ~cache:true block_start;
                     let fp, cancel =
                       if delegate then
                         Slaves.build_proof ~doc
@@ -2487,19 +2490,19 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                       Proof_global.close_future_proof ~opaque ~feedback_id:id fp in
                     if not delegate then ignore(Future.compute fp);
                     reach view.next;
-                    let st = Vernacstate.freeze_interp_state `No in
+                    let st = Vernacstate.freeze_interp_state ~marshallable:false in
                     ignore(stm_vernac_interp id ~proof st x);
                     feedback ~id:id Incomplete
                 | { VCS.kind = `Master }, _ -> assert false
                 end;
                 Proof_global.discard_all ()
-              ), (if redefine_qed then `No else `Yes), true
+              ), not redefine_qed, true
           | `Sync (name, `Immediate) -> (fun () ->
                 reach eop;
-                let st = Vernacstate.freeze_interp_state `No in
+                let st = Vernacstate.freeze_interp_state ~marshallable:false in
                 ignore(stm_vernac_interp id st x);
                 Proof_global.discard_all ()
-              ), `Yes, true
+              ), true, true
           | `Sync (name, reason) -> (fun () ->
                 log_processing_sync id name reason;
                 reach eop;
@@ -2523,25 +2526,25 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                 if keep <> VtKeep VtKeepAxiom then
                   reach view.next;
                 let wall_clock2 = Unix.gettimeofday () in
-                let st = Vernacstate.freeze_interp_state `No in
+                let st = Vernacstate.freeze_interp_state ~marshallable:false in
                 ignore(stm_vernac_interp id ?proof st x);
                 let wall_clock3 = Unix.gettimeofday () in
                 Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time"
                   (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2));
                 Proof_global.discard_all ()
-              ), `Yes, true
+              ), true, true
           | `MaybeASync (start, nodes, name, delegate) -> (fun () ->
-                reach ~cache:`Shallow start;
+                reach ~cache:true start;
                 (* no sections *)
                 if CList.is_empty (Environ.named_context (Global.env ()))
                 then Util.pi1 (aux (`ASync (start, nodes, name, delegate))) ()
                 else Util.pi1 (aux (`Sync (name, `NoPU_NoHint_NoES))) ()
-              ), (if redefine_qed then `No else `Yes), true
+              ), not redefine_qed, true
           in
           aux (collect_proof keep (view.next, x) brname brinfo eop)
       | `Sideff (ReplayCommand x,_) -> (fun () ->
             reach view.next;
-            let st = Vernacstate.freeze_interp_state `No in
+            let st = Vernacstate.freeze_interp_state ~marshallable:false in
             ignore(stm_vernac_interp id st x);
             update_global_env ()
           ), cache, true
@@ -2551,8 +2554,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
           ), cache, true
     in
     let cache_step =
-      if !cur_opt.async_proofs_cache = Some Force then `Yes
-      else cache_step in
+      !cur_opt.async_proofs_cache = Some Force || cache_step
+    in
     State.define ~doc ?safe_id
       ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id;
     stm_prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
@@ -2671,7 +2674,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
   load_objs require_libs;
 
   (* We record the state at this point! *)
-  State.define ~doc ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial;
+  State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial;
   Backtrack.record ();
   Slaves.init ();
   if async_proofs_is_master !cur_opt then begin
@@ -2785,7 +2788,7 @@ let merge_proof_branch ~valid ?id qast keep brname =
       VCS.rewrite_merge qed_id ~ours:(Qed (qed ofp)) ~at:master_id brname;
       VCS.delete_branch brname;
       VCS.gc ();
-      let _st : unit = Reach.known_state ~doc:dummy_doc (* XXX should be taken in input *) ~redefine_qed:true ~cache:`No qed_id in
+      let _st : unit = Reach.known_state ~doc:dummy_doc (* XXX should be taken in input *) ~redefine_qed:true ~cache:false qed_id in
       VCS.checkout VCS.Branch.master;
       `Unfocus qed_id
   | { VCS.kind = `Master } ->
@@ -2957,12 +2960,12 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
           let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
           let id = VCS.new_node ~id:newtip () in
           let head_id = VCS.get_branch_pos head in
-          let _st : unit = Reach.known_state ~doc ~cache:`Yes head_id in (* ensure it is ok *)
+          let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *)
           let step () =
             VCS.checkout VCS.Branch.master;
             let mid = VCS.get_branch_pos VCS.Branch.master in
             let _st' : unit = Reach.known_state ~doc ~cache:(VCS.is_interactive ()) mid in
-            let st = Vernacstate.freeze_interp_state `No in
+            let st = Vernacstate.freeze_interp_state ~marshallable:false in
             ignore(stm_vernac_interp id st x);
             (* Vernac x may or may not start a proof *)
             if not in_proof && Proof_global.there_are_pending_proofs () then
@@ -2987,7 +2990,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
               end;
               VCS.checkout_shallowest_proof_branch ();
             end in
-          State.define ~doc ~safe_id:head_id ~cache:`Yes step id;
+          State.define ~doc ~safe_id:head_id ~cache:true step id;
           Backtrack.record (); `Ok
 
       | VtUnknown, VtLater ->
@@ -3116,7 +3119,7 @@ type focus = {
 let query ~doc ~at ~route s =
   stm_purify (fun s ->
     if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc)
-    else Reach.known_state ~doc ~cache:`Yes at;
+    else Reach.known_state ~doc ~cache:true at;
     try
       while true do
         let { CAst.loc; v=ast } = parse_sentence ~doc at s in
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