Future: ported to Ephemeron + exception enhancing

A future always carries a fix_exn with it: a function that enriches
an exception with the state in which the error occurs and also a safe
state close to it where one could backtrack.

A future can be in two states: Ongoing or Finished.
The latter state is obtained by Future.join and after that the future
can be safely marshalled.
An Ongoing future can be marshalled, but its value is lost.  This makes
it possible to send the environment to a slave process without
pre-processing it to drop all unfinished proofs (they are dropped
automatically in some sense).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16892 85f007b7-540e-0410-9357-904b9bb8a0f7

17 files changed, 121 insertions, 192 deletions

diff --git a/checker/values.ml b/checker/values.ml
index 55c6367a7..9a0d9922f 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -69,10 +69,8 @@ let v_map vk vd =
 let v_computation f =
   Annot ("Future.computation",
   v_ref
-    (v_sum "computation" 2
-      [| [| Fail "Closure" |];
-         [| f ; v_sum "option" 1 [| [| Fail "Val(_,Some _)" |] |] |];
-     [| Fail "Exn" |] |]))
+    (v_sum "Future.comput" 0
+      [| [| Fail "Ongoing" |]; [| f |] |]))
 
 (** kernel/names *)
 
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 4c2f22199..dbe83a856 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -126,7 +126,7 @@ let on_body f = function
   | Undef _ as x -> x
   | Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs)))
   | OpaqueDef lc ->
-    OpaqueDef (Future.chain ~id:"Cooking.on_body" ~pure:true lc (fun lc ->
+    OpaqueDef (Future.chain lc (fun lc ->
         (Lazyconstr.opaque_from_val (f (Lazyconstr.force_opaque lc)))))
 
 let constr_of_def = function
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 973859ede..3083c1738 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -52,8 +52,7 @@ let subst_const_type sub arity = match arity with
 let subst_const_def sub def = match def with
   | Undef _ -> def
   | Def c -> Def (subst_constr_subst sub c)
-  | OpaqueDef lc ->
-    OpaqueDef (Future.chain ~pure:true lc (subst_lazy_constr sub))
+  | OpaqueDef lc -> OpaqueDef (Future.chain lc (subst_lazy_constr sub))
 
 (* TODO : the native compiler seems to rely on a fresh (ref NotLinked)
    being created at each substitution. Quite ugly... For the moment,
@@ -100,7 +99,7 @@ let hcons_const_def = function
     Def (from_val (Term.hcons_constr constr))
   | OpaqueDef lc ->
     OpaqueDef
-      (Future.chain ~pure:true lc
+      (Future.chain lc
          (fun lc -> opaque_from_val (Term.hcons_constr (force_opaque lc))))
 
 let hcons_const_body cb =
@@ -242,17 +241,6 @@ let join_constant_body cb =
   | OpaqueDef d -> ignore(Future.join d)
   | _ -> ()
 
-let prune_constant_body cb =
-  let cst, cbo = cb.const_constraints, cb.const_body in
-  let cst' = Future.drop cst in
-  let cbo' = match cbo with
-    | OpaqueDef d ->
-        let d' = Future.drop d in
-        if d' == d then cbo else OpaqueDef d'
-    | _ -> cbo in
-  if cst' == cst && cbo' == cbo then cb
-  else {cb with const_constraints = cst'; const_body = cbo'}
-
 let string_of_side_effect = function
   | SEsubproof (c,_) -> Names.string_of_con c
   | SEscheme (cl,_) ->
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index f593b4547..177ae9d45 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -59,7 +59,6 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
 
 val join_constant_body : constant_body -> unit
-val prune_constant_body : constant_body -> constant_body
 
 (** {6 Hash-consing} *)
 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 76feb8498..6a0a952f7 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -592,7 +592,7 @@ let rec collect_mbid l sign =  match sign with
 let clean_bounded_mod_expr sign =
   if is_functor sign then collect_mbid MBIset.empty sign else sign
 
-(** {6 Stm machinery : join and prune } *)
+(** {6 Stm machinery } *)
 
 let rec join_module mb =
   implem_iter join_signature join_expression mb.mod_expr;
@@ -610,29 +610,3 @@ and join_structure struc = List.iter join_field struc
 and join_signature sign = functor_iter join_modtype join_structure sign
 and join_expression me = functor_iter join_modtype (fun _ -> ()) me
 
-let rec prune_module mb =
-  let me, mta, mt = mb.mod_expr, mb.mod_type_alg, mb.mod_type in
-  let mt' = prune_signature mt in
-  let me' = implem_smartmap prune_signature prune_expression me in
-  let mta' = Option.smartmap prune_expression mta in
-  if me' == me && mta' == mta && mt' == mt then mb
-  else {mb with mod_expr = me'; mod_type_alg = mta'; mod_type = mt'}
-and prune_modtype mt =
-  let te, ta = mt.typ_expr, mt.typ_expr_alg in
-  let te' = prune_signature te in
-  let ta' = Option.smartmap prune_expression ta in
-  if te==te' && ta==ta' then mt else { mt with typ_expr=te'; typ_expr_alg=ta' }
-and prune_field (l,body as orig) = match body with
-  |SFBconst sb ->
-    let sb' = prune_constant_body sb in
-    if sb == sb' then orig else (l, SFBconst sb')
-  |SFBmind _ -> orig
-  |SFBmodule m ->
-    let m' = prune_module m in
-    if m == m' then orig else (l, SFBmodule m')
-  |SFBmodtype m ->
-    let m' = prune_modtype m in
-    if m == m' then orig else (l, SFBmodtype m')
-and prune_structure struc = List.smartmap prune_field struc
-and prune_signature sign = functor_smartmap prune_modtype prune_structure sign
-and prune_expression me = functor_smartmap prune_modtype (fun me -> me) me
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 6aed95988..11eb876ad 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -76,13 +76,11 @@ val subst_modtype_and_resolver : module_type_body -> module_path ->
 
 val clean_bounded_mod_expr : module_signature -> module_signature
 
-(** {6 Stm machinery : join and prune } *)
+(** {6 Stm machinery } *)
 
 val join_module : module_body -> unit
 val join_structure : structure_body -> unit
 
-val prune_structure : structure_body -> structure_body
-
 (** {6 Errors } *)
 
 type signature_mismatch_error =
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 57e44a322..90d52572a 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -197,28 +197,6 @@ let join_safe_environment e =
     (fun e fc -> add_constraints (Now (Future.join fc)) e)
     {e with future_cst = []} e.future_cst
 
-(* TODO : out of place and maybe incomplete w.r.t. modules *)
-(* this is there to explore the opaque pre-env structure but is
- * not part of the trusted code base *)
-let prune_env env =
-  let open Pre_env in
-  let prune_ckey (cb,k) = Declareops.prune_constant_body cb, k in
-  let prune_globals glob =
-    { glob with env_constants = Cmap_env.map prune_ckey glob.env_constants }
-  in
-  let env = Environ.pre_env env in
-  Environ.env_of_pre_env {env with
-    env_globals = prune_globals env.env_globals;
-    env_named_vals = [];
-    env_rel_val = []}
-let prune_safe_environment e =
-  { e with
-    modvariant = (match e.modvariant with LIBRARY -> LIBRARY | _ -> NONE);
-    revstruct = Modops.prune_structure e.revstruct;
-    future_cst = [];
-    env = prune_env e.env }
-
-
 (** {6 Various checks } *)
 
 let exists_modlabel l senv = Label.Set.mem l senv.modlabels
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index a56bb8578..b16d5b63d 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -43,8 +43,6 @@ val is_curmod_library : safe_environment -> bool
 (* safe_environment has functional data affected by lazy computations,
  * thus this function returns a new safe_environment *)
 val join_safe_environment : safe_environment -> safe_environment
-(* future computations are just dropped by this function *)
-val prune_safe_environment : safe_environment -> safe_environment
 
 (** {6 Enriching a safe environment } *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 567511c93..987621619 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -84,9 +84,8 @@ let infer_declaration ?(what="UNKNOWN") env dcl =
   | DefinitionEntry c ->
       let ctx, entry_body = c.const_entry_secctx, c.const_entry_body in
       if c.const_entry_opaque && not (Option.is_empty c.const_entry_type) then
-        let id = "infer_declaration " ^ what in
         let body_cst =
-          Future.chain ~id entry_body (fun (body, side_eff) ->
+          Future.chain entry_body (fun (body, side_eff) ->
             let body = handle_side_effects env body side_eff in
             let j, cst = infer env body in
             let j =
@@ -163,7 +162,7 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
-            OpaqueDef (Future.chain ~id:(string_of_con kn) lc (fun lc ->
+            OpaqueDef (Future.chain lc (fun lc ->
               let ids_typ = global_vars_set_constant_type env typ in
               let ids_def =
                 global_vars_set env (Lazyconstr.force_opaque lc) in
@@ -198,7 +197,7 @@ let translate_local_def env id centry =
 let translate_mind env kn mie = Indtypes.check_inductive env kn mie
 
 let handle_side_effects env ce = { ce with
-  const_entry_body = Future.chain ~id:"handle_side_effects" 
+  const_entry_body = Future.chain
     ce.const_entry_body (fun (body, side_eff) ->
-    handle_side_effects env body side_eff, Declareops.no_seff);
+       handle_side_effects env body side_eff, Declareops.no_seff);
 }
diff --git a/lib/future.ml b/lib/future.ml
index c1fb176df..b93d33640 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* to avoid side effects *)
+(* To deal with side effects we have to save/restore the system state *)
 let freeze = ref (fun () -> assert false : unit -> Dyn.t)
 let unfreeze = ref (fun _ -> () : Dyn.t -> unit)
 let set_freeze f g = freeze := f; unfreeze := g
@@ -26,59 +26,73 @@ let _ = Errors.register_handler (function
                 "asynchronous script processing.")
   | _ -> raise Errors.Unhandled)
 
+type fix_exn = exn -> exn
+let id x = prerr_endline "no fix_exn"; x
+
 (* Val is not necessarily a final state, so the
    computation restarts from the state stocked into Val *)
 type 'a comp =
   | Delegated
-  | Dropped
+      (* TODO in some cases one would like to block, sock here
+         a mutex and a condition to make this possible *)
   | Closure of (unit -> 'a)
   | Val of 'a * Dyn.t option
   | Exn of exn
+      (* Invariant: this exception is always "fixed" as in fix_exn *)
+
+type 'a comput =
+  | Ongoing of (fix_exn * 'a comp ref) Ephemeron.key
+  | Finished of 'a
 
-type 'a computation = 'a comp ref
+type 'a computation = 'a comput ref
+
+let create f x = ref (Ongoing (Ephemeron.create (f, Pervasives.ref x)))
+let get x =
+  match !x with
+  | Finished v -> (fun x -> x), ref( Val (v,None))
+  | Ongoing x ->
+      try Ephemeron.get x
+      with Ephemeron.InvalidKey -> (fun x -> x), ref (Exn NotHere)
 
 type 'a value = [ `Val of 'a | `Exn of exn ]
 
-let is_over x = match !x with
+let is_over kx = let _, x = get kx in match !x with
   | Val _ | Exn _ -> true
-  | Closure _ | Delegated | Dropped -> false
+  | Closure _ | Delegated -> false
 
-let is_val x = match !x with
+let is_val kx = let _, x = get kx in match !x with
   | Val _ -> true
-  | Exn _ | Closure _ | Delegated | Dropped -> false
+  | Exn _ | Closure _ | Delegated -> false
 
-let is_exn x = match !x with
+let is_exn kx = let _, x = get kx in match !x with
   | Exn _ -> true
-  | Val _ | Closure _ | Delegated | Dropped -> false
+  | Val _ | Closure _ | Delegated -> false
 
-let peek_val x = match !x with
+let peek_val kx = let _, x = get kx in match !x with
   | Val (v, _) -> Some v
-  | Exn _ | Closure _ | Delegated | Dropped -> None
-
-let from_val v = ref (Val (v, None))
-let from_here v = ref (Val (v, Some (!freeze ())))
-let proj = function
-  | `Val (x, _ ) -> `Val x
-  | `Exn e -> `Exn e
+  | Exn _ | Closure _ | Delegated -> None
 
-let create f = ref (Closure f)
+let from_val ?(fix_exn=id) v = create fix_exn (Val (v, None))
+let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ())))
 
 type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation]
-let create_delegate () =
-  let c = ref Delegated in
-  c, (fun v ->
-      assert (!c == Delegated);
-      match v with
-      | `Val v -> c := Val (v, None)
-      | `Exn e -> c := Exn e
-      | `Comp f -> c := !f)
-
-(* TODO: get rid of try/catch *)
-let compute ~pure c : 'a value = match !c with
+let create_delegate fix_exn =
+  let ck = create fix_exn Delegated in
+  ck, fun v ->
+        let fix_exn, c = get ck in
+        assert (!c == Delegated);
+        match v with
+        | `Val v -> c := Val (v, None)
+        | `Exn e -> c := Exn (fix_exn e)
+        | `Comp f -> let _, comp = get f in c := !comp
+
+(* TODO: get rid of try/catch to be stackless *)
+let compute ~pure ck : 'a value =
+  let fix_exn, c = get ck in
+  match !c with
   | Val (x, _) -> `Val x
   | Exn e -> `Exn e
   | Delegated -> `Exn NotReady
-  | Dropped -> `Exn NotHere
   | Closure f ->
       try
         let data = f () in
@@ -86,6 +100,7 @@ let compute ~pure c : 'a value = match !c with
         c := Val (data, state); `Val data
       with e ->
         let e = Errors.push e in
+        let e = fix_exn e in
         match e with
         | NotReady -> `Exn e
         | _ -> c := Exn e; `Exn e
@@ -94,20 +109,19 @@ let force ~pure x = match compute ~pure x with
   | `Val v -> v
   | `Exn e -> raise e
 
-let drop c = match !c with Closure _ | Val (_,Some _) -> ref Dropped | _ -> c
-
-let chain ?(id="none") ?(pure=false) c f = ref (match !c with
-  | Closure _ | Delegated | Dropped -> Closure (fun () -> f (force ~pure c))
+let chain ?(pure=false) ck f =
+  let fix_exn, c = get ck in
+  create fix_exn (match !c with
+  | Closure _ | Delegated -> Closure (fun () -> f (force ~pure ck))
   | Exn _ as x -> x
   | Val (v, None) -> Closure (fun () -> f v)
   | Val (v, Some _) when pure -> Closure (fun () -> f v)
-  | Val (v, Some state) ->
-(*        prerr_endline ("Future: restarting (check if optimizable): " ^ id); *)
-       Closure (fun () -> !unfreeze state; f v))
+  | Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v))
 
-let create_here f = chain ~pure:false (from_here ()) f
+let create fix_exn f = create fix_exn (Closure f)
 
-let replace x y =
+let replace kx y =
+  let _, x = get kx in
   match !x with
   | Exn _ -> x := Closure (fun () -> force ~pure:false y)
   | _ -> Errors.anomaly (Pp.str "Only Exn futures can be replaced")
@@ -125,19 +139,13 @@ let transactify f x =
   try f x
   with e -> let e = Errors.push e in !unfreeze state; raise e
 
-let purify_future f x =
-  match !x with
-  | Val _ | Exn _ | Delegated | Dropped -> f x
-  | Closure _ -> purify f x
-
+let purify_future f x = if is_over x then f x else purify f x
 let compute x = purify_future (compute ~pure:false) x
 let force x = purify_future (force ~pure:false) x
 
-let join x =
-  let v = force x in
-  (x := match !x with
-       | Val (x,_) -> Val (x, None)
-       | Exn _ | Delegated | Dropped | Closure _ -> assert false);
+let join kx =
+  let v = force kx in
+  kx := Finished v;
   v
 
 let split2 x =
@@ -156,3 +164,5 @@ let map2 f x l =
         with Failure _ | Invalid_argument _ ->
           Errors.anomaly (Pp.str "Future.map2 length mismatch")) in
     f xi y) 0 l
+
+let chain f g = chain f g
diff --git a/lib/future.mli b/lib/future.mli
index a1535b13d..4ba601976 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -6,48 +6,51 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Futures: for now lazy computations with some purity enforcing *)
-(* TODO: it may be worth separating in the type pure and inpure computations *)
+(* Futures: asynchronous computations with some purity enforcing *)
 
 exception NotReady
 
 type 'a computation
 type 'a value = [ `Val of 'a | `Exn of exn ]
+type fix_exn = exn -> exn
 
-(* Build a computation *)
-val create : (unit -> 'a) -> 'a computation
-val from_val : 'a -> 'a computation
+(* Build a computation.  fix_exn is used to enrich any exception raised
+   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
+
+(* 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
+
+(* Like from_val, but also takes a snapshot of the global state.  Morally
+   the value is not just the 'a but also the global system state *)
+val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation
 
 (* Run remotely, returns the function to assign *)
 type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation]
-val create_delegate : unit -> 'a computation * ('a assignement -> unit)
+val create_delegate : fix_exn -> 'a computation * ('a assignement -> unit)
 
 (* Given a computation that is_exn, replace it by another one *)
 val replace : 'a computation -> 'a computation -> unit
 
-(* Variants to stock a copy of the current environment *)
-val create_here : (unit -> 'a) -> 'a computation
-val from_here : 'a -> 'a computation
-
 (* Inspect a computation *)
 val is_over : 'a computation -> bool
 val is_val : 'a computation -> bool
 val is_exn : 'a computation -> bool
 val peek_val : 'a computation -> 'a option
 
-(* Chain computations.
-   Note that in [chain c f], f will execute in an environment modified by c
-   unless ~pure:true *)
-val chain :
-  ?id:string -> ?pure:bool -> 'a computation -> ('a -> 'b) -> 'b computation
+(* Chain computations.  *)
+val chain : 'a computation -> ('a -> 'b) -> 'b computation
 
 (* Forcing a computation *)
 val force : 'a computation -> 'a
 val compute : 'a computation -> 'a value
 
-val drop : 'a computation -> 'a computation
-
-(* Final call, no more impure chain allowed since the state is lost *)
+(* Final call, no more chain allowed since the state is lost *)
 val join : 'a computation -> 'a
 
 (* Utility *)
@@ -58,11 +61,14 @@ val map2 :
   ('a computation -> 'b -> 'c) ->
      'a list computation -> 'b list -> 'c list
 
-(* These functions are needed to get rid of side effects *)
-val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit
-
 (* Once set_freeze is called we can purify a computation *)
 val purify : ('a -> 'b) -> 'a -> 'b
 (* And also let a function alter the state but backtrack if it raises exn *)
 val transactify : ('a -> 'b) -> 'a -> 'b
 
+(* These functions are needed to get rid of side effects.
+   Thy are set for the outermos layer of the system, since they have to
+   deal with the whole system state. *)
+val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit
+
+
diff --git a/library/global.ml b/library/global.ml
index fd6cce46f..3b0e504d8 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -26,15 +26,12 @@ let global_env = ref Safe_typing.empty_environment
 let join_safe_environment () =
   global_env := Safe_typing.join_safe_environment !global_env
 
-let prune_safe_environment env = Safe_typing.prune_safe_environment env
-(* XXX TODO pass args so that these functions can stop at the current
- * file boundaries *)
 let () =
   Summary.declare_summary "Global environment"
     { Summary.freeze_function = (function
         | `Yes -> join_safe_environment (); !global_env
         | `No -> !global_env
-        | `Shallow -> prune_safe_environment !global_env);
+        | `Shallow -> !global_env);
       unfreeze_function = (fun fr -> global_env := fr);
       init_function = (fun () -> global_env := Safe_typing.empty_environment) }
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 81bfcacce..08eaa30f5 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -277,18 +277,18 @@ let close_proof ~now fpl =
     List.iter (fun x -> ignore(Future.compute x.Entries.const_entry_body)) entries;
   (pid, (entries, compute_guard, strength, hook))
 
-let return_proof ~fix_exn =
+let return_proof () =
   let { proof } = cur_pstate () in
   let initial_goals = Proof.initial_goals proof in
   let evd =
    try Proof.return proof with
    | Proof.UnfinishedProof ->
-       raise (fix_exn(Errors.UserError("last tactic before Qed",
-         str"Attempt to save an incomplete proof")))
+       raise (Errors.UserError("last tactic before Qed",
+         str"Attempt to save an incomplete proof"))
    | Proof.HasUnresolvedEvar ->
-       raise (fix_exn(Errors.UserError("last tactic before Qed",
+       raise (Errors.UserError("last tactic before Qed",
          str"Attempt to save a proof with existential " ++
-         str"variables still non-instantiated")))
+         str"variables still non-instantiated"))
   in
   let eff = Evd.eval_side_effects evd in
   (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
@@ -297,8 +297,8 @@ let return_proof ~fix_exn =
   List.map (fun (c, _) -> (Evarutil.nf_evar evd c, eff)) initial_goals
 
 let close_future_proof proof = close_proof ~now:false proof
-let close_proof () =
-  close_proof ~now:true (Future.from_here (return_proof ~fix_exn:(fun x -> x)))
+let close_proof fix_exn =
+  close_proof ~now:true (Future.from_here ~fix_exn (return_proof ()))
 
 (**********************************************************)
 (*                                                        *)
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 5922075ec..9d7407010 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -64,12 +64,14 @@ type closed_proof =
   (Entries.definition_entry list * lemma_possible_guards *
     Decl_kinds.goal_kind * unit Tacexpr.declaration_hook)
 
-val close_proof : unit -> closed_proof
+(* Takes a function to add to the exceptions data relative to the
+   state in which the proof was built *)
+val close_proof : (exn -> exn) -> closed_proof
 
 (* Intermediate step necessary to delegate the future.
  * Both access the current proof state. The formes is supposed to be
  * chained with a computation that completed the proof *)
-val return_proof : fix_exn:(exn -> exn) -> Entries.proof_output list
+val return_proof : unit -> Entries.proof_output list
 val close_future_proof :
   Entries.proof_output list Future.computation -> closed_proof
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 308bdc07d..9efe4eefc 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -68,8 +68,7 @@ let red_constant_entry n ce = function
   | None -> ce
   | Some red ->
       let proof_out = ce.const_entry_body in
-      { ce with const_entry_body = Future.chain ~id:"red_constant_entry"
-          proof_out (fun (body,eff) ->
+      { ce with const_entry_body = Future.chain proof_out (fun (body,eff) ->
           under_binders (Global.env()) 
             (fst (reduction_of_red_expr red)) n body,eff) }
 
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 43aefc722..5a936e623 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -48,9 +48,8 @@ let adjust_guardness_conditions const = function
   | [] -> const (* Not a recursive statement *)
   | possible_indexes ->
   (* Try all combinations... not optimal *)
-      (* XXX bug ignore(Future.join const.const_entry_body); *)
      { const with const_entry_body =
-        Future.chain ~id:"adjust_guardness_conditions" const.const_entry_body
+        Future.chain const.const_entry_body
         (fun (body, eff) ->
           match kind_of_term body with
           | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 789b56914..487120b27 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -201,9 +201,8 @@ module VCS : sig
   val set_state : id -> state -> unit
   val forget_state : id -> unit
 
-  (* TODO: move elsewhere if possible, so that purify can be just called *)
   (* cuts from start -> stop, raising Expired if some nodes are not there *)
-  val slice : start:id -> stop:id -> purify:(state -> state) -> vcs
+  val slice : start:id -> stop:id -> vcs
   
   val create_cluster : id list -> tip:id -> unit
   val cluster_of : id -> id option
@@ -391,7 +390,7 @@ end = struct (* {{{ *)
   
   let visit id = Vcs_aux.visit !vcs id
 
-  let slice ~start ~stop ~purify =
+  let slice ~start ~stop =
     let l =
       let rec aux id =
         if Stateid.equal id stop then [] else
@@ -408,9 +407,7 @@ end = struct (* {{{ *)
     (* Stm should have reached the beginning of proof *)
     assert (not (Option.is_empty info.state));
     (* This may be expensive *)
-    let info = { info with
-      state = Some (purify (Option.get info.state));
-      vcs_backup = None,None } in
+    let info = { info with vcs_backup = None, None } in
     let v = Vcs_.set_info v stop info in
     List.fold_right (fun (id,tr) v ->
       let v = Vcs_.commit v id tr in
@@ -499,10 +496,6 @@ module State : sig
 
   val exn_on : Stateid.t -> ?valid:Stateid.t -> exn -> exn
 
-  (* projects a state so that it can be marshalled and its content is
-   * sufficient for the execution of Coq on a proof branch *)
-  val make_shallow : state -> state
-
 end = struct (* {{{ *)
 
   (* cur_id holds Stateid.dummy in case the last attempt to define a state
@@ -523,15 +516,6 @@ end = struct (* {{{ *)
     (fun () -> in_t (freeze_global_state `No, !cur_id))
     (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i)
 
-  let make_shallow s =
-    if s.shallow then s
-    else
-      Future.purify (fun s ->
-        Printf.eprintf
-          "make_shallow & define should be protected by a lock!\n";
-        unfreeze_global_state s;
-        freeze_global_state `Shallow) s
-
   let is_cached id =
     Stateid.equal id !cur_id ||
     match VCS.get_info id with
@@ -734,16 +718,15 @@ end = struct (* {{{ *)
     match task with
     | TaskBuildProof (exn_info,bop,eop,_,_) ->
         ReqBuildProof(exn_info,eop,
-          VCS.slice ~start:eop ~stop:bop ~purify:State.make_shallow)
+          VCS.slice ~start:eop ~stop:bop)
 
   let cancel_switch_of_task = function
     | TaskBuildProof (_,_,_,_,c) -> c
 
   let build_proof_here (id,valid) eop =
-    Future.create (fun () ->
+    Future.create (State.exn_on id ~valid) (fun () ->
       !reach_known_state ~cache:`No eop;
-      let p = Proof_global.return_proof ~fix_exn:(State.exn_on id ~valid) in
-      p)
+      Proof_global.return_proof ())
 
   let slave_respond msg =
     match msg with
@@ -811,12 +794,12 @@ end = struct (* {{{ *)
     TQueue.wait_until_n_are_waiting_and_queue_empty
       (SlavesPool.n_slaves ()) queue
 
-  let build_proof ~exn_info ~start ~stop =
+  let build_proof ~exn_info:(id,valid as exn_info) ~start ~stop =
     let cancel_switch = ref false in
     if SlavesPool.is_empty () then
       build_proof_here exn_info stop, cancel_switch
     else 
-      let f, assign = Future.create_delegate () in
+      let f, assign = Future.create_delegate (State.exn_on id ~valid) in
       Pp.feedback (Interface.InProgress 1);
       TQueue.push queue
         (TaskBuildProof(exn_info,start,stop,assign,cancel_switch));
@@ -1120,7 +1103,8 @@ let known_state ?(redefine_qed=false) ~cache id =
                 reach eop;
                 begin match keep with
                 | VtKeep ->
-                    let proof = Proof_global.close_proof () in
+                    let proof =
+                      Proof_global.close_proof (State.exn_on id ~valid:eop) in
                     reach view.next;
                     vernac_interp id ~proof x
                 | VtDrop ->