From 980431c745997587a9463ead5bdf849e872ce1ad Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 12 Dec 2018 12:53:19 +0100
Subject: [stm] join the tip of the document even when fixing a proof (fix
 #9204)

---
 stm/stm.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index e835bdcb1e..61b8140ae6 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2715,7 +2715,7 @@ let finish ~doc =
   ); doc
 
 let wait ~doc =
-  let doc = finish ~doc in
+  let doc = observe ~doc (VCS.get_branch_pos VCS.Branch.master) in
   Slaves.wait_all_done ();
   VCS.print ();
   doc
@@ -2734,7 +2734,7 @@ let join ~doc =
   stm_prerr_endline (fun () -> "Joining the environment");
   Global.join_safe_environment ();
   stm_prerr_endline (fun () -> "Joining Admitted proofs");
-  join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ()));
+  join_admitted_proofs (VCS.get_branch_pos VCS.Branch.master);
   VCS.print ();
   doc
 
-- 
cgit v1.2.3


From 4838146ee993a3bafb6a359dff529aae815cfff6 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 13 Dec 2018 10:10:45 +0100
Subject: [stm] join: check no error states are part of the document

The error-resiliency feature may have managed to reach the end
of the document by recovering some error
---
 stm/stm.ml | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 61b8140ae6..5e453ecfe6 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2729,12 +2729,29 @@ let rec join_admitted_proofs id =
        join_admitted_proofs view.next
   | _ -> join_admitted_proofs view.next
 
+(* Error resiliency may have tolerated some broken commands *)
+let rec check_no_err_states ~doc visited id =
+  let open Stateid in
+  if Set.mem id visited then visited else
+  match state_of_id ~doc id with
+  | `Error e -> raise e
+  | _ ->
+     let view = VCS.visit id in
+     match view.step with
+     | `Qed(_,id) ->
+         let visited = check_no_err_states ~doc (Set.add id visited) id in
+         check_no_err_states ~doc visited view.next
+     | _ -> check_no_err_states ~doc (Set.add id visited) view.next
+
 let join ~doc =
   let doc = wait ~doc in
   stm_prerr_endline (fun () -> "Joining the environment");
   Global.join_safe_environment ();
   stm_prerr_endline (fun () -> "Joining Admitted proofs");
   join_admitted_proofs (VCS.get_branch_pos VCS.Branch.master);
+  stm_prerr_endline (fun () -> "Checking no error states");
+  ignore(check_no_err_states ~doc (Stateid.Set.singleton Stateid.initial)
+    (VCS.get_branch_pos VCS.Branch.master));
   VCS.print ();
   doc
 
-- 
cgit v1.2.3