STM: proof state also includes meta counters

Workers send back incomplete system states (only the proof part).
Such part must include the meta/evar counter.

5 files changed, 39 insertions, 10 deletions

diff --git a/library/states.ml b/library/states.ml
index a1c2a095d..96a487b16 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -12,6 +12,7 @@ open System
 type state = Lib.frozen * Summary.frozen
 
 let summary_of_state = snd
+let replace_summary (lib,_) s = lib, s
 
 let freeze ~marshallable =
   (Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable)
diff --git a/library/states.mli b/library/states.mli
index 66de14909..4d5d63e03 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -21,6 +21,7 @@ val freeze : marshallable:Summary.marshallable -> state
 val unfreeze : state -> unit
 
 val summary_of_state : state -> Summary.frozen
+val replace_summary : state -> Summary.frozen -> state
 
 (** {6 Rollback } *)
 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 0b8cbff36..201a16ebe 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -212,9 +212,11 @@ let whd_head_evar sigma c =
 (* Creating new metas *)
 (**********************)
 
+let meta_counter_summary_name = "meta counter"
+
 (* Generator of metavariables *)
 let new_meta =
-  let meta_ctr = Summary.ref 0 ~name:"meta counter" in
+  let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in
   fun () -> incr meta_ctr; !meta_ctr
 
 let mk_new_meta () = mkMeta(new_meta())
@@ -241,9 +243,11 @@ let make_pure_subst evi args =
 (* Creating new evars *)
 (**********************)
 
+let evar_counter_summary_name = "evar counter"
+
 (* Generator of existential names *)
 let new_untyped_evar =
-  let evar_ctr = Summary.ref 0 ~name:"evar counter" in
+  let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in
   fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr
 
 (*------------------------------------*
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 92a3984ba..49036798e 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -243,3 +243,6 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b ->
 
 val subterm_source : existential_key -> Evar_kinds.t Loc.located ->
   Evar_kinds.t Loc.located
+
+val meta_counter_summary_name : string
+val evar_counter_summary_name : string
diff --git a/stm/stm.ml b/stm/stm.ml
index a4db934b2..5edf48044 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -161,6 +161,11 @@ type step =
   | `Alias  of alias_t ]
 type visit = { step : step; next : Stateid.t }
 
+
+(* Parts of the system state that are morally part of the proof state *)
+let summary_pstate = [ Evarutil.meta_counter_summary_name;
+                       Evarutil.evar_counter_summary_name;
+                       "program-tcc-table" ]
 type state = {
   system : States.state;
   proof : Proof_global.state;
@@ -594,9 +599,12 @@ module State : sig
   type frozen_state
   val get_cached : Stateid.t -> frozen_state
   val same_env : frozen_state -> frozen_state -> bool
+
+  type proof_part
   type partial_state =
-    [ `Full of frozen_state | `Proof of Stateid.t * Proof_global.state ]
-  val proof_part_of_frozen : frozen_state -> Proof_global.state
+    [ `Full of frozen_state
+    | `Proof of Stateid.t * proof_part ]
+  val proof_part_of_frozen : frozen_state -> proof_part
   val assign : Stateid.t -> partial_state -> unit
 
 end = struct (* {{{ *)
@@ -620,9 +628,14 @@ end = struct (* {{{ *)
     (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i)
   
   type frozen_state = state
+  type proof_part =
+    Proof_global.state * Summary.frozen_bits (* only meta counters *)
   type partial_state =
-    [ `Full of frozen_state | `Proof of Stateid.t * Proof_global.state ]
-  let proof_part_of_frozen { proof } = proof
+    [ `Full of frozen_state
+    | `Proof of Stateid.t * proof_part ]
+  let proof_part_of_frozen { proof; system } =
+    proof,
+    Summary.project_summary (States.summary_of_state system) summary_pstate
 
   let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable)
 
@@ -657,9 +670,16 @@ end = struct (* {{{ *)
     if VCS.get_state id <> None then () else
     try match what with
     | `Full s -> VCS.set_state id s
-    | `Proof(ontop,p) ->
-         if is_cached ontop then (
-           VCS.set_state id { (get_cached ontop) with proof = p })
+    | `Proof(ontop,(pstate,counters)) ->
+         if is_cached ontop then
+           let s = get_cached ontop in
+           let s = { s with proof = pstate } in
+           let s = { s with system =
+             States.replace_summary s.system
+               (Summary.surgery_summary
+                 (States.summary_of_state s.system)
+               counters) } in
+           VCS.set_state id s
     with VCS.Expired -> ()
 
   let exn_on id ?valid (e, info) =
@@ -1555,7 +1575,7 @@ and Reach : sig
 
 end = struct (* {{{ *)
 
-let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
+let pstate = summary_pstate
 
 let async_policy () =
   let open Flags in