STM: states coming from workers have no proof terminators (Close #4246)

Hence we reuse the ones in master.

4 files changed, 32 insertions, 3 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 50a68952e..8677b854d 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -665,4 +665,7 @@ let freeze ~marshallable =
   | `No -> !pstates
 let unfreeze s = pstates := s; update_proof_mode ()
 let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof
+let copy_terminators ~src ~tgt =
+  assert(List.length src = List.length tgt);
+  List.map2 (fun op p -> { p with terminator = op.terminator }) src tgt
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 6a5116a9e..88e047782 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -197,3 +197,4 @@ type state
 val freeze : marshallable:[`Yes | `No | `Shallow] -> state
 val unfreeze : state -> unit
 val proof_of_state : state -> Proof.proof
+val copy_terminators : src:state -> tgt:state -> state
diff --git a/stm/stm.ml b/stm/stm.ml
index a6b21bcd9..373fd0ba3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -671,11 +671,22 @@ end = struct (* {{{ *)
   let assign id what =
     if VCS.get_state id <> None then () else
     try match what with
-    | `Full s -> VCS.set_state id s
+    | `Full s ->
+         let s =
+           try
+            let prev = (VCS.visit id).next in
+            if is_cached prev
+            then { s with proof = 
+              Proof_global.copy_terminators
+                ~src:(get_cached prev).proof ~tgt:s.proof }
+            else s
+           with VCS.Expired -> s in
+         VCS.set_state id s
     | `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 proof =
+             Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in
            let s = { s with system =
              States.replace_summary s.system
                (Summary.surgery_summary
@@ -1119,7 +1130,7 @@ end = struct (* {{{ *)
         when is_tac expr && State.same_env o n -> (* A pure tactic *)
           Some (id, `Proof (prev, State.proof_part_of_frozen n))
       | Some _, Some s ->
-          msg_warning (str "Sending back a fat state");
+          msg_warning (str "STM: sending back a fat state");
           Some (id, `Full s)
       | _, Some s -> Some (id, `Full s) in
     let rec aux seen = function
diff --git a/test-suite/ide/bug4246.fake b/test-suite/ide/bug4246.fake
new file mode 100644
index 000000000..16b552f67
--- /dev/null
+++ b/test-suite/ide/bug4246.fake
@@ -0,0 +1,14 @@
+# first proof
+ADD { Lemma a : True. }
+ADD { Proof using. }
+ADD here { trivial. } # first error
+ADD { fail. }
+ADD { Qed. }
+WAIT
+EDIT_AT here
+# Fixing the proof
+ADD { Qed. }
+WAIT
+EDIT_AT here
+ADD { Qed. }
+JOIN