aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli28
-rw-r--r--intf/vernacexpr.ml2
-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/proofBlockDelimiter.ml2
-rw-r--r--stm/stm.ml345
-rw-r--r--stm/stm.mli8
-rw-r--r--stm/vernac_classifier.ml9
-rw-r--r--stm/vernac_classifier.mli3
-rw-r--r--toplevel/vernac.ml4
-rw-r--r--vernac/command.ml2
-rw-r--r--vernac/lemmas.ml2
-rw-r--r--vernac/vernacentries.ml58
-rw-r--r--vernac/vernacentries.mli16
26 files changed, 362 insertions, 328 deletions
diff --git a/API/API.mli b/API/API.mli
index 879323a37..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;
@@ -2060,7 +2064,8 @@ end
module States :
sig
- val with_state_protection_on_exception : ('a -> 'b) -> 'a -> 'b
+ type state
+
val with_state_protection : ('a -> 'b) -> 'a -> 'b
end
@@ -3713,7 +3718,7 @@ sig
| VtProofStep of proof_step
| VtProofMode of string
| VtQuery of vernac_part_of_script * Feedback.route_id
- | VtBack of vernac_part_of_script * Stateid.t
+ | VtMeta
| VtUnknown
and vernac_qed_type =
| VtKeep
@@ -4512,6 +4517,9 @@ end
module Proof_global :
sig
+
+ type state
+
type proof_mode = {
name : string;
set : unit -> unit ;
@@ -5787,6 +5795,16 @@ end
module Vernacentries :
sig
+
+ 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) *)
+ }
+
+ 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
@@ -5814,11 +5832,11 @@ end
module Stm :
sig
type doc
- type state
val get_doc : Feedback.doc_id -> doc
+
val state_of_id : doc:doc ->
- Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
+ Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ]
end
(************************************************************************)
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index bc7146884..ea412a7d6 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -502,7 +502,7 @@ type vernac_type =
| VtProofStep of proof_step
| VtProofMode of string
| VtQuery of vernac_part_of_script * Feedback.route_id
- | VtBack of vernac_part_of_script * Stateid.t
+ | VtMeta
| VtUnknown
and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
and vernac_start = string * opacity_guarantee * Id.t list
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/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index b46556ea6..01b75e496 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -46,7 +46,7 @@ let simple_goal sigma g gs =
let is_focused_goal_simple ~doc id =
match state_of_id ~doc id with
| `Expired | `Error _ | `Valid None -> `Not
- | `Valid (Some { proof }) ->
+ | `Valid (Some { Vernacentries.proof }) ->
let proof = Proof_global.proof_of_state proof in
let focused, r1, r2, r3, sigma = Proof.proof proof in
let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
diff --git a/stm/stm.ml b/stm/stm.ml
index d1693519d..84a4c5cc5 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -22,7 +22,18 @@ open Pp
open CErrors
open Feedback
open Vernacexpr
-open Vernac_classifier
+
+(* 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
@@ -138,10 +149,12 @@ type step =
| `Qed of qed_t * Stateid.t
| `Sideff of seff_t * Stateid.t
| `Alias of alias_t ]
+
type visit = { step : step; next : Stateid.t }
let mkTransTac cast cblock cqueue =
Cmd { ctac = true; cast; cblock; cqueue; cids = []; ceff = false }
+
let mkTransCmd cast cids ceff cqueue =
Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff }
@@ -152,14 +165,11 @@ let summary_pstate = [ Evarutil.meta_counter_summary_name;
type cached_state =
| Empty
| Error of Exninfo.iexn
- | Valid of state
-and 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) *)
-}
+ | Valid of Vernacentries.interp_state
+
type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info
type backup = { mine : branch; others : branch list }
+
type 'vcs state_info = { (* TODO: Make this record private to VCS *)
mutable n_reached : int; (* debug cache: how many times was computed *)
mutable n_goals : int; (* open goals: indentation *)
@@ -715,6 +725,7 @@ module State : sig
?safe_id:Stateid.t ->
?redefine:bool -> ?cache:Summary.marshallable ->
?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit
+
val fix_exn_ref : (Exninfo.iexn -> Exninfo.iexn) ref
val install_cached : Stateid.t -> unit
@@ -722,16 +733,18 @@ module State : sig
val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool
val exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn
+
(* to send states across worker/master *)
- type frozen_state
- val get_cached : Stateid.t -> frozen_state
- val same_env : frozen_state -> frozen_state -> bool
+ val get_cached : Stateid.t -> Vernacentries.interp_state
+ val same_env : Vernacentries.interp_state -> Vernacentries.interp_state -> bool
type proof_part
+
type partial_state =
- [ `Full of frozen_state
- | `Proof of Stateid.t * proof_part ]
- val proof_part_of_frozen : frozen_state -> proof_part
+ [ `Full of Vernacentries.interp_state
+ | `ProofOnly of Stateid.t * proof_part ]
+
+ val proof_part_of_frozen : Vernacentries.interp_state -> proof_part
val assign : Stateid.t -> partial_state -> unit
(* Handlers for initial state, prior to document creation. *)
@@ -742,39 +755,29 @@ module State : sig
be removed in the state handling refactoring. *)
val cur_id : Stateid.t ref
-
end = struct (* {{{ *)
+ open Vernacentries
+
(* 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)
- (* helpers *)
- let freeze_global_state marshallable =
- { system = States.freeze ~marshallable;
- proof = Proof_global.freeze ~marshallable;
- shallow = (marshallable = `Shallow) }
- let unfreeze_global_state { system; proof } =
- States.unfreeze system; Proof_global.unfreeze proof
-
- (* hack to make futures functional *)
- let () = Future.set_freeze
- (fun () -> Obj.magic (freeze_global_state `No, !cur_id))
- (fun t -> let s,i = Obj.magic t in unfreeze_global_state s; cur_id := i)
-
- type frozen_state = state
type proof_part =
Proof_global.state * Summary.frozen_bits (* only meta counters *)
+
type partial_state =
- [ `Full of frozen_state
- | `Proof of Stateid.t * proof_part ]
- let proof_part_of_frozen { proof; system } =
+ [ `Full of Vernacentries.interp_state
+ | `ProofOnly of Stateid.t * proof_part ]
+
+ let proof_part_of_frozen { Vernacentries.proof; system } =
proof,
Summary.project_summary (States.summary_of_state system) summary_pstate
let freeze marshallable id =
- VCS.set_state id (Valid (freeze_global_state marshallable))
+ VCS.set_state id (Valid (Vernacentries.freeze_interp_state marshallable))
+
let freeze_invalid id iexn = VCS.set_state id (Error iexn)
let is_cached ?(cache=`No) id only_valid =
@@ -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 unfreeze_global_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 ()
@@ -819,13 +826,13 @@ end = struct (* {{{ *)
try
let prev = (VCS.visit id).next in
if is_cached_and_valid prev
- then { s with proof =
+ then { s with Vernacentries.proof =
Proof_global.copy_terminators
~src:(get_cached prev).proof ~tgt:s.proof }
else s
with VCS.Expired -> s in
VCS.set_state id (Valid s)
- | `Proof(ontop,(pstate,counters)) ->
+ | `ProofOnly(ontop,(pstate,counters)) ->
if is_cached_and_valid ontop then
let s = get_cached ontop in
let s = { s with proof =
@@ -895,11 +902,11 @@ end = struct (* {{{ *)
let init_state = ref None
let register_root_state () =
- init_state := Some (freeze_global_state `No)
+ init_state := Some (Vernacentries.freeze_interp_state `No)
let restore_root_state () =
cur_id := Stateid.dummy;
- unfreeze_global_state Option.(get !init_state)
+ Vernacentries.unfreeze_interp_state (Option.get !init_state);
end (* }}} *)
@@ -994,7 +1001,7 @@ end
(* Wrapper for Vernacentries.interp to set the feedback id *)
(* It is currently called 19 times, this number should be certainly
reduced... *)
-let stm_vernac_interp ?proof id ?route { verbose; loc; expr } =
+let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacentries.interp_state =
(* The Stm will gain the capability to interpret commmads affecting
the whole document state, such as backtrack, etc... so we start
to design the stm command interpreter now *)
@@ -1011,18 +1018,18 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } =
| VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> is_filtered_command e
| _ -> false
in
- let aux_interp cmd =
+ let aux_interp st cmd =
if is_filtered_command cmd then
- stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr)
+ (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
else match cmd with
- | VernacShow ShowScript -> ShowScript.show_script ()
+ | VernacShow ShowScript -> ShowScript.show_script (); st
| expr ->
stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
- try Vernacentries.interp ?verbosely:(Some verbose) ?proof (Loc.tag ?loc expr)
+ try Vernacentries.interp ?verbosely:(Some verbose) ?proof st (Loc.tag ?loc expr)
with e ->
let e = CErrors.push e in
Exninfo.iraise Hooks.(call_process_error_once e)
- in aux_interp expr
+ in aux_interp st expr
(****************************** CRUFT *****************************************)
(******************************************************************************)
@@ -1036,8 +1043,8 @@ module Backtrack : sig
(* we could navigate the dag, but this ways easy *)
val branches_of : Stateid.t -> backup
- (* To be installed during initialization *)
- val undo_vernac_classifier : vernac_expr -> vernac_classification
+ (* Returns the state that the command should backtract to *)
+ val undo_vernac_classifier : vernac_expr -> Stateid.t * vernac_when
end = struct (* {{{ *)
@@ -1105,7 +1112,7 @@ end = struct (* {{{ *)
try
match v with
| VernacResetInitial ->
- VtBack (true, Stateid.initial), VtNow
+ Stateid.initial, VtNow
| VernacResetName (_,name) ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
(try
@@ -1113,20 +1120,20 @@ end = struct (* {{{ *)
fold_until (fun b (id,_,label,_,_) ->
if b then `Stop id else `Cont (List.mem name label))
false id in
- VtBack (true, oid), VtNow
+ oid, VtNow
with Not_found ->
- VtBack (true, id), VtNow)
+ id, VtNow)
| VernacBack n ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let oid = fold_until (fun n (id,_,_,_,_) ->
if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
- VtBack (true, oid), VtNow
+ oid, VtNow
| VernacUndo n ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let oid = fold_until (fun n (id,_,_,tactic,undo) ->
let value = (if tactic then 1 else 0) - undo in
if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in
- VtBack (true, oid), VtLater
+ oid, VtLater
| VernacUndoTo _
| VernacRestart as e ->
let m = match e with VernacUndoTo m -> m | _ -> 0 in
@@ -1143,17 +1150,17 @@ end = struct (* {{{ *)
0 id in
let oid = fold_until (fun n (id,_,_,_,_) ->
if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in
- VtBack (true, oid), VtLater
+ oid, VtLater
| VernacAbortAll ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let oid = fold_until (fun () (id,vcs,_,_,_) ->
match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
() id in
- VtBack (true, oid), VtLater
+ oid, VtLater
| VernacBacktrack (id,_,_)
| VernacBackTo id ->
- VtBack (VCS.is_interactive () = `Yes, Stateid.of_int id), VtNow
- | _ -> VtUnknown, VtNow
+ Stateid.of_int id, VtNow
+ | _ -> anomaly Pp.(str "incorrect VtMeta classification")
with
| Not_found ->
CErrors.user_err ~hdr:"undo_vernac_classifier"
@@ -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)
+ ~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 ->
@@ -1457,7 +1474,7 @@ end = struct (* {{{ *)
let perform_states query =
if query = [] then [] else
- let is_tac e = match classify_vernac e with
+ let is_tac e = match Vernac_classifier.classify_vernac e with
| VtProofStep _, _ -> true
| _ -> false
in
@@ -1480,7 +1497,7 @@ end = struct (* {{{ *)
| _, None -> None
| Some (prev, o, `Cmd { cast = { expr }}), Some n
when is_tac expr && State.same_env o n -> (* A pure tactic *)
- Some (id, `Proof (prev, State.proof_part_of_frozen n))
+ Some (id, `ProofOnly (prev, State.proof_part_of_frozen n))
| Some _, Some s ->
msg_debug (Pp.str "STM: sending back a fat state");
Some (id, `Full s)
@@ -1575,9 +1592,16 @@ end = struct (* {{{ *)
(* We jump at the beginning since the kernel handles side effects by also
* looking at the ones that happen to be present in the current env *)
Reach.known_state ~cache:`No start;
- stm_vernac_interp stop ~proof
+ (* STATE SPEC:
+ * - start: First non-expired state! [This looks very fishy]
+ * - end : start + qed
+ * => takes nothing from the itermediate states.
+ *)
+ (* 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))) };
+ expr = (VernacEndProof (Proved (Opaque,None))) });
`OK proof
end
with e ->
@@ -1633,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;
@@ -1812,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
@@ -1826,7 +1849,14 @@ end = struct (* {{{ *)
else begin
let (i, ast) = r_ast in
Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p);
- stm_vernac_interp r_state_fb ast;
+ (* STATE SPEC:
+ * - start : id
+ * - return: id
+ * => captures state id in a future closure, which will
+ discard execution state but for the proof + univs.
+ *)
+ 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
@@ -1865,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 ->
@@ -1957,8 +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
- stm_vernac_interp r_for { r_what with verbose = true };
+ (* STATE SPEC:
+ * - start: r_where
+ * - end : after execution of r_what
+ *)
+ 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
@@ -2166,14 +2203,20 @@ let known_state ?(redefine_qed=false) ~cache id =
Proofview.give_up else Proofview.tclUNIT ()
end in
match (VCS.get_info base_state).state with
- | Valid { proof } ->
+ | Valid { Vernacentries.proof } ->
Proof_global.unfreeze proof;
Proof_global.with_current_proof (fun _ p ->
feedback ~id:id Feedback.AddedAxiom;
fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ());
- Option.iter (fun expr -> stm_vernac_interp id {
+ (* STATE SPEC:
+ * - start: Modifies the input state adding a proof.
+ * - end : maybe after recovery command.
+ *)
+ (* 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 })
+ strlen = 0 } ))
recovery_command
| _ -> assert false
end
@@ -2211,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 =
@@ -2247,7 +2292,10 @@ 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;
- stm_vernac_interp id 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
| `Cmd { cast = x; ceff = eff } -> (fun () ->
@@ -2255,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);
- stm_vernac_interp id 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;
- stm_vernac_interp id 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 stm_vernac_interp id 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
@@ -2316,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;
- stm_vernac_interp id ~proof 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; stm_vernac_interp id 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;
@@ -2344,7 +2401,8 @@ let known_state ?(redefine_qed=false) ~cache id =
if keep != VtKeepAsAxiom then
reach view.next;
let wall_clock2 = Unix.gettimeofday () in
- stm_vernac_interp id ?proof 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));
@@ -2360,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; stm_vernac_interp id 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;
@@ -2414,7 +2475,6 @@ let new_doc { doc_type ; require_libs } =
State.restore_root_state ();
let doc = VCS.init doc_type Stateid.initial in
- set_undo_classifier Backtrack.undo_vernac_classifier;
begin match doc_type with
| Interactive ln ->
@@ -2505,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
@@ -2515,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
@@ -2545,7 +2605,7 @@ let merge_proof_branch ~valid ?id qast keep brname =
VCS.rewrite_merge qed_id ~ours:(Qed (qed ofp)) ~at:master_id brname;
VCS.delete_branch brname;
VCS.gc ();
- Reach.known_state ~redefine_qed:true ~cache:`No qed_id;
+ let _st = Reach.known_state ~redefine_qed:true ~cache:`No qed_id in
VCS.checkout VCS.Branch.master;
`Unfocus qed_id
| { VCS.kind = `Master } ->
@@ -2578,7 +2638,38 @@ let snapshot_vio ~doc ldir long_f_dot_vo =
let reset_task_queue = Slaves.reset_task_queue
(* Document building *)
-let process_transaction ?(newtip=Stateid.fresh ())
+let process_back_meta_command ~part_of_script ~newtip ~head oid aast w =
+ match part_of_script, w with
+ | true, w ->
+ let id = VCS.new_node ~id:newtip () in
+ let { mine; others } = Backtrack.branches_of oid in
+ let valid = VCS.get_branch_pos head in
+ List.iter (fun branch ->
+ if not (List.mem_assoc branch (mine::others)) then
+ ignore(merge_proof_branch ~valid aast VtDrop branch))
+ (VCS.branches ());
+ VCS.checkout_shallowest_proof_branch ();
+ let head = VCS.current_branch () in
+ List.iter (fun b ->
+ if not(VCS.Branch.equal b head) then begin
+ VCS.checkout b;
+ VCS.commit (VCS.new_node ()) (Alias (oid,aast));
+ end)
+ (VCS.branches ());
+ VCS.checkout_shallowest_proof_branch ();
+ VCS.commit id (Alias (oid,aast));
+ Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
+
+ | false, VtNow ->
+ stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string oid);
+ Backtrack.backto oid;
+ VCS.checkout_shallowest_proof_branch ();
+ Reach.known_state ~cache:(VCS.is_interactive ()) oid; `Ok
+
+ | false, VtLater ->
+ anomaly(str"undo classifier: VtMeta + VtLater must imply part_of_script.")
+
+let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
({ verbose; loc; expr } as x) c =
stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
let vcs = VCS.backup () in
@@ -2587,47 +2678,22 @@ let process_transaction ?(newtip=Stateid.fresh ())
VCS.checkout head;
let rc = begin
stm_prerr_endline (fun () ->
- " classified as: " ^ string_of_vernac_classification c);
+ " classified as: " ^ Vernac_classifier.string_of_vernac_classification c);
match c with
- (* Back *)
- | VtBack (true, oid), w ->
- let id = VCS.new_node ~id:newtip () in
- let { mine; others } = Backtrack.branches_of oid in
- let valid = VCS.get_branch_pos head in
- List.iter (fun branch ->
- if not (List.mem_assoc branch (mine::others)) then
- ignore(merge_proof_branch ~valid x VtDrop branch))
- (VCS.branches ());
- VCS.checkout_shallowest_proof_branch ();
- let head = VCS.current_branch () in
- List.iter (fun b ->
- if not(VCS.Branch.equal b head) then begin
- VCS.checkout b;
- VCS.commit (VCS.new_node ()) (Alias (oid,x));
- end)
- (VCS.branches ());
- VCS.checkout_shallowest_proof_branch ();
- VCS.commit id (Alias (oid,x));
- Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
- | VtBack (false, id), VtNow ->
- stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
- Backtrack.backto id;
- VCS.checkout_shallowest_proof_branch ();
- Reach.known_state ~cache:(VCS.is_interactive ()) id; `Ok
- | VtBack (false, id), VtLater ->
- anomaly(str"classifier: VtBack + VtLater must imply part_of_script.")
-
+ (* Meta *)
+ | VtMeta, _ ->
+ let id, w = Backtrack.undo_vernac_classifier expr in
+ process_back_meta_command ~part_of_script ~newtip ~head id x w
(* Query *)
- | VtQuery (false, route), VtNow ->
- begin
- let query_sid = VCS.cur_tip () in
- try stm_vernac_interp ~route (VCS.cur_tip ()) x
- with e ->
- let e = CErrors.push e in
- Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e)
- end; `Ok
- (* Part of the script commands don't set the query route *)
- | VtQuery (true, _route), w ->
+ | VtQuery (false,route), VtNow ->
+ let query_sid = VCS.cur_tip () in
+ (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
+ | VtQuery (true, route), w ->
let id = VCS.new_node ~id:newtip () in
let queue =
if !Flags.async_proofs_full then `QueryQueue (ref false)
@@ -2696,7 +2762,9 @@ let process_transaction ?(newtip=Stateid.fresh ())
(* Side effect on all branches *)
| VtUnknown, _ when expr = VernacToplevelControl Drop ->
- stm_vernac_interp (VCS.get_branch_pos head) 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
@@ -2717,12 +2785,13 @@ let process_transaction ?(newtip=Stateid.fresh ())
let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
let id = VCS.new_node ~id:newtip () in
let head_id = VCS.get_branch_pos head in
- Reach.known_state ~cache:`Yes head_id; (* ensure it is ok *)
+ let _st = Reach.known_state ~cache:`Yes head_id in (* ensure it is ok *)
let step () =
VCS.checkout VCS.Branch.master;
let mid = VCS.get_branch_pos VCS.Branch.master in
- Reach.known_state ~cache:(VCS.is_interactive ()) mid;
- stm_vernac_interp id x;
+ let _st' = Reach.known_state ~cache:(VCS.is_interactive ()) mid in
+ 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
@@ -2854,7 +2923,7 @@ let add ~doc ~ontop ?newtip verb (loc, ast) =
let indentation, strlen = compute_indentation ?loc ontop in
CWarnings.set_current_loc loc;
(* XXX: Classifiy vernac should be moved inside process transaction *)
- let clas = classify_vernac ast in
+ let clas = Vernac_classifier.classify_vernac ast in
let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in
match process_transaction ?newtip aast clas with
| `Ok -> doc, VCS.cur_tip (), `NewTip
@@ -2869,17 +2938,17 @@ 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
let indentation, strlen = compute_indentation ?loc at in
CWarnings.set_current_loc loc;
- let clas = classify_vernac ast in
+ let clas = Vernac_classifier.classify_vernac ast in
let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
match clas with
- | VtBack (_,id), _ -> (* TODO: can this still happen ? *)
- ignore(process_transaction aast (VtBack (false,id), VtNow))
+ | VtMeta , _ -> (* TODO: can this still happen ? *)
+ ignore(process_transaction ~part_of_script:false aast (VtMeta,VtNow))
| _ ->
ignore(process_transaction aast (VtQuery (false, route), VtNow)))
s
diff --git a/stm/stm.mli b/stm/stm.mli
index c65cf6a9a..31f4599d3 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -217,16 +217,10 @@ val state_ready_hook : (Stateid.t -> unit) Hook.t
(* Messages from the workers to the master *)
val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
-type state = {
- system : States.state;
- proof : Proof_global.state;
- shallow : bool
-}
-
val get_doc : Feedback.doc_id -> doc
val state_of_id : doc:doc ->
- Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
+ Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ]
(* Queries for backward compatibility *)
val current_proof_depth : doc:doc -> int
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 158ad9084..3aa2cd707 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -31,7 +31,7 @@ let string_of_vernac_type = function
Option.default "" proof_block_detection
| VtProofMode s -> "ProofMode " ^ s
| VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route
- | VtBack (b, _) -> "Stm Back " ^ string_of_in_script b
+ | VtMeta -> "Meta "
let string_of_vernac_when = function
| VtLater -> "Later"
@@ -53,9 +53,6 @@ let make_polymorphic (a, b as x) =
VtStartProof (x, Doesn'tGuaranteeOpacity, ids), b
| _ -> x
-let undo_classifier = ref (fun _ -> assert false)
-let set_undo_classifier f = undo_classifier := f
-
let rec classify_vernac e =
let static_classifier e = match e with
(* Univ poly compatibility: we run it now, so that we can just
@@ -75,7 +72,7 @@ let rec classify_vernac e =
| VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
(match classify_vernac e with
| ( VtQuery _ | VtProofStep _ | VtSideff _
- | VtBack _ | VtProofMode _ ), _ as x -> x
+ | VtProofMode _ | VtMeta), _ as x -> x
| VtQed _, _ ->
VtProofStep { parallel = `No; proof_block_detection = None },
VtNow
@@ -191,7 +188,7 @@ let rec classify_vernac e =
| VernacBack _ | VernacAbortAll
| VernacUndoTo _ | VernacUndo _
| VernacResetName _ | VernacResetInitial
- | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e
+ | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow
(* What are these? *)
| VernacToplevelControl _
| VernacRestoreState _
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
index 2fa1e0b8d..fe42a03a3 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/vernac_classifier.mli
@@ -18,9 +18,6 @@ val classify_vernac : vernac_expr -> vernac_classification
val declare_vernac_classifier :
Vernacexpr.extend_name -> (raw_generic_argument list -> unit -> vernac_classification) -> unit
-(** Set by Stm *)
-val set_undo_classifier : (vernac_expr -> vernac_classification) -> unit
-
(** Standard constant classifiers *)
val classify_as_query : vernac_classification
val classify_as_sideeff : vernac_classification
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index d736975d3..cf63fbdc3 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -119,7 +119,7 @@ let rec interp_vernac ~check ~interactive doc sid (loc,com) =
(* XXX: We need to run this before add as the classification is
highly dynamic and depends on the structure of the
- document. Hopefully this is fixed when VtBack can be removed
+ document. Hopefully this is fixed when VtMeta can be removed
and Undo etc... are just interpreted regularly. *)
(* XXX: The classifier can emit warnings so we need to guard
@@ -127,7 +127,7 @@ let rec interp_vernac ~check ~interactive doc sid (loc,com) =
let wflags = CWarnings.get_flags () in
CWarnings.set_flags "none";
let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with
- | VtProofStep _ | VtBack (_, _) | VtStartProof _ -> true
+ | VtProofStep _ | VtMeta | VtStartProof _ -> true
| _ -> false
in
CWarnings.set_flags wflags;
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 66427b709..b7a861214 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2148,23 +2148,48 @@ 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) *)
+}
+
+let s_cache = ref (States.freeze ~marshallable:`No)
+let s_proof = ref (Proof_global.freeze ~marshallable:`No)
+
+let invalidate_cache () =
+ s_cache := Obj.magic 0;
+ s_proof := Obj.magic 0
+
+let freeze_interp_state marshallable =
+ { system = (s_cache := States.freeze ~marshallable; !s_cache);
+ proof = (s_proof := Proof_global.freeze ~marshallable; !s_proof);
+ shallow = marshallable = `Shallow }
+
+let unfreeze_interp_state { system; proof } =
+ if (!s_cache != system) then (s_cache := system; States.unfreeze system);
+ if (!s_proof != proof) then (s_proof := proof; 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 XXX Careful here with the cache! *)
+ invalidate_cache ();
+ unfreeze_interp_state st;
let (e, _) = CErrors.push e in
match e with
| HasNotFailed ->
@@ -2175,7 +2200,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 +2213,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
@@ -2227,3 +2252,8 @@ let interp ?(verbosely=true) ?proof (loc,c) =
in
if verbosely then Flags.verbosely (aux false) c
else aux false c
+
+let interp ?verbosely ?proof st cmd =
+ unfreeze_interp_state st;
+ interp ?verbosely ?proof st cmd;
+ freeze_interp_state `No
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index a09011d24..56635c801 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -14,11 +14,21 @@ val dump_global : Libnames.reference or_by_notation -> unit
val vernac_require :
Libnames.reference option -> bool option -> Libnames.reference list -> unit
+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) *)
+}
+
+val freeze_interp_state : Summary.marshallable -> interp_state
+val unfreeze_interp_state : interp_state -> unit
+
(** The main interpretation function of vernacular expressions *)
val interp :
?verbosely:bool ->
?proof:Proof_global.closed_proof ->
- Vernacexpr.vernac_expr Loc.located -> unit
+ interp_state ->
+ Vernacexpr.vernac_expr Loc.located -> interp_state
(** Prepare a "match" template for a given inductive type.
For each branch of the match, we list the constructor name
@@ -28,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-06-16 21:29:54 +0000