Merge PR #12357: [declare] Remove some unused `fix_exn`

Reviewed-by: gares

1 files changed, 23 insertions, 22 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 04f08e488b..b72cee7a9d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -830,8 +830,6 @@ module State : sig
     ?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 install_parsing_state : Stateid.t -> unit *)
   val is_cached : ?cache:bool -> Stateid.t -> bool
@@ -865,8 +863,6 @@ end = struct (* {{{ *)
   (* cur_id holds Stateid.dummy in case the last attempt to define a state
    * failed, so the global state may contain garbage *)
   let cur_id = ref Stateid.dummy
-  let fix_exn_ref = ref (fun x -> x)
-
   let freeze () = { id = !cur_id; vernac_state = Vernacstate.freeze_interp_state ~marshallable:false }
   let unfreeze st =
     Vernacstate.unfreeze_interp_state st.vernac_state;
@@ -1001,10 +997,7 @@ end = struct (* {{{ *)
     try
       stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^
         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 then cache_state ~marshallable:false id;
       stm_prerr_endline (fun () -> "setting cur id to "^str_id);
       cur_id := id;
@@ -1495,7 +1488,9 @@ end = struct (* {{{ *)
         feedback (InProgress ~-1)
 
   let build_proof_here ~doc ?loc ~drop_pt (id,valid) eop =
-    Future.create (State.exn_on id ~valid) (fun () ->
+    (* [~fix_exn:exn_on] here does more than amending the exn
+       information, it also updates the STM state *)
+    Future.create ~fix_exn:(State.exn_on id ~valid) (fun () ->
       let wall_clock1 = Unix.gettimeofday () in
       Reach.known_state ~doc ~cache:(VCS.is_interactive ()) eop;
       let wall_clock2 = Unix.gettimeofday () in
@@ -1509,38 +1504,45 @@ end = struct (* {{{ *)
     try
       VCS.restore document;
       VCS.print ();
-      let proof, future_proof, time =
+      let proof, time =
         let wall_clock = Unix.gettimeofday () in
         let fp = build_proof_here ~doc:dummy_doc (* XXX should be document *) ?loc ~drop_pt:drop exn_info stop in
         let proof = Future.force fp in
-        proof, fp, Unix.gettimeofday () -. wall_clock in
+        proof, Unix.gettimeofday () -. wall_clock in
       (* We typecheck the proof with the kernel (in the worker) to spot
        * the few errors tactics don't catch, like the "fix" tactic building
        * a bad fixpoint *)
-      let fix_exn = Future.fix_exn_of future_proof in
       (* STATE: We use the current installed imperative state *)
       let st = State.freeze () in
       if not drop then begin
-        let checked_proof = Future.chain future_proof (fun p ->
-
-          (* Unfortunately close_future_proof and friends are not pure so we need
-             to set the state manually here *)
+        (* Unfortunately close_future_proof and friends are not pure so we need
+           to set the state manually here *)
           State.unfreeze st;
           let pobject, _info =
-            PG_compat.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in
+            PG_compat.close_future_proof ~feedback_id:stop (Future.from_val proof) in
 
           let st = Vernacstate.freeze_interp_state ~marshallable:false in
           let opaque = Declare.Opaque in
-          stm_qed_delay_proof ~st ~id:stop
-            ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None))) in
-        ignore(Future.join checked_proof);
-      end;
+          try
+            let _pstate =
+              stm_qed_delay_proof ~st ~id:stop
+                ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None)) in
+            ()
+          with exn ->
+            (* If [stm_qed_delay_proof] fails above we need to use the
+               exn callback in the same way than build_proof_here;
+               actually [fix_exn] there does more more than just
+               modifying exn info, it also updates the STM state *)
+            let iexn = Exninfo.capture exn in
+            let iexn = State.exn_on (fst exn_info) ~valid:(snd exn_info) iexn in
+            Exninfo.iraise iexn
+        end;
       (* STATE: Restore the state XXX: handle exn *)
       State.unfreeze st;
       RespBuiltProof(proof,time)
     with
     | e when CErrors.noncritical e || e = Stack_overflow ->
-        let (e, info) = Exninfo.capture e in
+        let e, info = Exninfo.capture e in
         (* This can happen if the proof is broken.  The error has also been
          * signalled as a feedback, hence we can silently recover *)
         let e_error_at, e_safe_id = match Stateid.get info with
@@ -3310,7 +3312,6 @@ let unreachable_state_hook = Hooks.unreachable_state_hook
 let document_add_hook = Hooks.document_add_hook
 let document_edit_hook = Hooks.document_edit_hook
 let sentence_exec_hook = Hooks.sentence_exec_hook
-let () = Declare.Obls.stm_get_fix_exn := (fun () -> !State.fix_exn_ref)
 
 type document = VCS.vcs
 let backup () = VCS.backup ()