[declare] Remove some unused `fix_exn`

In the current proof save path, the kernel can raise an exception when
checking a proof wrapped into a future.

However, in this case, the future itself will "fix" the produced
exception, with the mandatory handler set at the future's creation
time.

Thus, there is no need for the declare layer to mess with exceptions
anymore, if my logic is correct. Note that the `fix_exn` parameter to
the `Declare` API was not used anymore.

This undoes 77cf18eb844b45776b2ec67be9f71e8dd4ca002c which comes from
pre-github times, so unfortunately I didn't have access to the
discussion.

We need to be careful in `perform_buildp` as to catch the `Qed` error
and properly notify the STM about it with `State.exn_on`; this was
previously done by the declare layer using a hack [grabbing internal
state of the future, that the future itself was not using as it was
already forced], but we now do it in the caller in a more principled
way.

This has been tested in the case that tactics succeed but Qed fails
asynchronously.

1 files changed, 15 insertions, 14 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 04f08e488b..183e8b9912 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,7 @@ end = struct (* {{{ *)
         feedback (InProgress ~-1)
 
   let build_proof_here ~doc ?loc ~drop_pt (id,valid) eop =
-    Future.create (State.exn_on id ~valid) (fun () ->
+    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
@@ -1517,7 +1510,6 @@ end = struct (* {{{ *)
       (* 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
@@ -1527,12 +1519,22 @@ end = struct (* {{{ *)
              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 p) 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
+          try
+            stm_qed_delay_proof ~st ~id:stop
+              ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None))
+          with exn ->
+            (* If [stm_qed_delay_proof] fails above we need to use the
+               exn callback in the same way than build_proof_here;
+               this is actually wronly named fix_exn as it does _way_
+               more than just modifying exn info *)
+            let iexn = Exninfo.capture exn in
+            let iexn = State.exn_on (fst exn_info) ~valid:(snd exn_info) iexn in
+            Exninfo.iraise iexn)
+        in
         ignore(Future.join checked_proof);
       end;
       (* STATE: Restore the state XXX: handle exn *)
@@ -1540,7 +1542,7 @@ end = struct (* {{{ *)
       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 ()