STM: make ~valid state id non optional from APIs

It used to be Stateid.initial by default.  That is indeed a valid
state id but very likely not the very best one (that would be
the tip of the document).

3 files changed, 12 insertions, 12 deletions

diff --git a/lib/stateid.ml b/lib/stateid.ml
index 500581a39..ae25735c5 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -22,7 +22,7 @@ let to_int id = id
 let newer_than id1 id2 = id1 > id2
 
 let state_id_info : (t * t) Exninfo.t = Exninfo.make ()
-let add exn ?(valid = initial) id =
+let add exn ~valid id =
   Exninfo.add exn state_id_info (valid, id)
 let get exn = Exninfo.get exn state_id_info
 
diff --git a/lib/stateid.mli b/lib/stateid.mli
index cd8fddf0c..1d87a343b 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -26,9 +26,8 @@ val newer_than : t -> t -> bool
 
 (* Attaches to an exception the concerned state id, plus an optional
  * state id that is a valid state id before the error.
- * Backtracking to the valid id is safe.
- * The initial_state_id is assumed to be safe. *)
-val add : Exninfo.info -> ?valid:t -> t -> Exninfo.info
+ * Backtracking to the valid id is safe. *)
+val add : Exninfo.info -> valid:t -> t -> Exninfo.info
 val get : Exninfo.info -> (t * t) option
 
 type ('a,'b) request = {
diff --git a/stm/stm.ml b/stm/stm.ml
index 32185247f..e387e6322 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -746,7 +746,7 @@ module State : sig
   val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool
 
 
-  val exn_on : Stateid.t -> ?valid:Stateid.t -> iexn -> iexn
+  val exn_on : Stateid.t -> valid:Stateid.t -> iexn -> iexn
   (* to send states across worker/master *)
   type frozen_state
   val get_cached : Stateid.t -> frozen_state
@@ -854,14 +854,14 @@ end = struct (* {{{ *)
            VCS.set_state id (Valid s)
     with VCS.Expired -> ()
 
-  let exn_on id ?valid (e, info) =
+  let exn_on id ~valid (e, info) =
     match Stateid.get info with
     | Some _ -> (e, info)
     | None ->
         let loc = Option.default Loc.ghost (Loc.get_loc info) in
         let (e, info) = Hooks.(call_process_error_once (e, info)) in
         Hooks.(call execution_error id loc (iprint (e, info)));
-        (e, Stateid.add info ?valid id)
+        (e, Stateid.add info ~valid id)
 
   let same_env { system = s1 } { system = s2 } =
     let s1 = States.summary_of_state s1 in
@@ -2354,7 +2354,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
     msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
     exit 1
 
-let merge_proof_branch ?valid ?id qast keep brname =
+let merge_proof_branch ~valid ?id qast keep brname =
   let brinfo = VCS.get_branch brname in
   let qed fproof = { qast; keep; brname; brinfo; fproof } in
   match brinfo with
@@ -2377,7 +2377,7 @@ let merge_proof_branch ?valid ?id qast keep brname =
       VCS.checkout VCS.Branch.master;
       `Unfocus qed_id
   | { VCS.kind = `Master } ->
-       iraise (State.exn_on ?valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null))
+       iraise (State.exn_on ~valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null))
 
 (* When tty is true, this code also does some of the job of the user interface:
    jump back to a state that is valid *)
@@ -2446,9 +2446,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
       | VtStm (VtBack oid, true), w ->
           let id = VCS.new_node ~id:newtip () in
           let { mine; others } = Backtrack.branches_of oid in
+          let valid = VCS.get_branch_pos head in
           List.iter (fun branch ->
             if not (List.mem_assoc branch (mine::others)) then
-              ignore(merge_proof_branch x VtDrop branch))
+              ignore(merge_proof_branch ~valid x VtDrop branch))
             (VCS.branches ());
           VCS.checkout_shallowest_proof_branch ();
           let head = VCS.current_branch () in
@@ -2543,8 +2544,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
           detect_proof_block id cblock; *)
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtQed keep, w ->
-          let valid = if tty then Some(VCS.get_branch_pos head) else None in
-          let rc = merge_proof_branch ?valid ~id:newtip x keep head in
+          let valid = VCS.get_branch_pos head in
+          let rc = merge_proof_branch ~valid ~id:newtip x keep head in
           VCS.checkout_shallowest_proof_branch ();
           Backtrack.record (); if w == VtNow then finish ();
           rc