aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli10
-rw-r--r--kernel/opaqueproof.ml16
-rw-r--r--kernel/term_typing.ml6
-rw-r--r--lib/future.ml82
-rw-r--r--lib/future.mli69
-rw-r--r--library/states.ml2
-rw-r--r--library/states.mli7
-rw-r--r--plugins/derive/derive.ml2
-rw-r--r--plugins/funind/indfun_common.ml9
-rw-r--r--plugins/funind/indfun_common.mli2
-rw-r--r--plugins/funind/invfun.ml3
-rw-r--r--plugins/funind/recdef.ml3
-rw-r--r--plugins/ltac/tacentries.ml4
-rw-r--r--proofs/pfedit.ml2
-rw-r--r--proofs/proof_global.ml4
-rw-r--r--stm/stm.ml135
-rw-r--r--vernac/command.ml2
-rw-r--r--vernac/lemmas.ml2
-rw-r--r--vernac/vernacentries.ml67
-rw-r--r--vernac/vernacentries.mli5
20 files changed, 202 insertions, 230 deletions
diff --git a/API/API.mli b/API/API.mli
index d4f0872a3..a41009fa2 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1914,7 +1914,11 @@ module Summary :
sig
type frozen
- type marshallable
+
+ type marshallable =
+ [ `Yes (* Full data will be marshalled to disk *)
+ | `No (* Full data will be store in memory, e.g. for Undo *)
+ | `Shallow ] (* Only part of the data will be marshalled to a slave process *)
type 'a summary_declaration =
{ freeze_function : marshallable -> 'a;
@@ -2062,7 +2066,6 @@ module States :
sig
type state
- val with_state_protection_on_exception : ('a -> 'b) -> 'a -> 'b
val with_state_protection : ('a -> 'b) -> 'a -> 'b
end
@@ -5799,6 +5802,9 @@ sig
shallow : bool (* is the state trimmed down (libstack) *)
}
+ val freeze_interp_state : Summary.marshallable -> interp_state
+ val unfreeze_interp_state : interp_state -> unit
+
val dump_global : Libnames.reference Misctypes.or_by_notation -> unit
val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
Evd.evar_map * Redexpr.red_expr) Hook.t
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 5e20c1b51..400f9feee 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -78,12 +78,12 @@ let subst_opaque sub = function
let iter_direct_opaque f = function
| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
| Direct (d,cu) ->
- Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u))
+ Direct (d,Future.chain cu (fun (c, u) -> f c; c, u))
let discharge_direct_opaque ~cook_constr ci = function
| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
| Direct (d,cu) ->
- Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u))
+ Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u))
let join_opaque { opaque_val = prfs; opaque_dir = odp } = function
| Direct (_,cu) -> ignore(Future.join cu)
@@ -105,7 +105,7 @@ let force_proof { opaque_val = prfs; opaque_dir = odp } = function
| Indirect (l,dp,i) ->
let pt =
if DirPath.equal dp odp
- then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst
+ then Future.chain (snd (Int.Map.find i prfs)) fst
else !get_opaque dp i in
let c = Future.force pt in
force_constr (List.fold_right subst_substituted l (from_val c))
@@ -120,20 +120,20 @@ let force_constraints { opaque_val = prfs; opaque_dir = odp } = function
| Some u -> Future.force u
let get_constraints { opaque_val = prfs; opaque_dir = odp } = function
- | Direct (_,cu) -> Some(Future.chain ~pure:true cu snd)
+ | Direct (_,cu) -> Some(Future.chain cu snd)
| Indirect (_,dp,i) ->
if DirPath.equal dp odp
- then Some(Future.chain ~pure:true (snd (Int.Map.find i prfs)) snd)
+ then Some(Future.chain (snd (Int.Map.find i prfs)) snd)
else !get_univ dp i
let get_proof { opaque_val = prfs; opaque_dir = odp } = function
- | Direct (_,cu) -> Future.chain ~pure:true cu fst
+ | Direct (_,cu) -> Future.chain cu fst
| Indirect (l,dp,i) ->
let pt =
if DirPath.equal dp odp
- then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst
+ then Future.chain (snd (Int.Map.find i prfs)) fst
else !get_opaque dp i in
- Future.chain ~pure:true pt (fun c ->
+ Future.chain pt (fun c ->
force_constr (List.fold_right subst_substituted l (from_val c)))
module FMap = Future.UUIDMap
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 22e109b01..f93b24b3e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -266,7 +266,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
let tyj = infer_type env typ in
let proofterm =
- Future.chain ~pure:true body (fun ((body,uctx),side_eff) ->
+ Future.chain body (fun ((body,uctx),side_eff) ->
let j, uctx = match trust with
| Pure ->
let env = push_context_set uctx env in
@@ -535,7 +535,7 @@ let export_side_effects mb env ce =
let { const_entry_body = body } = c in
let _, eff = Future.force body in
let ce = DefinitionEntry { c with
- const_entry_body = Future.chain ~pure:true body
+ const_entry_body = Future.chain body
(fun (b_ctx, _) -> b_ctx, ()) } in
let not_exists (c,_,_,_) =
try ignore(Environ.lookup_constant c env); false
@@ -628,7 +628,7 @@ let translate_local_def mb env id centry =
let translate_mind env kn mie = Indtypes.check_inductive env kn mie
let inline_entry_side_effects env ce = { ce with
- const_entry_body = Future.chain ~pure:true
+ const_entry_body = Future.chain
ce.const_entry_body (fun ((body, ctx), side_eff) ->
let body, ctx',_ = inline_side_effects env body ctx side_eff in
(body, ctx'), ());
diff --git a/lib/future.ml b/lib/future.ml
index d9463aa0f..09285ea27 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -6,12 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* To deal with side effects we have to save/restore the system state *)
-type freeze
-let freeze = ref (fun () -> assert false : unit -> freeze)
-let unfreeze = ref (fun _ -> () : freeze -> unit)
-let set_freeze f g = freeze := f; unfreeze := g
-
let not_ready_msg = ref (fun name ->
Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^
"Please wait or pass "^
@@ -30,6 +24,7 @@ let customize_not_here_msg f = not_here_msg := f
exception NotReady of string
exception NotHere of string
+
let _ = CErrors.register_handler (function
| NotReady name -> !not_ready_msg name
| NotHere name -> !not_here_msg name
@@ -59,7 +54,7 @@ type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computat
and 'a comp =
| Delegated of (unit -> unit)
| Closure of (unit -> 'a)
- | Val of 'a * freeze option
+ | Val of 'a
| Exn of Exninfo.iexn (* Invariant: this exception is always "fixed" as in fix_exn *)
and 'a comput =
@@ -74,7 +69,7 @@ let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x =
ref (Ongoing (name, CEphemeron.create (uuid, f, Pervasives.ref x)))
let get x =
match !x with
- | Finished v -> unnamed, UUID.invalid, id, ref (Val (v,None))
+ | Finished v -> unnamed, UUID.invalid, id, ref (Val v)
| Ongoing (name, x) ->
try let uuid, fix, c = CEphemeron.get x in name, uuid, fix, c
with CEphemeron.InvalidKey ->
@@ -95,13 +90,13 @@ let is_exn kx = let _, _, _, x = get kx in match !x with
| Val _ | Closure _ | Delegated _ -> false
let peek_val kx = let _, _, _, x = get kx in match !x with
- | Val (v, _) -> Some v
+ | Val v -> Some v
| Exn _ | Closure _ | Delegated _ -> None
let uuid kx = let _, id, _, _ = get kx in id
-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 ())))
+let from_val ?(fix_exn=id) v = create fix_exn (Val v)
+let from_here ?(fix_exn=id) v = create fix_exn (Val v)
let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn
@@ -110,7 +105,7 @@ let create_delegate ?(blocking=true) ~name fix_exn =
let _, _, fix_exn, c = get ck in
assert (match !c with Delegated _ -> true | _ -> false);
begin match v with
- | `Val v -> c := Val (v, None)
+ | `Val v -> c := Val v
| `Exn e -> c := Exn (fix_exn e)
| `Comp f -> let _, _, _, comp = get f in c := !comp end;
signal () in
@@ -124,17 +119,16 @@ let create_delegate ?(blocking=true) ~name fix_exn =
ck, assignement signal ck
(* TODO: get rid of try/catch to be stackless *)
-let rec compute ~pure ck : 'a value =
+let rec compute ck : 'a value =
let _, _, fix_exn, c = get ck in
match !c with
- | Val (x, _) -> `Val x
+ | Val x -> `Val x
| Exn (e, info) -> `Exn (e, info)
- | Delegated wait -> wait (); compute ~pure ck
+ | Delegated wait -> wait (); compute ck
| Closure f ->
try
let data = f () in
- let state = if pure then None else Some (!freeze ()) in
- c := Val (data, state); `Val data
+ c := Val data; `Val data
with e ->
let e = CErrors.push e in
let e = fix_exn e in
@@ -142,60 +136,30 @@ let rec compute ~pure ck : 'a value =
| (NotReady _, _) -> `Exn e
| _ -> c := Exn e; `Exn e
-let force ~pure x = match compute ~pure x with
+let force x = match compute x with
| `Val v -> v
| `Exn e -> Exninfo.iraise e
-let chain ~pure ck f =
+let chain ck f =
let name, uuid, fix_exn, c = get ck in
create ~uuid ~name fix_exn (match !c with
- | Closure _ | Delegated _ -> Closure (fun () -> f (force ~pure ck))
+ | Closure _ | Delegated _ -> Closure (fun () -> f (force ck))
| Exn _ as x -> x
- | Val (v, None) when pure -> Val (f v, None)
- | Val (v, Some _) when pure -> Val (f v, None)
- | Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v)
- | Val (v, None) ->
- match !ck with
- | Finished _ -> CErrors.anomaly(Pp.str
- "Future.chain ~pure:false call on an already joined computation.")
- | Ongoing _ -> CErrors.anomaly(Pp.strbrk(
- "Future.chain ~pure:false call on a pure computation. "^
- "This can happen if the computation was initial created with "^
- "Future.from_val or if it was Future.chain ~pure:true with a "^
- "function and later forced.")))
+ | Val v -> Val (f v))
let create fix_exn f = create fix_exn (Closure f)
let replace kx y =
let _, _, _, x = get kx in
match !x with
- | Exn _ -> x := Closure (fun () -> force ~pure:false y)
+ | Exn _ -> x := Closure (fun () -> force y)
| _ -> CErrors.anomaly
(Pp.str "A computation can be replaced only if is_exn holds.")
-let purify f x =
- let state = !freeze () in
- try
- let v = f x in
- !unfreeze state;
- v
- with e ->
- let e = CErrors.push e in !unfreeze state; Exninfo.iraise e
-
-let transactify f x =
- let state = !freeze () in
- try f x
- with e ->
- let e = CErrors.push e in !unfreeze state; Exninfo.iraise e
-
-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 ~pure x = purify_future (force ~pure) x
-let chain ~pure x f =
- let y = chain ~pure x f in
- if is_over x then ignore(force ~pure y);
+let chain x f =
+ let y = chain x f in
+ if is_over x then ignore(force y);
y
-let force x = force ~pure:false x
let join kx =
let v = force kx in
@@ -205,12 +169,11 @@ let join kx =
let sink kx = if is_val kx then ignore(join kx)
let split2 x =
- chain ~pure:true x (fun x -> fst x),
- chain ~pure:true x (fun x -> snd x)
+ chain x (fun x -> fst x), chain x (fun x -> snd x)
let map2 f x l =
CList.map_i (fun i y ->
- let xi = chain ~pure:true x (fun x ->
+ let xi = chain x (fun x ->
try List.nth x i
with Failure _ | Invalid_argument _ ->
CErrors.anomaly (Pp.str "Future.map2 length mismatch.")) in
@@ -226,6 +189,5 @@ let print f kx =
match !x with
| Delegated _ -> str "Delegated" ++ uid
| Closure _ -> str "Closure" ++ uid
- | Val (x, None) -> str "PureVal" ++ uid ++ spc () ++ hov 0 (f x)
- | Val (x, Some _) -> str "StateVal" ++ uid ++ spc () ++ hov 0 (f x)
+ | Val x -> str "PureVal" ++ uid ++ spc () ++ hov 0 (f x)
| Exn (e, _) -> str "Exn" ++ uid ++ spc () ++ hov 0 (str (Printexc.to_string e))
diff --git a/lib/future.mli b/lib/future.mli
index acfce51a0..853f81cea 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -6,42 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* Futures: asynchronous computations with some purity enforcing
+(* Futures: asynchronous computations.
*
* A Future.computation is like a lazy_t but with some extra bells and whistles
- * to deal with imperative code and eventual delegation to a slave process.
+ * to deal with eventual delegation to a slave process.
*
- * Example of a simple scenario taken into account:
- *
- * let f = Future.from_here (number_of_constants (Global.env())) in
- * let g = Future.chain ~pure:false f (fun n ->
- * n = number_of_constants (Global.env())) in
- * ...
- * Lemmas.save_named ...;
- * ...
- * let b = Future.force g in
- *
- * The Future.computation f holds a (immediate, no lazy here) value.
- * We then chain to obtain g that (will) hold false if (when it will be
- * run) the global environment has a different number of constants, true
- * if nothing changed.
- * Before forcing g, we add to the global environment one more constant.
- * When finally we force g. Its value is going to be *true*.
- * This because Future.from_here stores in the computation not only the initial
- * value but the entire system state. When g is forced the state is restored,
- * hence Global.env() returns the environment that was actual when f was
- * created.
- * Last, forcing g is run protecting the system state, hence when g finishes,
- * the actual system state is restored.
- *
- * If you compare this with lazy_t, you see that the value returned is *false*,
- * that is counter intuitive and error prone.
- *
- * Still not all computations are impure and access/alter the system state.
- * This class can be optimized by using ~pure:true, but there is no way to
- * statically check if this flag is misused, hence use it with care.
- *
- * Other differences with lazy_t is that a future computation that produces
+ * One difference with lazy_t is that a future computation that produces
* and exception can be substituted for another computation of the same type.
* Moreover a future computation can be delegated to another execution entity
* that will be allowed to set the result. Finally future computations can
@@ -113,27 +83,17 @@ val is_exn : 'a computation -> bool
val peek_val : 'a computation -> 'a option
val uuid : 'a computation -> UUID.t
-(* [chain pure c f] chains computation [c] with [f].
- * [chain] forces immediately the new computation if the old one is_over (Exn or Val).
- * The [pure] parameter is tricky:
- * [pure]:
- * When pure is true, the returned computation will not keep a copy
- * of the global state.
- * [let c' = chain ~pure:true c f in let c'' = chain ~pure:false c' g in]
- * is invalid. It works if one forces [c''] since the whole computation
- * will be executed in one go. It will not work, and raise an anomaly, if
- * one forces c' and then c''.
- * [join c; chain ~pure:false c g] is invalid and fails at runtime.
- * [force c; chain ~pure:false c g] is correct.
- *)
-val chain : pure:bool ->
- 'a computation -> ('a -> 'b) -> 'b computation
+(* [chain c f] chains computation [c] with [f].
+ * [chain] is eager, that is to say, it won't suspend the new computation
+ * if the old one is_over (Exn or Val).
+*)
+val chain : 'a computation -> ('a -> 'b) -> 'b computation
(* Forcing a computation *)
val force : 'a computation -> 'a
val compute : 'a computation -> 'a value
-(* Final call, no more *inpure* chain allowed since the state is lost.
+(* Final call.
* Also the fix_exn function is lost, hence error reporting can be incomplete
* in a computation obtained by chaining on a joined future. *)
val join : 'a computation -> 'a
@@ -148,19 +108,8 @@ val map2 :
('a computation -> 'b -> 'c) ->
'a list computation -> 'b list -> 'c list
-(* 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
-
(** Debug: print a computation given an inner printing function. *)
val print : ('a -> Pp.t) -> 'a computation -> Pp.t
-type freeze
-(* 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 -> freeze) -> (freeze -> unit) -> unit
-
val customize_not_ready_msg : (string -> Pp.t) -> unit
val customize_not_here_msg : (string -> Pp.t) -> unit
diff --git a/library/states.ml b/library/states.ml
index 03e4610a6..27e0a94f9 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -37,5 +37,3 @@ let with_state_protection f x =
with reraise ->
let reraise = CErrors.push reraise in
(unfreeze st; iraise reraise)
-
-let with_state_protection_on_exception = Future.transactify
diff --git a/library/states.mli b/library/states.mli
index 780a4e8dc..accd0e7ea 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -30,10 +30,3 @@ val replace_summary : state -> Summary.frozen -> state
val with_state_protection : ('a -> 'b) -> 'a -> 'b
-(** [with_state_protection_on_exception f x] applies [f] to [x] and restores the
- state of the whole system as it was before applying [f] only if an
- exception is raised. Unlike [with_state_protection] it also takes into
- account the proof state *)
-
-val with_state_protection_on_exception : ('a -> 'b) -> 'a -> 'b
-
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 1524079f4..6d3d4b743 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -10,7 +10,7 @@ open Context.Named.Declaration
let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body)
: Safe_typing.private_constants Entries.const_entry_body =
- Future.chain ~pure:true x begin fun ((b,ctx),fx) ->
+ Future.chain x begin fun ((b,ctx),fx) ->
(f b , ctx) , fx
end
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 1e8854249..76fcd5ec8 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -549,3 +549,12 @@ type tcc_lemma_value =
| Undefined
| Value of Term.constr
| Not_needed
+
+(* We only "purify" on exceptions *)
+let funind_purify f x =
+ let st = Vernacentries.freeze_interp_state `No in
+ try f x
+ with e ->
+ let e = CErrors.push e in
+ Vernacentries.unfreeze_interp_state st;
+ Exninfo.iraise e
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 2e2ced790..d41abee87 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -123,3 +123,5 @@ type tcc_lemma_value =
| Undefined
| Value of Term.constr
| Not_needed
+
+val funind_purify : ('a -> 'b) -> ('a -> 'b)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 299753766..9cb2a0a3f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -759,7 +759,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
let funs = Array.of_list funs and graphs = Array.of_list graphs in
let map (c, u) = mkConstU (c, EInstance.make u) in
let funs_constr = Array.map map funs in
- States.with_state_protection_on_exception
+ (* XXX STATE Why do we need this... why is the toplevel protection not enought *)
+ funind_purify
(fun () ->
let env = Global.env () in
let evd = ref (Evd.from_env env) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 74c454334..76f859ed7 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1595,7 +1595,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
spc () ++ str"is defined" )
)
in
- States.with_state_protection_on_exception (fun () ->
+ (* XXX STATE Why do we need this... why is the toplevel protection not enought *)
+ funind_purify (fun () ->
com_terminate
tcc_lemma_name
tcc_lemma_constr
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index bcd5b388a..0bf6e3d15 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -468,7 +468,9 @@ let register_ltac local tacl =
let () = List.iter iter_rec recvars in
List.map map rfun
in
- let defs = Future.transactify defs () in
+ (* STATE XXX: Review what is going on here. Why does this needs
+ protection? Why is not the STM level protection enough? Fishy *)
+ let defs = States.with_state_protection defs () in
let iter (def, tac) = match def with
| NewTac id ->
Tacenv.register_ltac false local id tac;
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 23f96b5a3..469e1a011 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -156,7 +156,7 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
let ce =
if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce
else { ce with
- const_entry_body = Future.chain ~pure:true ce.const_entry_body
+ const_entry_body = Future.chain ce.const_entry_body
(fun (pt, _) -> pt, ()) } in
let (cb, ctx), () = Future.force ce.const_entry_body in
let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index cd4d1dcf6..621178982 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -373,11 +373,11 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in
(univs, typ), ((body, Univ.ContextSet.empty), eff)
in
- fun t p -> Future.split2 (Future.chain ~pure:true p (make_body t))
+ fun t p -> Future.split2 (Future.chain p (make_body t))
else
fun t p ->
Future.from_val (univctx, nf t),
- Future.chain ~pure:true p (fun (pt,eff) ->
+ Future.chain p (fun (pt,eff) ->
(* Deferred proof, we already checked the universe declaration with
the initial universes, ensure that the final universes respect
the declaration as well. If the declaration is non-extensible,
diff --git a/stm/stm.ml b/stm/stm.ml
index 231ec0547..84a4c5cc5 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -23,7 +23,17 @@ open CErrors
open Feedback
open Vernacexpr
-let _ds = Vernacentries._dummy_interp_state
+(* Protect against state changes *)
+let stm_purify f x =
+ let st = Vernacentries.freeze_interp_state `No in
+ try
+ let res = f x in
+ Vernacentries.unfreeze_interp_state st;
+ res
+ with e ->
+ let e = CErrors.push e in
+ Vernacentries.unfreeze_interp_state st;
+ Exninfo.iraise e
let execution_error ?loc state_id msg =
feedback ~id:state_id
@@ -754,13 +764,6 @@ end = struct (* {{{ *)
let cur_id = ref Stateid.dummy
let fix_exn_ref = ref (fun x -> x)
- (* hack to make futures functional *)
- (* this will be removed when we don't call it anymore as we fully
- handle state functionally *)
- let () = Future.set_freeze
- (fun () -> Obj.magic (freeze_interp_state `No, !cur_id))
- (fun t -> let s,i = Obj.magic t in unfreeze_interp_state s; cur_id := i)
-
type proof_part =
Proof_global.state * Summary.frozen_bits (* only meta counters *)
@@ -797,9 +800,13 @@ end = struct (* {{{ *)
let install_cached id =
match VCS.get_info id with
| { state = Valid s } ->
- if Stateid.equal id !cur_id then () (* optimization *)
- else begin Vernacentries.unfreeze_interp_state s; cur_id := id end
- | { state = Error ie } -> cur_id := id; Exninfo.iraise ie
+ Vernacentries.unfreeze_interp_state s;
+ cur_id := id
+
+ | { state = Error ie } ->
+ cur_id := id;
+ Exninfo.iraise ie
+
| _ ->
(* coqc has a 1 slot cache and only for valid states *)
if VCS.is_interactive () = `No && Stateid.equal id !cur_id then ()
@@ -1429,18 +1436,28 @@ end = struct (* {{{ *)
* 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 = Vernacentries.freeze_interp_state `No in
if not drop then begin
- let checked_proof = Future.chain ~pure:false future_proof (fun p ->
+ 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 *)
+ Vernacentries.unfreeze_interp_state st;
let pobject, _ =
Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in
let terminator = (* The one sent by master is an InvalidKey *)
Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in
+
+ let st = Vernacentries.freeze_interp_state `No in
stm_vernac_interp stop
- ~proof:(pobject, terminator) _ds
+ ~proof:(pobject, terminator) st
{ verbose = false; loc; indentation = 0; strlen = 0;
expr = (VernacEndProof (Proved (Opaque,None))) }) in
ignore(Future.join checked_proof);
end;
+ (* STATE: Restore the state XXX: handle exn *)
+ Vernacentries.unfreeze_interp_state st;
RespBuiltProof(proof,time)
with
| e when CErrors.noncritical e || e = Stack_overflow ->
@@ -1580,7 +1597,9 @@ end = struct (* {{{ *)
* - end : start + qed
* => takes nothing from the itermediate states.
*)
- ignore(stm_vernac_interp stop ~proof _ds
+ (* STATE We use the state resulting from reaching start. *)
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp stop ~proof st
{ verbose = false; loc; indentation = 0; strlen = 0;
expr = (VernacEndProof (Proved (Opaque,None))) });
`OK proof
@@ -1638,10 +1657,9 @@ end = struct (* {{{ *)
let pr =
Future.from_val (map (Option.get (Global.body_of_constant_body c))) in
let uc =
- Future.chain
- ~pure:true uc Univ.hcons_universe_context_set in
- let pr = Future.chain ~pure:true pr discharge in
- let pr = Future.chain ~pure:true pr Constr.hcons in
+ Future.chain uc Univ.hcons_universe_context_set in
+ let pr = Future.chain pr discharge in
+ let pr = Future.chain pr Constr.hcons in
Future.sink pr;
let extra = Future.join uc in
u.(bucket) <- uc;
@@ -1817,7 +1835,7 @@ end = struct (* {{{ *)
Option.iter VCS.restore vcs;
try
Reach.known_state ~cache:`No id;
- Future.purify (fun () ->
+ stm_purify (fun () ->
let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in
let g = Evd.find sigma0 r_goal in
let is_ground c = Evarutil.is_ground_term sigma0 (EConstr.of_constr c) in
@@ -1837,8 +1855,8 @@ end = struct (* {{{ *)
* => captures state id in a future closure, which will
discard execution state but for the proof + univs.
*)
-
- ignore(stm_vernac_interp r_state_fb _ds ast);
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp r_state_fb st ast);
let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
match Evd.(evar_body (find sigma r_goal)) with
| Evd.Evar_empty -> RespNoProgress
@@ -1877,7 +1895,8 @@ end = struct (* {{{ *)
| VernacRedirect (_,(_,e)) -> find ~time ~fail e
| VernacFail e -> find ~time ~fail:true e
| e -> e, time, fail in find ~time:false ~fail:false e in
- Vernacentries.with_fail fail (fun () ->
+ let st = Vernacentries.freeze_interp_state `No in
+ Vernacentries.with_fail st fail (fun () ->
(if time then System.with_time !Flags.time else (fun x -> x)) (fun () ->
ignore(TaskQueue.with_n_workers nworkers (fun queue ->
Proof_global.with_current_proof (fun _ p ->
@@ -1969,12 +1988,14 @@ end = struct (* {{{ *)
VCS.restore r_doc;
VCS.print ();
Reach.known_state ~cache:`No r_where;
+ (* STATE *)
+ let st = Vernacentries.freeze_interp_state `No in
try
(* STATE SPEC:
* - start: r_where
* - end : after execution of r_what
*)
- ignore(stm_vernac_interp r_for _ds { r_what with verbose = true });
+ ignore(stm_vernac_interp r_for st { r_what with verbose = true });
feedback ~id:r_for Processed
with e when CErrors.noncritical e ->
let e = CErrors.push e in
@@ -2191,7 +2212,9 @@ let known_state ?(redefine_qed=false) ~cache id =
* - start: Modifies the input state adding a proof.
* - end : maybe after recovery command.
*)
- Option.iter (fun expr -> ignore(stm_vernac_interp id _ds {
+ (* STATE: We use an updated state with proof *)
+ let st = Vernacentries.freeze_interp_state `No in
+ Option.iter (fun expr -> ignore(stm_vernac_interp id st {
verbose = true; loc = None; expr; indentation = 0;
strlen = 0 } ))
recovery_command
@@ -2231,10 +2254,12 @@ let known_state ?(redefine_qed=false) ~cache id =
let inject_non_pstate (s,l) =
Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env ()
in
- let rec pure_cherry_pick_non_pstate safe_id id = Future.purify (fun id ->
- stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
- reach ~safe_id id;
- cherry_pick_non_pstate ()) id
+ let rec pure_cherry_pick_non_pstate safe_id id =
+ stm_purify (fun id ->
+ stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
+ reach ~safe_id id;
+ cherry_pick_non_pstate ())
+ id
(* traverses the dag backward from nodes being already calculated *)
and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id =
@@ -2267,7 +2292,9 @@ let known_state ?(redefine_qed=false) ~cache id =
| `Cmd { cast = x; ceff = eff; ctac = true; cblock } -> (fun () ->
resilient_tactic id cblock (fun () ->
reach view.next;
- ignore(stm_vernac_interp id _ds x)
+ (* State resulting from reach *)
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp id st x)
);
if eff then update_global_env ()
), (if eff then `Yes else cache), true
@@ -2276,18 +2303,23 @@ let known_state ?(redefine_qed=false) ~cache id =
| Flags.APon | Flags.APonLazy ->
resilient_command reach view.next
| Flags.APoff -> reach view.next);
- ignore(stm_vernac_interp id _ds x);
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp id st x);
if eff then update_global_env ()
), (if eff then `Yes else cache), true
| `Fork ((x,_,_,_), None) -> (fun () ->
resilient_command reach view.next;
- ignore(stm_vernac_interp id _ds x);
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp id st x);
wall_clock_last_fork := Unix.gettimeofday ()
), `Yes, true
| `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *)
reach ~cache:`Shallow prev;
reach view.next;
- (try ignore(stm_vernac_interp id _ds x);
+
+ (try
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp id st x);
with e when CErrors.noncritical e ->
let (e, info) = CErrors.push e in
let info = Stateid.add info ~valid:prev id in
@@ -2337,14 +2369,18 @@ let known_state ?(redefine_qed=false) ~cache id =
Proof_global.close_future_proof ~feedback_id:id fp in
if not delegate then ignore(Future.compute fp);
reach view.next;
- ignore(stm_vernac_interp id ~proof _ds x);
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp id ~proof st x);
feedback ~id:id Incomplete
| { VCS.kind = `Master }, _ -> assert false
end;
Proof_global.discard_all ()
), (if redefine_qed then `No else `Yes), true
| `Sync (name, `Immediate) -> (fun () ->
- reach eop; ignore(stm_vernac_interp id _ds x); Proof_global.discard_all ()
+ reach eop;
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp id st x);
+ Proof_global.discard_all ()
), `Yes, true
| `Sync (name, reason) -> (fun () ->
log_processing_sync id name reason;
@@ -2365,7 +2401,8 @@ let known_state ?(redefine_qed=false) ~cache id =
if keep != VtKeepAsAxiom then
reach view.next;
let wall_clock2 = Unix.gettimeofday () in
- ignore(stm_vernac_interp id ?proof _ds x);
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp id ?proof st x);
let wall_clock3 = Unix.gettimeofday () in
Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time"
(Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2));
@@ -2381,7 +2418,10 @@ let known_state ?(redefine_qed=false) ~cache id =
in
aux (collect_proof keep (view.next, x) brname brinfo eop)
| `Sideff (ReplayCommand x,_) -> (fun () ->
- reach view.next; ignore(stm_vernac_interp id _ds x); update_global_env ()
+ reach view.next;
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp id st x);
+ update_global_env ()
), cache, true
| `Sideff (CherryPickEnv, origin) -> (fun () ->
reach view.next;
@@ -2525,7 +2565,7 @@ let check_task name (tasks,rcbackup) i =
RemoteCounter.restore rcbackup;
let vcs = VCS.backup () in
try
- let rc = Future.purify (Slaves.check_task name tasks) i in
+ let rc = stm_purify (Slaves.check_task name tasks) i in
VCS.restore vcs;
rc
with e when CErrors.noncritical e -> VCS.restore vcs; false
@@ -2535,7 +2575,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
RemoteCounter.restore rcbackup;
let finish_task u (_,_,i) =
let vcs = VCS.backup () in
- let u = Future.purify (Slaves.finish_task name u d p t) i in
+ let u = stm_purify (Slaves.finish_task name u d p t) i in
VCS.restore vcs;
u in
try
@@ -2647,11 +2687,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
(* Query *)
| VtQuery (false,route), VtNow ->
let query_sid = VCS.cur_tip () in
- (try ignore(stm_vernac_interp ~route query_sid _ds x)
+ (try
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp ~route query_sid st x)
with e ->
- let e = CErrors.push e in
- Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e));
- `Ok
+ let e = CErrors.push e in
+ Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e)); `Ok
| VtQuery (true, route), w ->
let id = VCS.new_node ~id:newtip () in
let queue =
@@ -2721,7 +2762,9 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
(* Side effect on all branches *)
| VtUnknown, _ when expr = VernacToplevelControl Drop ->
- ignore(stm_vernac_interp (VCS.get_branch_pos head) _ds x); `Ok
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp (VCS.get_branch_pos head) st x);
+ `Ok
| VtSideff l, w ->
let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
@@ -2747,8 +2790,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
VCS.checkout VCS.Branch.master;
let mid = VCS.get_branch_pos VCS.Branch.master in
let _st' = Reach.known_state ~cache:(VCS.is_interactive ()) mid in
- ignore(stm_vernac_interp id _ds x);
-
+ let st = Vernacentries.freeze_interp_state `No in
+ ignore(stm_vernac_interp id st x);
(* Vernac x may or may not start a proof *)
if not in_proof && Proof_global.there_are_pending_proofs () then
begin
@@ -2895,7 +2938,7 @@ type focus = {
}
let query ~doc ~at ~route s =
- Future.purify (fun s ->
+ stm_purify (fun s ->
if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc)
else Reach.known_state ~cache:`Yes at;
let loc, ast = parse_sentence ~doc at s in
diff --git a/vernac/command.ml b/vernac/command.ml
index a1a87d54e..f095a5d6c 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -79,7 +79,7 @@ let red_constant_entry n ce sigma = function
let (_, c) = redfun env sigma c in
EConstr.Unsafe.to_constr c
in
- { ce with const_entry_body = Future.chain ~pure:true proof_out
+ { ce with const_entry_body = Future.chain proof_out
(fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) }
let warn_implicits_in_term =
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index d45665dd4..9ab89c883 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -60,7 +60,7 @@ let adjust_guardness_conditions const = function
(* Try all combinations... not optimal *)
let env = Global.env() in
{ const with const_entry_body =
- Future.chain ~pure:true const.const_entry_body
+ Future.chain const.const_entry_body
(fun ((body, ctx), eff) ->
match kind_of_term body with
| Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 7f2985aca..13b6eafc2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2148,23 +2148,42 @@ let locate_if_not_already ?loc (e, info) =
exception HasNotFailed
exception HasFailed of Pp.t
-let with_fail b f =
- if not b then f ()
+type interp_state = { (* TODO: inline records in OCaml 4.03 *)
+ system : States.state; (* summary + libstack *)
+ proof : Proof_global.state; (* proof state *)
+ shallow : bool (* is the state trimmed down (libstack) *)
+}
+
+(* Unfortunately we cannot cache here due to some bits in the STM not
+ being fully pure. *)
+let freeze_interp_state marshallable =
+ { system = States.freeze ~marshallable;
+ proof = Proof_global.freeze ~marshallable;
+ shallow = marshallable = `Shallow }
+
+let unfreeze_interp_state { system; proof } =
+ States.unfreeze system;
+ Proof_global.unfreeze proof
+
+(* XXX STATE: this type hints that restoring the state should be the
+ caller's responsibility *)
+let with_fail st b f =
+ if not b
+ then f ()
else begin try
(* If the command actually works, ignore its effects on the state.
* Note that error has to be printed in the right state, hence
* within the purified function *)
- Future.purify
- (fun v ->
- try f v; raise HasNotFailed
- with
- | HasNotFailed as e -> raise e
- | e ->
- let e = CErrors.push e in
- raise (HasFailed (CErrors.iprint
- (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))))
- ()
+ try f (); raise HasNotFailed
+ with
+ | HasNotFailed as e -> raise e
+ | e ->
+ let e = CErrors.push e in
+ raise (HasFailed (CErrors.iprint
+ (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e)))
with e when CErrors.noncritical e ->
+ (* Restore the previous state *)
+ unfreeze_interp_state st;
let (e, _) = CErrors.push e in
match e with
| HasNotFailed ->
@@ -2175,7 +2194,7 @@ let with_fail b f =
| _ -> assert false
end
-let interp ?(verbosely=true) ?proof (loc,c) =
+let interp ?(verbosely=true) ?proof st (loc,c) =
let orig_program_mode = Flags.is_program_mode () in
let rec aux ?locality ?polymorphism isprogcmd = function
@@ -2188,7 +2207,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
| VernacPolymorphic (b, c) -> user_err Pp.(str "Polymorphism specified twice")
| VernacLocal _ -> user_err Pp.(str "Locality specified twice")
| VernacFail v ->
- with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v)
+ with_fail st true (fun () -> aux ?locality ?polymorphism isprogcmd v)
| VernacTimeout (n,v) ->
current_timeout := Some n;
aux ?locality ?polymorphism isprogcmd v
@@ -2228,21 +2247,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
if verbosely then Flags.verbosely (aux false) c
else aux false c
-type interp_state = { (* TODO: inline records in OCaml 4.03 *)
- system : States.state; (* summary + libstack *)
- proof : Proof_global.state; (* proof state *)
- shallow : bool (* is the state trimmed down (libstack) *)
-}
-
-let freeze_interp_state marshallable =
- { system = States.freeze ~marshallable;
- proof = Proof_global.freeze ~marshallable;
- shallow = (marshallable = `Shallow) }
-
-let unfreeze_interp_state { system; proof } =
- States.unfreeze system; Proof_global.unfreeze proof
-
-let _dummy_interp_state = { system = Obj.magic 0; proof = Obj.magic 0; shallow = false }
-
let interp ?verbosely ?proof st cmd =
- interp ?verbosely ?proof cmd; st
+ unfreeze_interp_state st;
+ interp ?verbosely ?proof st cmd;
+ freeze_interp_state `No
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 5559e6b81..56635c801 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -22,7 +22,6 @@ type interp_state = { (* TODO: inline records in OCaml 4.03 *)
val freeze_interp_state : Summary.marshallable -> interp_state
val unfreeze_interp_state : interp_state -> unit
-val _dummy_interp_state : interp_state
(** The main interpretation function of vernacular expressions *)
val interp :
@@ -39,7 +38,9 @@ val interp :
val make_cases : string -> string list list
-val with_fail : bool -> (unit -> unit) -> unit
+(* XXX STATE: this type hints that restoring the state should be the
+ caller's responsibility *)
+val with_fail : interp_state -> bool -> (unit -> unit) -> unit
val command_focus : unit Proof.focus_kind
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 22:50:13 +0000