From 0e2897d33a7c07236a34b6ba3a7bb1bc6bb4bb65 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 15 May 2020 03:14:15 +0200
Subject: [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.
---
 lib/future.ml  | 14 ++++++--------
 lib/future.mli | 16 +++-------------
 2 files changed, 9 insertions(+), 21 deletions(-)

(limited to 'lib')

diff --git a/lib/future.ml b/lib/future.ml
index 661637fcd1..23d089fb6b 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -67,8 +67,8 @@ and 'a computation = 'a comput ref
 
 let unnamed = "unnamed"
 
-let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x =
-  ref (Ongoing (name, CEphemeron.create (uuid, f, ref x)))
+let create ?(name=unnamed) ?(uuid=UUID.fresh ()) ~fix_exn x =
+  ref (Ongoing (name, CEphemeron.create (uuid, fix_exn, ref x)))
 let get x =
   match !x with
   | Finished v -> unnamed, UUID.invalid, id, ref (Val v)
@@ -97,9 +97,7 @@ let peek_val kx = let _, _, _, x = get kx in match !x with
 
 let uuid kx = let _, id, _, _ = get kx in id
 
-let from_val ?(fix_exn=id) v = create fix_exn (Val v)
-
-let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn
+let from_val v = create ~fix_exn:id (Val v)
 
 let create_delegate ?(blocking=true) ~name fix_exn =
   let assignment signal ck = fun v ->
@@ -116,7 +114,7 @@ let create_delegate ?(blocking=true) ~name fix_exn =
     let cond = Condition.create () in
     (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock),
     (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in
-  let ck = create ~name fix_exn (Delegated wait) in
+  let ck = create ~name ~fix_exn (Delegated wait) in
   ck, assignment signal ck
 
 (* TODO: get rid of try/catch to be stackless *)
@@ -143,12 +141,12 @@ let force x = match compute x with
 
 let chain ck f =
   let name, uuid, fix_exn, c = get ck in
-  create ~uuid ~name fix_exn (match !c with
+  create ~uuid ~name ~fix_exn (match !c with
   | Closure _ | Delegated _ -> Closure (fun () -> f (force ck))
   | Exn _ as x -> x
   | Val v -> Val (f v))
 
-let create fix_exn f = create fix_exn (Closure f)
+let create ~fix_exn f = create ~fix_exn (Closure f)
 
 let replace kx y =
   let _, _, _, x = get kx in
diff --git a/lib/future.mli b/lib/future.mli
index 7a85c37970..612a67f962 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -47,21 +47,11 @@ type fix_exn = Exninfo.iexn -> Exninfo.iexn
    by forcing the computations or any computation that is chained after
    it. It is used by STM to attach errors to their corresponding states,
    and to communicate to the code catching the exception a valid state id. *)
-val create : fix_exn -> (unit -> 'a) -> 'a computation
+val create : fix_exn:fix_exn -> (unit -> 'a) -> 'a computation
 
 (* Usually from_val is used to create "fake" futures, to use the same API
-   as if a real asynchronous computations was there.  In this case fixing
-   the exception is not needed, but *if* the future is chained, the fix_exn
-   argument should really be given *)
-val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation
-
-(* To get the fix_exn of a computation and build a Lemmas.declaration_hook.
- * When a future enters the environment a corresponding hook is run to perform
- * some work.  If this fails, then its failure has to be annotated with the
- * same state id that corresponds to the future computation end.  I.e. Qed
- * is split into two parts, the lazy one (the future) and the eager one
- * (the hook), both performing some computations for the same state id. *)
-val fix_exn_of : 'a computation -> fix_exn
+   as if a real asynchronous computations was there. *)
+val from_val : 'a -> 'a computation
 
 (* Run remotely, returns the function to assign.
    If not blocking (the default) it raises NotReady if forced before the
-- 
cgit v1.2.3