From 17f3346c5c42c16eed58bf2325aa996c3892a5e9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 11 May 2016 14:53:46 +0200
Subject: STM: invalid states are first class citizens
A state in the cache (document node) is now one of "Empty | Error | Valid".
This paves the way to commands/blocks-of-commands resilient-to/confining
errors: one can catch and "ignore" the exception obtained by reaching the
previous state and do something sensible, like running anyway the command
or skipping until the end of an error-confining block is reached.
Invalid states carry an enriched exception with the safe_id attached, so
that if one edits_at or observe them gets a safe place to land (CoqIDE
needs such piece of info).
Little API change in Stm.state_of_id now returning a `Error variant for
the new kind of state.
---
stm/stm.ml | 135 ++++++++++++++++++++++++++++++++++--------------------------
stm/stm.mli | 2 +-
2 files changed, 78 insertions(+), 59 deletions(-)
diff --git a/stm/stm.ml b/stm/stm.ml
index e2acb10293..1dd089a26c 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -187,20 +187,24 @@ let summary_pstate = [ Evarutil.meta_counter_summary_name;
Evd.evar_counter_summary_name;
"program-tcc-table" ]
type state = {
- system : States.state;
- proof : Proof_global.state;
- shallow : bool
+ system : States.state; (* summary + libstack *)
+ proof : Proof_global.state; (* proof state *)
+ shallow : bool (* is the state trimmed down (libstack) *)
}
+type cached_state =
+ | Empty
+ | Error of Exninfo.iexn
+ | Valid of state
type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info
type backup = { mine : branch; others : branch list }
-type 'vcs state_info = { (* Make private *)
- mutable n_reached : int;
- mutable n_goals : int;
- mutable state : state option;
+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 *)
+ mutable state : cached_state; (* state value *)
mutable vcs_backup : 'vcs option * backup option;
}
let default_info () =
- { n_reached = 0; n_goals = 0; state = None; vcs_backup = None,None }
+ { n_reached = 0; n_goals = 0; state = Empty; vcs_backup = None,None }
(* Functions that work on a Vcs with a specific branch type *)
module Vcs_aux : sig
@@ -296,10 +300,10 @@ module VCS : sig
val cur_tip : unit -> id
val get_info : id -> vcs state_info
- val reached : id -> bool -> unit
+ val reached : id -> unit
val goals : id -> int -> unit
- val set_state : id -> state -> unit
- val get_state : id -> state option
+ val set_state : id -> cached_state -> unit
+ val get_state : id -> cached_state
(* cuts from start -> stop, raising Expired if some nodes are not there *)
val slice : start:id -> stop:id -> vcs
@@ -345,11 +349,11 @@ end = struct (* {{{ *)
| Qed { qast } -> string_of_ppcmds (pr_ast qast) in
let is_green id =
match get_info vcs id with
- | Some { state = Some _ } -> true
+ | Some { state = Valid _ } -> true
| _ -> false in
let is_red id =
match get_info vcs id with
- | Some s -> Int.equal s.n_reached ~-1
+ | Some { state = Error _ } -> true
| _ -> false in
let head = current_branch vcs in
let heads =
@@ -452,13 +456,12 @@ end = struct (* {{{ *)
| Some x -> x
| None -> raise Vcs_aux.Expired
let set_state id s =
- (get_info id).state <- Some s;
+ (get_info id).state <- s;
if Flags.async_proofs_is_master () then Hooks.(call state_ready id)
let get_state id = (get_info id).state
- let reached id b =
+ let reached id =
let info = get_info id in
- if b then info.n_reached <- info.n_reached + 1
- else info.n_reached <- -1
+ info.n_reached <- info.n_reached + 1
let goals id n = (get_info id).n_goals <- n
let cur_tip () = get_branch_pos (current_branch ())
@@ -508,7 +511,7 @@ end = struct (* {{{ *)
let l = nodes_in_slice ~start ~stop in
let copy_info v id =
Vcs_.set_info v id
- { (get_info id) with state = None; vcs_backup = None,None } in
+ { (get_info id) with state = Empty; vcs_backup = None,None } in
let copy_info_w_state v id =
Vcs_.set_info v id { (get_info id) with vcs_backup = None,None } in
let v = Vcs_.empty start in
@@ -518,11 +521,12 @@ end = struct (* {{{ *)
let v = copy_info v id in
v) l v in
(* Stm should have reached the beginning of proof *)
- assert (not (Option.is_empty (get_info start).state));
+ assert (match (get_info start).state with Valid _ -> true | _ -> false);
(* We put in the new dag the most recent state known to master *)
let rec fill id =
- if (get_info id).state = None then fill (Vcs_aux.visit v id).next
- else copy_info_w_state v id in
+ match (get_info id).state with
+ | Empty | Error _ -> fill (Vcs_aux.visit v id).next
+ | Valid _ -> copy_info_w_state v id in
let v = fill stop in
(* We put in the new dag the first state (since Qed shall run on it,
* see check_task_aux) *)
@@ -596,7 +600,10 @@ end = struct (* {{{ *)
end (* }}} *)
let state_of_id id =
- try `Valid (VCS.get_info id).state
+ try match (VCS.get_info id).state with
+ | Valid s -> `Valid (Some s)
+ | Error (e,_) -> `Error e
+ | Empty -> `Valid None
with VCS.Expired -> `Expired
@@ -616,6 +623,7 @@ module State : sig
val install_cached : Stateid.t -> unit
val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool
+ val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool
val exn_on : Stateid.t -> ?valid:Stateid.t -> iexn -> iexn
@@ -661,51 +669,60 @@ end = struct (* {{{ *)
proof,
Summary.project_summary (States.summary_of_state system) summary_pstate
- let freeze marshallable id = VCS.set_state id (freeze_global_state marshallable)
+ let freeze marshallable id =
+ VCS.set_state id (Valid (freeze_global_state marshallable))
+ let freeze_invalid id iexn = VCS.set_state id (Error iexn)
- let is_cached ?(cache=`No) id =
+ let is_cached ?(cache=`No) id only_valid =
if Stateid.equal id !cur_id then
try match VCS.get_info id with
- | { state = None } when cache = `Yes -> freeze `No id; true
- | { state = None } when cache = `Shallow -> freeze `Shallow id; true
+ | { state = Empty } when cache = `Yes -> freeze `No id; true
+ | { state = Empty } when cache = `Shallow -> freeze `Shallow id; true
| _ -> true
with VCS.Expired -> false
else
try match VCS.get_info id with
- | { state = Some _ } -> true
- | _ -> false
+ | { state = Empty } -> false
+ | { state = Valid _ } -> true
+ | { state = Error _ } -> not only_valid
with VCS.Expired -> false
+ let is_cached_and_valid ?cache id = is_cached ?cache id true
+ let is_cached ?cache id = is_cached ?cache id false
+
let install_cached id =
- if Stateid.equal id !cur_id then () else (* optimization *)
- let s =
- match VCS.get_info id with
- | { state = Some s } -> s
- | _ -> anomaly (str "unfreezing a non existing state") in
- unfreeze_global_state s; cur_id := 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
+ | _ ->
+ (* coqc has a 1 slot cache and only for valid states *)
+ if interactive () = `No && Stateid.equal id !cur_id then ()
+ else anomaly (str "installing a non cached state")
let get_cached id =
try match VCS.get_info id with
- | { state = Some s } -> s
+ | { state = Valid s } -> s
| _ -> anomaly (str "not a cached state")
with VCS.Expired -> anomaly (str "not a cached state (expired)")
let assign id what =
- if VCS.get_state id <> None then () else
+ if VCS.get_state id <> Empty then () else
try match what with
| `Full s ->
let s =
try
let prev = (VCS.visit id).next in
- if is_cached prev
+ if is_cached_and_valid prev
then { s with proof =
Proof_global.copy_terminators
~src:(get_cached prev).proof ~tgt:s.proof }
else s
with VCS.Expired -> s in
- VCS.set_state id s
+ VCS.set_state id (Valid s)
| `Proof(ontop,(pstate,counters)) ->
- if is_cached ontop then
+ if is_cached_and_valid ontop then
let s = get_cached ontop in
let s = { s with proof =
Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in
@@ -714,7 +731,7 @@ end = struct (* {{{ *)
(Summary.surgery_summary
(States.summary_of_state s.system)
counters) } in
- VCS.set_state id s
+ VCS.set_state id (Valid s)
with VCS.Expired -> ()
let exn_on id ?valid (e, info) =
@@ -753,20 +770,22 @@ end = struct (* {{{ *)
cur_id := id;
if feedback_processed then
Hooks.(call state_computed id ~in_cache:false);
- VCS.reached id true;
+ VCS.reached id;
if Proof_global.there_are_pending_proofs () then
VCS.goals id (Proof_global.get_open_goals ())
with e ->
let (e, info) = Errors.push e in
let good_id = !cur_id in
- cur_id := Stateid.dummy;
- VCS.reached id false;
- Hooks.(call unreachable_state id (e, info));
- match Stateid.get info, safe_id with
- | None, None -> iraise (exn_on id ~valid:good_id (e, info))
- | None, Some good_id -> iraise (exn_on id ~valid:good_id (e, info))
- | Some _, None -> iraise (e, info)
- | Some (_,at), Some id -> iraise (e, Stateid.add info ~valid:id at)
+ VCS.reached id;
+ let ie =
+ match Stateid.get info, safe_id with
+ | None, None -> (exn_on id ~valid:good_id (e, info))
+ | None, Some good_id -> (exn_on id ~valid:good_id (e, info))
+ | Some _, None -> (e, info)
+ | Some (_,at), Some id -> (e, Stateid.add info ~valid:id at) in
+ if cache = `Yes || cache = `Shallow then freeze_invalid id ie;
+ Hooks.(call unreachable_state id ie);
+ Exninfo.iraise ie
end (* }}} *)
@@ -842,7 +861,7 @@ end = struct (* {{{ *)
let back_safe () =
let id =
fold_until (fun n (id,_,_,_,_) ->
- if n >= 0 && State.is_cached id then `Stop id else `Cont (succ n))
+ if n >= 0 && State.is_cached_and_valid id then `Stop id else `Cont (succ n))
0 (VCS.get_branch_pos (VCS.current_branch ())) in
backto id
@@ -1133,7 +1152,7 @@ end = struct (* {{{ *)
let e_msg = iprint (e, info) in
prerr_endline (fun () -> "failed with the following exception:");
prerr_endline (fun () -> string_of_ppcmds e_msg);
- let e_safe_states = List.filter State.is_cached my_states in
+ let e_safe_states = List.filter State.is_cached_and_valid my_states in
RespError { e_error_at; e_safe_id; e_msg; e_safe_states }
let perform_states query =
@@ -1151,12 +1170,12 @@ end = struct (* {{{ *)
let prev =
try
let { next = prev; step } = VCS.visit id in
- if State.is_cached prev && List.mem prev seen
+ if State.is_cached_and_valid prev && List.mem prev seen
then Some (prev, State.get_cached prev, step)
else None
with VCS.Expired -> None in
let this =
- if State.is_cached id then Some (State.get_cached id) else None in
+ if State.is_cached_and_valid id then Some (State.get_cached id) else None in
match prev, this with
| _, None -> None
| Some (prev, o, `Cmd { cast = { expr }}), Some n
@@ -1724,7 +1743,7 @@ let collect_proof keep cur hd brkind id =
let name = name ids in
`ASync (parent last,proof_using_ast last,accn,name,delegate name)
| `Fork((_, hd', GuaranteesOpacity, ids), _) when
- has_proof_no_using last && not (State.is_cached (parent last)) &&
+ has_proof_no_using last && not (State.is_cached_and_valid (parent last)) &&
!Flags.compilation_mode = Flags.BuildVio ->
assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch);
(try
@@ -1760,7 +1779,7 @@ let collect_proof keep cur hd brkind id =
let rc = collect (Some cur) [] id in
if is_empty rc then make_sync `AlreadyEvaluated rc
else if (keep == VtKeep || keep == VtKeepAsAxiom) &&
- (not(State.is_cached id) || !Flags.async_proofs_full)
+ (not(State.is_cached_and_valid id) || !Flags.async_proofs_full)
then check_policy rc
else make_sync `AlreadyEvaluated rc
@@ -1808,9 +1827,9 @@ let known_state ?(redefine_qed=false) ~cache id =
and reach ?(redefine_qed=false) ?(cache=cache) id =
prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id);
if not redefine_qed && State.is_cached ~cache id then begin
- State.install_cached id;
Hooks.(call state_computed id ~in_cache:true);
- prerr_endline (fun () -> "reached (cache)")
+ prerr_endline (fun () -> "reached (cache)");
+ State.install_cached id
end else
let step, cache_step, feedback_processed =
let view = VCS.visit id in
@@ -1842,7 +1861,7 @@ let known_state ?(redefine_qed=false) ~cache id =
reach view.next; vernac_interp id x;
wall_clock_last_fork := Unix.gettimeofday ()
), `Yes, true
- | `Fork ((x,_,_,_), Some prev) -> (fun () ->
+ | `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *)
reach ~cache:`Shallow prev;
reach view.next;
(try vernac_interp id x;
diff --git a/stm/stm.mli b/stm/stm.mli
index 6ffe0beb44..d825ff33eb 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -122,7 +122,7 @@ type state = {
proof : Proof_global.state;
shallow : bool
}
-val state_of_id : Stateid.t -> [ `Valid of state option | `Expired ]
+val state_of_id : Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
(** read-eval-print loop compatible interface ****************************** **)
--
cgit v1.2.3
From d75da809429d5d2d40d108608db9e5acd9aec9c9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 May 2016 11:08:37 +0200
Subject: STM: support for nested boxes of nodes to model error boundaries
Dag extended to support arbitrary clusters, renamed to Property.
Vcs generalized to not impose the data hold by a Property.
Stm(VCS) names a property "a box" and imposes a topological invariant (no
overlap). It defines 2 kind of boxes: ProofTasks (the old cluster
notion) and ErrorBound (meant to confine errors to sub-proofs).
In the meanwhile more equations added to Make(..) functors in order to
have just one Stateid.Set module around.
---
lib/stateid.ml | 8 ++-
lib/stateid.mli | 3 +-
stm/dag.ml | 94 ++++++++++++++++++++---------------
stm/dag.mli | 50 ++++++++++---------
stm/stm.ml | 151 +++++++++++++++++++++++++++++++++++++++-----------------
stm/vcs.ml | 75 ++++++++++++++--------------
stm/vcs.mli | 66 ++++++++++++++-----------
7 files changed, 269 insertions(+), 178 deletions(-)
diff --git a/lib/stateid.ml b/lib/stateid.ml
index c17df2b321..500581a39e 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -29,7 +29,13 @@ let get exn = Exninfo.get exn state_id_info
let equal = Int.equal
let compare = Int.compare
-module Set = Set.Make(struct type t = int let compare = compare end)
+module Self = struct
+ type t = int
+ let compare = compare
+ let equal = equal
+end
+
+module Set = Set.Make(Self)
type ('a,'b) request = {
exn_info : t * t;
diff --git a/lib/stateid.mli b/lib/stateid.mli
index 516ad891ff..cd8fddf0ce 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -11,7 +11,8 @@ type t
val equal : t -> t -> bool
val compare : t -> t -> int
-module Set : Set.S with type elt = t
+module Self : Map.OrderedType with type t = t
+module Set : Set.S with type elt = t and type t = Set.Make(Self).t
val initial : t
val dummy : t
diff --git a/stm/dag.ml b/stm/dag.ml
index 0c7f9f34bd..99e7c92648 100644
--- a/stm/dag.ml
+++ b/stm/dag.ml
@@ -8,15 +8,6 @@
module type S = sig
- module Cluster :
- sig
- type 'd t
- val equal : 'd t -> 'd t -> bool
- val compare : 'd t -> 'd t -> int
- val to_string : 'd t -> string
- val data : 'd t -> 'd
- end
-
type node
module NodeSet : Set.S with type elt = node
@@ -31,45 +22,57 @@ module type S = sig
val del_nodes : ('e,'i,'d) t -> NodeSet.t -> ('e,'i,'d) t
val all_nodes : ('e,'i,'d) t -> NodeSet.t
- val iter : ('e,'i,'d) t ->
- (node -> 'd Cluster.t option -> 'i option ->
- (node * 'e) list -> unit) -> unit
-
- val create_cluster : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t
- val cluster_of : ('e,'i,'d) t -> node -> 'd Cluster.t option
- val del_cluster : ('e,'i,'d) t -> 'd Cluster.t -> ('e,'i,'d) t
-
val get_info : ('e,'i,'d) t -> node -> 'i option
val set_info : ('e,'i,'d) t -> node -> 'i -> ('e,'i,'d) t
val clear_info : ('e,'i,'d) t -> node -> ('e,'i,'d) t
+ module Property :
+ sig
+ type 'd t
+ val equal : 'd t -> 'd t -> bool
+ val compare : 'd t -> 'd t -> int
+ val to_string : 'd t -> string
+ val data : 'd t -> 'd
+ val having_it : 'd t -> NodeSet.t
+ end
+
+ val create_property : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t
+ val property_of : ('e,'i,'d) t -> node -> 'd Property.t list
+ val del_property : ('e,'i,'d) t -> 'd Property.t -> ('e,'i,'d) t
+
+ val iter : ('e,'i,'d) t ->
+ (node -> 'd Property.t list -> 'i option ->
+ (node * 'e) list -> unit) -> unit
+
end
module Make(OT : Map.OrderedType) = struct
-module Cluster =
+module NodeSet = Set.Make(OT)
+
+module Property =
struct
- type 'd t = 'd * int
- let equal (_,i1) (_,i2) = Int.equal i1 i2
- let compare (_,i1) (_,i2) = Int.compare i1 i2
- let to_string (_,i) = string_of_int i
- let data (d,_) = d
+ type 'd t = { data : 'd; uid : int; having_it : NodeSet.t }
+ let equal { uid = i1 } { uid = i2 } = Int.equal i1 i2
+ let compare { uid = i1 } { uid = i2 } = Int.compare i1 i2
+ let to_string { uid = i } = string_of_int i
+ let data { data = d } = d
+ let having_it { having_it } = having_it
end
type node = OT.t
module NodeMap = CMap.Make(OT)
-module NodeSet = Set.Make(OT)
type ('edge,'info,'data) t = {
graph : (node * 'edge) list NodeMap.t;
- clusters : 'data Cluster.t NodeMap.t;
+ properties : 'data Property.t list NodeMap.t;
infos : 'info NodeMap.t;
}
let empty = {
graph = NodeMap.empty;
- clusters = NodeMap.empty;
+ properties = NodeMap.empty;
infos = NodeMap.empty;
}
@@ -94,7 +97,7 @@ let del_edge dag id tgt = { dag with
let del_nodes dag s = {
infos = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.infos;
- clusters = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.clusters;
+ properties = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.properties;
graph = NodeMap.filter (fun n l ->
let drop = NodeSet.mem n s in
if not drop then
@@ -102,20 +105,31 @@ let del_nodes dag s = {
not drop)
dag.graph }
+let map_add_list k v m =
+ try
+ let l = NodeMap.find k m in
+ NodeMap.add k (v::l) m
+ with Not_found -> NodeMap.add k [v] m
+
let clid = ref 1
-let create_cluster dag l data =
+let create_property dag l data =
incr clid;
- { dag with clusters =
- List.fold_right (fun x clusters ->
- NodeMap.add x (data, !clid) clusters) l dag.clusters }
-
-let cluster_of dag id =
- try Some (NodeMap.find id dag.clusters)
- with Not_found -> None
-
-let del_cluster dag c =
- { dag with clusters =
- NodeMap.filter (fun _ c' -> not (Cluster.equal c' c)) dag.clusters }
+ let having_it = List.fold_right NodeSet.add l NodeSet.empty in
+ let property = { Property.data; uid = !clid; having_it } in
+ { dag with properties =
+ List.fold_right (fun x ps -> map_add_list x property ps) l dag.properties }
+
+let property_of dag id =
+ try NodeMap.find id dag.properties
+ with Not_found -> []
+
+let del_property dag c =
+ { dag with properties =
+ NodeMap.filter (fun _ cl -> cl <> [])
+ (NodeMap.map (fun cl ->
+ List.filter (fun c' ->
+ not (Property.equal c' c)) cl)
+ dag.properties) }
let get_info dag id =
try Some (NodeMap.find id dag.infos)
@@ -126,7 +140,7 @@ let set_info dag id info = { dag with infos = NodeMap.add id info dag.infos }
let clear_info dag id = { dag with infos = NodeMap.remove id dag.infos }
let iter dag f =
- NodeMap.iter (fun k v -> f k (cluster_of dag k) (get_info dag k) v) dag.graph
+ NodeMap.iter (fun k v -> f k (property_of dag k) (get_info dag k) v) dag.graph
let all_nodes dag = NodeMap.domain dag.graph
diff --git a/stm/dag.mli b/stm/dag.mli
index 6b4442df00..e783cd8ee1 100644
--- a/stm/dag.mli
+++ b/stm/dag.mli
@@ -7,19 +7,7 @@
(************************************************************************)
module type S = sig
-
- (* A cluster is just a set of nodes. This set holds some data.
- Stm uses this to group nodes contribution to the same proofs and
- that can be evaluated asynchronously *)
- module Cluster :
- sig
- type 'd t
- val equal : 'd t -> 'd t -> bool
- val compare : 'd t -> 'd t -> int
- val to_string : 'd t -> string
- val data : 'd t -> 'd
- end
-
+
type node
module NodeSet : Set.S with type elt = node
@@ -34,19 +22,35 @@ module type S = sig
val del_nodes : ('e,'i,'d) t -> NodeSet.t -> ('e,'i,'d) t
val all_nodes : ('e,'i,'d) t -> NodeSet.t
- val iter : ('e,'i,'d) t ->
- (node -> 'd Cluster.t option -> 'i option ->
- (node * 'e) list -> unit) -> unit
-
- val create_cluster : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t
- val cluster_of : ('e,'i,'d) t -> node -> 'd Cluster.t option
- val del_cluster : ('e,'i,'d) t -> 'd Cluster.t -> ('e,'i,'d) t
-
val get_info : ('e,'i,'d) t -> node -> 'i option
val set_info : ('e,'i,'d) t -> node -> 'i -> ('e,'i,'d) t
val clear_info : ('e,'i,'d) t -> node -> ('e,'i,'d) t
-end
+ (* A property applies to a set of nodes and holds some data.
+ Stm uses this feature to group nodes contributing to the same proofs and
+ to structure proofs in boxes limiting the scope of errors *)
+ module Property :
+ sig
+ type 'd t
+ val equal : 'd t -> 'd t -> bool
+ val compare : 'd t -> 'd t -> int
+ val to_string : 'd t -> string
+ val data : 'd t -> 'd
+ val having_it : 'd t -> NodeSet.t
+ end
+
+ val create_property : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t
+ val property_of : ('e,'i,'d) t -> node -> 'd Property.t list
+ val del_property : ('e,'i,'d) t -> 'd Property.t -> ('e,'i,'d) t
+
+ val iter : ('e,'i,'d) t ->
+ (node -> 'd Property.t list -> 'i option ->
+ (node * 'e) list -> unit) -> unit
+
+ end
-module Make(OT : Map.OrderedType) : S with type node = OT.t
+module Make(OT : Map.OrderedType) : S
+with type node = OT.t
+and type NodeSet.t = Set.Make(OT).t
+and type NodeSet.elt = OT.t
diff --git a/stm/stm.ml b/stm/stm.ml
index 1dd089a26c..1c8603f0f5 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -140,7 +140,7 @@ let update_global_env () =
if Proof_global.there_are_pending_proofs () then
Proof_global.update_global_env ()
-module Vcs_ = Vcs.Make(Stateid)
+module Vcs_ = Vcs.Make(Stateid.Self)
type future_proof = Proof_global.closed_proof_output Future.computation
type proof_mode = string
type depth = int
@@ -206,15 +206,28 @@ type 'vcs state_info = { (* TODO: Make this record private to VCS *)
let default_info () =
{ n_reached = 0; n_goals = 0; state = Empty; vcs_backup = None,None }
+(* Clusters of nodes implemented as Dag properties. While Dag and Vcs impose
+ * no constraint on properties, here we impose boxes to be non overlapping. *)
+type box =
+ | ProofTask of pt
+ | ErrorBound of eb
+and pt = { (* TODO: inline records in OCaml 4.03 *)
+ start : Stateid.t;
+ qed : Stateid.t;
+}
+and eb = {
+ stuff : unit;
+}
+
(* Functions that work on a Vcs with a specific branch type *)
module Vcs_aux : sig
- val proof_nesting : (branch_type, 't,'i) Vcs_.t -> int
+ val proof_nesting : (branch_type, 't,'i,'c) Vcs_.t -> int
val find_proof_at_depth :
- (branch_type, 't, 'i) Vcs_.t -> int ->
+ (branch_type, 't, 'i,'c) Vcs_.t -> int ->
Vcs_.Branch.t * branch_type Vcs_.branch_info
exception Expired
- val visit : (branch_type, transaction,'i) Vcs_.t -> Vcs_.Dag.node -> visit
+ val visit : (branch_type, transaction,'i,'c) Vcs_.t -> Vcs_.Dag.node -> visit
end = struct (* {{{ *)
@@ -278,7 +291,7 @@ module VCS : sig
pos : id;
}
- type vcs = (branch_type, transaction, vcs state_info) Vcs_.t
+ type vcs = (branch_type, transaction, vcs state_info, box) Vcs_.t
val init : id -> unit
@@ -296,7 +309,7 @@ module VCS : sig
val edit_branch : Branch.t
val branch : ?root:id -> ?pos:id -> Branch.t -> branch_type -> unit
val reset_branch : Branch.t -> id -> unit
- val reachable : id -> Vcs_.NodeSet.t
+ val reachable : id -> Stateid.Set.t
val cur_tip : unit -> id
val get_info : id -> vcs state_info
@@ -309,9 +322,11 @@ module VCS : sig
val slice : start:id -> stop:id -> vcs
val nodes_in_slice : start:id -> stop:id -> Stateid.t list
- val create_cluster : id list -> qed:id -> start:id -> unit
- val cluster_of : id -> (id * id) option
- val delete_cluster_of : id -> unit
+ val create_proof_task_box : id list -> qed:id -> start:id -> unit
+ val create_error_bound_box : id list -> switch:id -> unit
+ val box_of : id -> box list
+ val delete_proof_task_box_of : id -> unit
+ val proof_task_box_of : id -> pt option
val proof_nesting : unit -> int
val checkout_shallowest_proof_branch : unit -> unit
@@ -331,7 +346,6 @@ end = struct (* {{{ *)
include Vcs_
exception Expired = Vcs_aux.Expired
- module StateidSet = Set.Make(Stateid)
open Printf
let print_dag vcs () =
@@ -373,8 +387,6 @@ end = struct (* {{{ *)
let edge tr =
sprintf "<%s>"
(quote (string_of_transaction tr)) in
- let ids = ref StateidSet.empty in
- let clus = Hashtbl.create 13 in
let node_info id =
match get_info vcs id with
| None -> ""
@@ -387,39 +399,66 @@ end = struct (* {{{ *)
let nodefmt oc id =
fprintf oc "%s [label=%s,style=filled,fillcolor=%s];\n"
(node id) (node_info id) (color id) in
- let add_to_clus_or_ids from cf =
- match cf with
- | None -> ids := StateidSet.add from !ids; false
- | Some c -> Hashtbl.replace clus c
- (try let n = Hashtbl.find clus c in from::n
- with Not_found -> [from]); true in
+
+ let ids = ref Stateid.Set.empty in
+ let boxes = ref [] in
+ (* Fill in *)
+ Dag.iter graph (fun from _ _ l ->
+ ids := Stateid.Set.add from !ids;
+ List.iter (fun box -> boxes := box :: !boxes)
+ (Dag.property_of graph from);
+ List.iter (fun (dest, _) ->
+ ids := Stateid.Set.add dest !ids;
+ List.iter (fun box -> boxes := box :: !boxes)
+ (Dag.property_of graph dest))
+ l);
+ boxes := CList.sort_uniquize Dag.Property.compare !boxes;
+
let oc = open_out fname_dot in
output_string oc "digraph states {\n";
Dag.iter graph (fun from cf _ l ->
- let c1 = add_to_clus_or_ids from cf in
List.iter (fun (dest, trans) ->
- let c2 = add_to_clus_or_ids dest (Dag.cluster_of graph dest) in
- fprintf oc "%s -> %s [xlabel=%s,labelfloat=%b];\n"
- (node from) (node dest) (edge trans) (c1 && c2)) l
+ fprintf oc "%s -> %s [xlabel=%s,labelfloat=true];\n"
+ (node from) (node dest) (edge trans)) l
);
- StateidSet.iter (nodefmt oc) !ids;
- Hashtbl.iter (fun c nodes ->
- fprintf oc "subgraph cluster_%s {\n" (Dag.Cluster.to_string c);
- List.iter (nodefmt oc) nodes;
- fprintf oc "color=blue; }\n"
- ) clus;
+
+ let contains b1 b2 =
+ Stateid.Set.subset
+ (Dag.Property.having_it b2) (Dag.Property.having_it b1) in
+ let same_box = Dag.Property.equal in
+ let outerboxes boxes =
+ List.filter (fun b ->
+ not (List.exists (fun b1 ->
+ not (same_box b1 b) && contains b1 b) boxes)
+ ) boxes in
+ let rec rec_print b =
+ boxes := CList.remove same_box b !boxes;
+ let sub_boxes = List.filter (contains b) (outerboxes !boxes) in
+ fprintf oc "subgraph cluster_%s {\n" (Dag.Property.to_string b);
+ List.iter rec_print sub_boxes;
+ Stateid.Set.iter (fun id ->
+ if Stateid.Set.mem id !ids then begin
+ ids := Stateid.Set.remove id !ids;
+ nodefmt oc id
+ end)
+ (Dag.Property.having_it b);
+ fprintf oc "color=blue; }\n" in
+ List.iter rec_print (outerboxes !boxes);
+ Stateid.Set.iter (nodefmt oc) !ids;
+
List.iteri (fun i (b,id) ->
let shape = if Branch.equal head b then "box3d" else "box" in
fprintf oc "b%d -> %s;\n" i (node id);
fprintf oc "b%d [shape=%s,label=\"%s\"];\n" i shape
(Branch.to_string b);
) heads;
+
output_string oc "}\n";
close_out oc;
ignore(Sys.command
("dot -Tpdf -Gcharset=latin1 " ^ fname_dot ^ " -o" ^ fname_ps))
- type vcs = (branch_type, transaction, vcs state_info) t
+ type vcs = (branch_type, transaction, vcs state_info, box) t
let vcs : vcs ref = ref (empty Stateid.dummy)
let init id =
@@ -535,15 +574,39 @@ end = struct (* {{{ *)
let nodes_in_slice ~start ~stop =
List.rev (List.map fst (nodes_in_slice ~start ~stop))
- let create_cluster l ~qed ~start = vcs := create_cluster !vcs l (qed,start)
- let cluster_of id = Option.map Dag.Cluster.data (cluster_of !vcs id)
- let delete_cluster_of id =
- Option.iter (fun x -> vcs := delete_cluster !vcs x) (Vcs_.cluster_of !vcs id)
+ let topo_invariant l =
+ let all = List.fold_right Stateid.Set.add l Stateid.Set.empty in
+ List.for_all
+ (fun x ->
+ let props = property_of !vcs x in
+ let sets = List.map Dag.Property.having_it props in
+ List.for_all (fun s -> Stateid.Set.(subset s all || subset all s)) sets)
+ l
+
+ let create_proof_task_box l ~qed ~start =
+ if not (topo_invariant l) then anomaly (str "overlapping boxes");
+ vcs := create_property !vcs l (ProofTask { qed; start })
+ let create_error_bound_box l ~switch =
+ vcs := create_property !vcs l
+ (ErrorBound { stuff = () })
+ let box_of id = List.map Dag.Property.data (property_of !vcs id)
+ let delete_proof_task_box_of id =
+ List.iter (fun x -> vcs := delete_property !vcs x)
+ (List.filter (fun x ->
+ match Dag.Property.data x with ProofTask _ -> true | _ -> false)
+ (Vcs_.property_of !vcs id))
+ let proof_task_box_of id =
+ match
+ CList.map_filter (function ProofTask x -> Some x | _ -> None) (box_of id)
+ with
+ | [] -> None
+ | [x] -> Some x
+ | _ -> anomaly (str "node with more than 1 proof task box")
let gc () =
let old_vcs = !vcs in
let new_vcs, erased_nodes = gc old_vcs in
- Vcs_.NodeSet.iter (fun id ->
+ Stateid.Set.iter (fun id ->
match (Vcs_aux.visit old_vcs id).step with
| `Qed ({ fproof = Some (_, cancel_switch) }, _)
| `Cmd { cqueue = `TacQueue cancel_switch }
@@ -1878,7 +1941,7 @@ let known_state ?(redefine_qed=false) ~cache id =
let drop_pt = keep == VtKeepAsAxiom in
let stop, exn_info, loc = eop, (id, eop), x.loc in
log_processing_async id name;
- VCS.create_cluster nodes ~qed:id ~start;
+ VCS.create_proof_task_box nodes ~qed:id ~start;
begin match brinfo, qed.fproof with
| { VCS.kind = `Edit _ }, None -> assert false
| { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) ->
@@ -2403,7 +2466,7 @@ let edit_at id =
| _ -> assert false
in
let is_ancestor_of_cur_branch id =
- Vcs_.NodeSet.mem id
+ Stateid.Set.mem id
(VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in
let has_failed qed_id =
match VCS.visit qed_id with
@@ -2418,13 +2481,13 @@ let edit_at id =
| { next } -> master_for_br root next in
let reopen_branch start at_id mode qed_id tip old_branch =
let master_id, cancel_switch, keep =
- (* Hum, this should be the real start_id in the clusted and not next *)
+ (* Hum, this should be the real start_id in the cluster and not next *)
match VCS.visit qed_id with
| { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep
- | _ -> anomaly (str "Cluster not ending with Qed") in
+ | _ -> anomaly (str "ProofTask not ending with Qed") in
VCS.branch ~root:master_id ~pos:id
VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch));
- VCS.delete_cluster_of id;
+ VCS.delete_proof_task_box_of id;
cancel_switch := true;
Reach.known_state ~cache:(interactive ()) id;
VCS.checkout_shallowest_proof_branch ();
@@ -2438,14 +2501,14 @@ let edit_at id =
let { mine = brname, brinfo; others } = Backtrack.branches_of id in
List.iter (fun (name,{ VCS.kind = k; root; pos }) ->
if not(VCS.Branch.equal name VCS.Branch.master) &&
- Vcs_.NodeSet.mem root ancestors then
+ Stateid.Set.mem root ancestors then
VCS.branch ~root ~pos name k)
others;
VCS.reset_branch VCS.Branch.master (master_for_br brinfo.VCS.root id);
VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos
(Option.default brname bn)
(no_edit brinfo.VCS.kind);
- VCS.delete_cluster_of id;
+ VCS.delete_proof_task_box_of id;
VCS.gc ();
VCS.print ();
if not !Flags.async_proofs_full then
@@ -2460,14 +2523,14 @@ let edit_at id =
| Some{ mine = bn, { VCS.kind = `Proof(m,_) }} -> Some(m,bn)
| Some{ mine = _, { VCS.kind = `Edit(m,_,_,_,bn) }} -> Some (m,bn)
| _ -> None in
- match focused, VCS.cluster_of id, branch_info with
+ match focused, VCS.proof_task_box_of id, branch_info with
| _, Some _, None -> assert false
- | false, Some (qed_id,start), Some(mode,bn) ->
+ | false, Some { qed = qed_id ; start }, Some(mode,bn) ->
let tip = VCS.cur_tip () in
if has_failed qed_id && is_pure qed_id && not !Flags.async_proofs_never_reopen_branch
then reopen_branch start id mode qed_id tip bn
else backto id (Some bn)
- | true, Some (qed_id,_), Some(mode,bn) ->
+ | true, Some { qed = qed_id }, Some(mode,bn) ->
if on_cur_branch id then begin
assert false
end else if is_ancestor_of_cur_branch id then begin
diff --git a/stm/vcs.ml b/stm/vcs.ml
index 38c029901d..c483ea4a9d 100644
--- a/stm/vcs.ml
+++ b/stm/vcs.ml
@@ -22,51 +22,49 @@ module type S = sig
end
type id
-
- (* Branches have [branch_info] attached to them. *)
+
type ('kind) branch_info = {
kind : [> `Master] as 'kind;
root : id;
pos : id;
}
-
- type ('kind,'diff,'info) t constraint 'kind = [> `Master ]
-
- val empty : id -> ('kind,'diff,'info) t
-
- val current_branch : ('k,'e,'i) t -> Branch.t
- val branches : ('k,'e,'i) t -> Branch.t list
-
- val get_branch : ('k,'e,'i) t -> Branch.t -> 'k branch_info
- val reset_branch : ('k,'e,'i) t -> Branch.t -> id -> ('k,'e,'i) t
+
+ type ('kind,'diff,'info,'property_data) t constraint 'kind = [> `Master ]
+
+ val empty : id -> ('kind,'diff,'info,'property_data) t
+
+ val current_branch : ('k,'e,'i,'c) t -> Branch.t
+ val branches : ('k,'e,'i,'c) t -> Branch.t list
+
+ val get_branch : ('k,'e,'i,'c) t -> Branch.t -> 'k branch_info
+ val reset_branch : ('k,'e,'i,'c) t -> Branch.t -> id -> ('k,'e,'i,'c) t
val branch :
- ('kind,'e,'i) t -> ?root:id -> ?pos:id ->
- Branch.t -> 'kind -> ('kind,'e,'i) t
- val delete_branch : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t
+ ('kind,'e,'i,'c) t -> ?root:id -> ?pos:id ->
+ Branch.t -> 'kind -> ('kind,'e,'i,'c) t
+ val delete_branch : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t
val merge :
- ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t ->
- Branch.t -> ('k,'diff,'i) t
- val commit : ('k,'diff,'i) t -> id -> 'diff -> ('k,'diff,'i) t
+ ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t ->
+ Branch.t -> ('k,'diff,'i,'c) t
+ val commit : ('k,'diff,'i,'c) t -> id -> 'diff -> ('k,'diff,'i,'c) t
val rewrite_merge :
- ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> at:id ->
- Branch.t -> ('k,'diff,'i) t
- val checkout : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t
-
- val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t
- val get_info : ('k,'e,'info) t -> id -> 'info option
+ ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> at:id ->
+ Branch.t -> ('k,'diff,'i,'c) t
+ val checkout : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t
- module NodeSet : Set.S with type elt = id
-
- val gc : ('k,'e,'info) t -> ('k,'e,'info) t * NodeSet.t
-
- val reachable : ('k,'e,'info) t -> id -> NodeSet.t
+ val set_info : ('k,'e,'info,'c) t -> id -> 'info -> ('k,'e,'info,'c) t
+ val get_info : ('k,'e,'info,'c) t -> id -> 'info option
+ (* Read only dag *)
module Dag : Dag.S with type node = id
- val dag : ('kind,'diff,'info) t -> ('diff,'info,id*id) Dag.t
+ val dag : ('kind,'diff,'info,'cdata) t -> ('diff,'info,'cdata) Dag.t
+
+ val create_property : ('k,'e,'i,'c) t -> id list -> 'c -> ('k,'e,'i,'c) t
+ val property_of : ('k,'e,'i,'c) t -> id -> 'c Dag.Property.t list
+ val delete_property : ('k,'e,'i,'c) t -> 'c Dag.Property.t -> ('k,'e,'i,'c) t
- val create_cluster : ('k,'e,'i) t -> id list -> (id * id) -> ('k,'e,'i) t
- val cluster_of : ('k,'e,'i) t -> id -> (id * id) Dag.Cluster.t option
- val delete_cluster : ('k,'e,'i) t -> (id * id) Dag.Cluster.t -> ('k,'e,'i) t
+ (* Removes all unreachable nodes and returns them *)
+ val gc : ('k,'e,'info,'c) t -> ('k,'e,'info,'c) t * Dag.NodeSet.t
+ val reachable : ('k,'e,'info,'c) t -> id -> Dag.NodeSet.t
end
@@ -78,7 +76,6 @@ type id = OT.t
module NodeSet = Dag.NodeSet
-
module Branch =
struct
type t = string
@@ -99,10 +96,10 @@ type 'kind branch_info = {
pos : id;
}
-type ('kind,'edge,'info) t = {
+type ('kind,'edge,'info,'property_data) t = {
cur_branch : Branch.t;
heads : 'kind branch_info BranchMap.t;
- dag : ('edge,'info,id*id) Dag.t;
+ dag : ('edge,'info,'property_data) Dag.t;
}
let empty root = {
@@ -167,9 +164,9 @@ let checkout vcs name = { vcs with cur_branch = name }
let set_info vcs id info = { vcs with dag = Dag.set_info vcs.dag id info }
let get_info vcs id = Dag.get_info vcs.dag id
-let create_cluster vcs l i = { vcs with dag = Dag.create_cluster vcs.dag l i }
-let cluster_of vcs i = Dag.cluster_of vcs.dag i
-let delete_cluster vcs c = { vcs with dag = Dag.del_cluster vcs.dag c }
+let create_property vcs l i = { vcs with dag = Dag.create_property vcs.dag l i }
+let property_of vcs i = Dag.property_of vcs.dag i
+let delete_property vcs c = { vcs with dag = Dag.del_property vcs.dag c }
let branches vcs = BranchMap.fold (fun x _ accu -> x :: accu) vcs.heads []
let dag vcs = vcs.dag
diff --git a/stm/vcs.mli b/stm/vcs.mli
index 8f22fee843..46b40f8a4c 100644
--- a/stm/vcs.mli
+++ b/stm/vcs.mli
@@ -19,10 +19,11 @@
As a consequence, "checkout" just updates the current branch.
The type [id] is the type of commits (a node in the dag)
- The type [Vcs.t] has 3 parameters:
+ The type [Vcs.t] has 4 parameters:
['info] data attached to a node (like a system state)
['diff] data attached to an edge (the commit content, a "patch")
['kind] extra data attached to a branch (like being the master branch)
+ ['cdata] extra data hold by dag properties
*)
module type S = sig
@@ -45,46 +46,51 @@ module type S = sig
pos : id;
}
- type ('kind,'diff,'info) t constraint 'kind = [> `Master ]
+ type ('kind,'diff,'info,'property_data) t constraint 'kind = [> `Master ]
- val empty : id -> ('kind,'diff,'info) t
+ val empty : id -> ('kind,'diff,'info,'property_data) t
- val current_branch : ('k,'e,'i) t -> Branch.t
- val branches : ('k,'e,'i) t -> Branch.t list
+ val current_branch : ('k,'e,'i,'c) t -> Branch.t
+ val branches : ('k,'e,'i,'c) t -> Branch.t list
- val get_branch : ('k,'e,'i) t -> Branch.t -> 'k branch_info
- val reset_branch : ('k,'e,'i) t -> Branch.t -> id -> ('k,'e,'i) t
+ val get_branch : ('k,'e,'i,'c) t -> Branch.t -> 'k branch_info
+ val reset_branch : ('k,'e,'i,'c) t -> Branch.t -> id -> ('k,'e,'i,'c) t
val branch :
- ('kind,'e,'i) t -> ?root:id -> ?pos:id ->
- Branch.t -> 'kind -> ('kind,'e,'i) t
- val delete_branch : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t
+ ('kind,'e,'i,'c) t -> ?root:id -> ?pos:id ->
+ Branch.t -> 'kind -> ('kind,'e,'i,'c) t
+ val delete_branch : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t
val merge :
- ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t ->
- Branch.t -> ('k,'diff,'i) t
- val commit : ('k,'diff,'i) t -> id -> 'diff -> ('k,'diff,'i) t
+ ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t ->
+ Branch.t -> ('k,'diff,'i,'c) t
+ val commit : ('k,'diff,'i,'c) t -> id -> 'diff -> ('k,'diff,'i,'c) t
val rewrite_merge :
- ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> at:id ->
- Branch.t -> ('k,'diff,'i) t
- val checkout : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t
+ ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> at:id ->
+ Branch.t -> ('k,'diff,'i,'c) t
+ val checkout : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t
- val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t
- val get_info : ('k,'e,'info) t -> id -> 'info option
+ val set_info : ('k,'e,'info,'c) t -> id -> 'info -> ('k,'e,'info,'c) t
+ val get_info : ('k,'e,'info,'c) t -> id -> 'info option
- module NodeSet : Set.S with type elt = id
+ (* Read only dag *)
+ module Dag : Dag.S with type node = id
+ val dag : ('kind,'diff,'info,'cdata) t -> ('diff,'info,'cdata) Dag.t
- (* Removes all unreachable nodes and returns them *)
- val gc : ('k,'e,'info) t -> ('k,'e,'info) t * NodeSet.t
+ (* Properties are not a concept typical of a VCS, but a useful metadata
+ * of a DAG (or graph). *)
+ val create_property : ('k,'e,'i,'c) t -> id list -> 'c -> ('k,'e,'i,'c) t
+ val property_of : ('k,'e,'i,'c) t -> id -> 'c Dag.Property.t list
+ val delete_property : ('k,'e,'i,'c) t -> 'c Dag.Property.t -> ('k,'e,'i,'c) t
- val reachable : ('k,'e,'info) t -> id -> NodeSet.t
+ (* Removes all unreachable nodes and returns them *)
+ val gc : ('k,'e,'info,'c) t -> ('k,'e,'info,'c) t * Dag.NodeSet.t
+ val reachable : ('k,'e,'info,'c) t -> id -> Dag.NodeSet.t
- (* read only dag *)
- module Dag : Dag.S with type node = id
- val dag : ('kind,'diff,'info) t -> ('diff,'info,id * id) Dag.t
- val create_cluster : ('k,'e,'i) t -> id list -> (id * id) -> ('k,'e,'i) t
- val cluster_of : ('k,'e,'i) t -> id -> (id * id) Dag.Cluster.t option
- val delete_cluster : ('k,'e,'i) t -> (id * id) Dag.Cluster.t -> ('k,'e,'i) t
-
end
-module Make(OT : Map.OrderedType) : S with type id = OT.t
+module Make(OT : Map.OrderedType) : S
+with type id = OT.t
+and type Dag.node = OT.t
+and type Dag.NodeSet.t = Set.Make(OT).t
+and type Dag.NodeSet.elt = OT.t
+
--
cgit v1.2.3
From 07115d044cb97bc6c0a7323783d4d53e083d3e89 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 13 May 2016 11:39:34 +0200
Subject: STM: carry AST and indentation of document commands
This paves the way to detecting error boundaries via indentation
---
stm/stm.ml | 140 +++++++++++++++++++++++++++++++++++++++----------------------
1 file changed, 89 insertions(+), 51 deletions(-)
diff --git a/stm/stm.ml b/stm/stm.ml
index 1c8603f0f5..492ac99fe1 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -76,8 +76,14 @@ let interactive () =
let async_proofs_workers_extra_env = ref [||]
-type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr }
-let pr_ast { expr } = pr_vernac expr
+type aast = {
+ verbose : bool;
+ loc : Loc.t;
+ indentation : int;
+ strlen : int;
+ mutable expr : vernac_expr; (* mutable: Proof using hinted by aux file *)
+}
+let pr_ast { expr; indentation } = int indentation ++ str " " ++ pr_vernac expr
let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
@@ -114,17 +120,31 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
end
(* Wrapper for Vernac.parse_sentence to set the feedback id *)
-let vernac_parse ?newtip ?route eid s =
+let indentation_of_string s =
+ let len = String.length s in
+ let rec aux n i precise =
+ if i >= len then 0, precise, len
+ else
+ match s.[i] with
+ | ' ' | '\t' -> aux (succ n) (succ i) precise
+ | '\n' | '\r' -> aux 0 (succ i) true
+ | _ -> n, precise, len in
+ aux 0 0 false
+
+let vernac_parse ?(indlen_prev=fun() -> 0) ?newtip ?route eid s =
let feedback_id =
if Option.is_empty newtip then Edit eid
else State (Option.get newtip) in
+ let indentation, precise, strlen = indentation_of_string s in
+ let indentation =
+ if precise then indentation else indlen_prev () + indentation in
set_id_for_feedback ?route feedback_id;
let pa = Pcoq.Gram.parsable (Stream.of_string s) in
Flags.with_option Flags.we_are_parsing (fun () ->
try
match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
| None -> raise (Invalid_argument "vernac_parse")
- | Some ast -> ast
+ | Some (loc, ast) -> indentation, strlen, loc, ast
with e when Errors.noncritical e ->
let (e, info) = Errors.push e in
let loc = Option.default Loc.ghost (Loc.get_loc info) in
@@ -153,19 +173,22 @@ type branch_type =
type cmd_t = {
ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *)
ceff : bool; (* is a side-effecting command in the middle of a proof *)
- cast : ast;
+ cast : aast;
cids : Id.t list;
- cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch | `SkipQueue ] }
-type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list
+ cqueue : [ `MainQueue
+ | `TacQueue of cancel_switch
+ | `QueryQueue of cancel_switch
+ | `SkipQueue ] }
+type fork_t = aast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list
type qed_t = {
- qast : ast;
+ qast : aast;
keep : vernac_qed_type;
mutable fproof : (future_proof * cancel_switch) option;
brname : Vcs_.Branch.t;
brinfo : branch_type Vcs_.branch_info
}
-type seff_t = ast option
-type alias_t = Stateid.t * ast
+type seff_t = aast option
+type alias_t = Stateid.t * aast
type transaction =
| Cmd of cmd_t
| Fork of fork_t
@@ -177,7 +200,7 @@ type step =
[ `Cmd of cmd_t
| `Fork of fork_t * Stateid.t option
| `Qed of qed_t * Stateid.t
- | `Sideff of [ `Ast of ast * Stateid.t | `Id of Stateid.t ]
+ | `Sideff of [ `Ast of aast * Stateid.t | `Id of Stateid.t ]
| `Alias of alias_t ]
type visit = { step : step; next : Stateid.t }
@@ -186,15 +209,15 @@ type visit = { step : step; next : Stateid.t }
let summary_pstate = [ Evarutil.meta_counter_summary_name;
Evd.evar_counter_summary_name;
"program-tcc-table" ]
-type state = {
- system : States.state; (* summary + libstack *)
- proof : Proof_global.state; (* proof state *)
- shallow : bool (* is the state trimmed down (libstack) *)
-}
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) *)
+}
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 *)
@@ -305,7 +328,7 @@ module VCS : sig
val rewrite_merge : id -> ours:transaction -> at:id -> Branch.t -> unit
val delete_branch : Branch.t -> unit
val commit : id -> transaction -> unit
- val mk_branch_name : ast -> Branch.t
+ val mk_branch_name : aast -> Branch.t
val edit_branch : Branch.t
val branch : ?root:id -> ?pos:id -> Branch.t -> branch_type -> unit
val reset_branch : Branch.t -> id -> unit
@@ -330,7 +353,7 @@ module VCS : sig
val proof_nesting : unit -> int
val checkout_shallowest_proof_branch : unit -> unit
- val propagate_sideff : replay:ast option -> unit
+ val propagate_sideff : replay:aast option -> unit
val gc : unit -> unit
@@ -1199,7 +1222,7 @@ end = struct (* {{{ *)
Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in
vernac_interp stop
~proof:(pobject, terminator)
- { verbose = false; loc;
+ { verbose = false; loc; indentation = 0; strlen = 0;
expr = (VernacEndProof (Proved (Opaque None,None))) }) in
ignore(Future.join checked_proof);
end;
@@ -1340,7 +1363,7 @@ end = struct (* {{{ *)
* looking at the ones that happen to be present in the current env *)
Reach.known_state ~cache:`No start;
vernac_interp stop ~proof
- { verbose = false; loc;
+ { verbose = false; loc; indentation = 0; strlen = 0;
expr = (VernacEndProof (Proved (Opaque None,None))) };
`OK proof
end
@@ -1493,7 +1516,7 @@ and TacTask : sig
t_state : Stateid.t;
t_state_fb : Stateid.t;
t_assign : output Future.assignement -> unit;
- t_ast : int * ast;
+ t_ast : int * aast;
t_goal : Goal.goal;
t_kill : unit -> unit;
t_name : string }
@@ -1510,7 +1533,7 @@ end = struct (* {{{ *)
t_state : Stateid.t;
t_state_fb : Stateid.t;
t_assign : output Future.assignement -> unit;
- t_ast : int * ast;
+ t_ast : int * aast;
t_goal : Goal.goal;
t_kill : unit -> unit;
t_name : string }
@@ -1519,7 +1542,7 @@ end = struct (* {{{ *)
r_state : Stateid.t;
r_state_fb : Stateid.t;
r_document : VCS.vcs option;
- r_ast : int * ast;
+ r_ast : int * aast;
r_goal : Goal.goal;
r_name : string }
@@ -1605,13 +1628,15 @@ end (* }}} *)
and Partac : sig
val vernac_interp :
- cancel_switch -> int -> Stateid.t -> Stateid.t -> ast -> unit
+ cancel_switch -> int -> Stateid.t -> Stateid.t -> aast -> unit
end = struct (* {{{ *)
module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask)
- let vernac_interp cancel nworkers safe_id id { verbose; loc; expr = e } =
+ let vernac_interp cancel nworkers safe_id id
+ { indentation; verbose; loc; expr = e; strlen }
+ =
let e, time, fail =
let rec find time fail = function
| VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e
@@ -1628,7 +1653,7 @@ end = struct (* {{{ *)
Future.create_delegate
~name:(Printf.sprintf "subgoal %d" i)
(State.exn_on id ~valid:safe_id) in
- let t_ast = (i, { verbose; loc; expr = e }) in
+ let t_ast = (i, { indentation; verbose; loc; expr = e; strlen }) in
let t_name = Goal.uid g in
TaskQueue.enqueue_task queue
({ t_state = safe_id; t_state_fb = id;
@@ -1662,16 +1687,16 @@ end (* }}} *)
and QueryTask : sig
- type task = { t_where : Stateid.t; t_for : Stateid.t ; t_what : ast }
+ type task = { t_where : Stateid.t; t_for : Stateid.t ; t_what : aast }
include AsyncTaskQueue.Task with type task := task
end = struct (* {{{ *)
type task =
- { t_where : Stateid.t; t_for : Stateid.t ; t_what : ast }
+ { t_where : Stateid.t; t_for : Stateid.t ; t_what : aast }
type request =
- { r_where : Stateid.t ; r_for : Stateid.t ; r_what : ast; r_doc : VCS.vcs }
+ { r_where : Stateid.t ; r_for : Stateid.t ; r_what : aast; r_doc : VCS.vcs }
type response = unit
let name = ref "queryworker"
@@ -1717,7 +1742,7 @@ end (* }}} *)
and Query : sig
val init : unit -> unit
- val vernac_interp : cancel_switch -> Stateid.t -> Stateid.t -> ast -> unit
+ val vernac_interp : cancel_switch -> Stateid.t -> Stateid.t -> aast -> unit
end = struct (* {{{ *)
@@ -2194,10 +2219,11 @@ let snapshot_vio ldir long_f_dot_v =
let reset_task_queue = Slaves.reset_task_queue
(* Document building *)
-let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
+let process_transaction ?(newtip=Stateid.fresh ()) ~tty
+ ({ verbose; loc; expr } as x) c
+ =
let warn_if_pos a b =
if b then msg_warning(pr_ast a ++ str" should not be part of a script") in
- let v, x = expr, { verbose = verbose; loc; expr } in
prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x));
let vcs = VCS.backup () in
try
@@ -2252,7 +2278,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
| VtQuery (false,(report_id,route)), VtNow when tty = true ->
finish ();
(try Future.purify (vernac_interp report_id ~route)
- { verbose = true; loc; expr }
+ {x with verbose = true }
with e when Errors.noncritical e ->
let e = Errors.push e in
iraise (State.exn_on report_id e)); `Ok
@@ -2381,11 +2407,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
anomaly(str"classifier: VtUnknown must imply VtNow")
end in
(* Proof General *)
- begin match v with
+ begin match expr with
| VernacStm (PGLast _) ->
if not (VCS.Branch.equal head VCS.Branch.master) then
vernac_interp Stateid.dummy
- { verbose = true; loc = Loc.ghost;
+ { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0;
expr = VernacShow (ShowGoal OpenSubgoals) }
| _ -> ()
end;
@@ -2406,19 +2432,30 @@ let get_ast id =
let stop_worker n = Slaves.cancel_worker n
+(* You may need to know the len + indentation of previous command to compute
+ * the indentation of the current one.
+ * Eg. foo. bar.
+ * Here bar is indented of the indentation of foo + its strlen (4) *)
+let ind_len_of id =
+ if Stateid.equal id Stateid.initial then 0
+ else match (VCS.visit id).step with
+ | `Cmd { ctac = true; cast = { indentation; strlen } } ->
+ indentation + strlen
+ | _ -> 0
+
let add ~ontop ?newtip ?(check=ignore) verb eid s =
let cur_tip = VCS.cur_tip () in
- if Stateid.equal ontop cur_tip then begin
- let _, ast as loc_ast = vernac_parse ?newtip eid s in
- check(loc_ast);
- let clas = classify_vernac ast in
- match process_transaction ?newtip ~tty:false verb clas loc_ast with
- | `Ok -> VCS.cur_tip (), `NewTip
- | `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ())
- end else begin
+ if not (Stateid.equal ontop cur_tip) then
(* For now, arbitrary edits should be announced with edit_at *)
- anomaly(str"Not yet implemented, the GUI should not try this")
- end
+ anomaly(str"Not yet implemented, the GUI should not try this");
+ let indentation, strlen, loc, ast =
+ vernac_parse ~indlen_prev:(fun () -> ind_len_of ontop) ?newtip eid s in
+ check(loc,ast);
+ let clas = classify_vernac ast in
+ let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in
+ match process_transaction ?newtip ~tty:false aast clas with
+ | `Ok -> VCS.cur_tip (), `NewTip
+ | `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ())
let set_perspective id_list = Slaves.set_perspective id_list
@@ -2433,15 +2470,15 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
if Stateid.equal at Stateid.dummy then finish ()
else Reach.known_state ~cache:`Yes at;
let newtip, route = report_with in
- let _, ast as loc_ast = vernac_parse ~newtip ~route 0 s in
+ let indentation, strlen, loc, ast = vernac_parse ~newtip ~route 0 s in
let clas = classify_vernac ast in
+ let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
match clas with
| VtStm (w,_), _ ->
- ignore(process_transaction
- ~tty:false true (VtStm (w,false), VtNow) loc_ast)
+ ignore(process_transaction ~tty:false aast (VtStm (w,false), VtNow))
| _ ->
ignore(process_transaction
- ~tty:false true (VtQuery (false,report_with), VtNow) loc_ast))
+ ~tty:false aast (VtQuery (false,report_with), VtNow)))
s
let edit_at id =
@@ -2573,9 +2610,10 @@ let restore d = VCS.restore d
(*********************** TTY API (PG, coqtop, coqc) ***************************)
(******************************************************************************)
-let interp verb (_,e as lexpr) =
+let interp verb (loc,e) =
let clas = classify_vernac e in
- let rc = process_transaction ~tty:true verb clas lexpr in
+ let aast = { verbose = verb; indentation = 0; strlen = 0; loc; expr = e } in
+ let rc = process_transaction ~tty:true aast clas in
if rc <> `Ok then anomaly(str"tty loop can't be mixed with the STM protocol");
if interactive () = `Yes ||
(!Flags.async_proofs_mode = Flags.APoff &&
--
cgit v1.2.3
From 5e86a655278f8f8be38363cc3bfc2f88ec2c3e40 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 May 2016 11:11:30 +0200
Subject: STM: proof block detection/error resilience API
This commit introduces the concept of proof blocks that are
resilient to errors. They are represented as ErrorBound boxes
in the STM document with the topological invariant that they never
overlap.
The detection and error recovery of ErrorBound boxes is defined outside
the STM. One can define a box by providing a function to detect it
statically by crawling the parsed document and a function to recover
from an error at run time.
---
intf/vernacexpr.mli | 7 +-
ltac/extratactics.ml4 | 4 +-
ltac/g_ltac.ml4 | 3 +-
plugins/decl_mode/g_decl_mode.ml4 | 2 +-
stm/stm.ml | 213 +++++++++++++++++++++++++++++++-------
stm/stm.mli | 83 ++++++++++++++-
stm/vernac_classifier.ml | 13 ++-
7 files changed, 275 insertions(+), 50 deletions(-)
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index ae9328fcc0..6ce15a7c5a 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -454,7 +454,7 @@ type vernac_type =
| VtStartProof of vernac_start
| VtSideff of vernac_sideff_type
| VtQed of vernac_qed_type
- | VtProofStep of bool (* parallelize *)
+ | VtProofStep of proof_step
| VtProofMode of string
| VtQuery of vernac_part_of_script * report_with
| VtStm of vernac_control * vernac_part_of_script
@@ -476,6 +476,11 @@ and vernac_control =
and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
| Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
+and proof_step = { (* TODO: inline with OCaml 4.03 *)
+ parallel : bool;
+ proof_block_detection : proof_block_name option
+}
+and proof_block_name = string (* open type of delimiters *)
type vernac_when =
| VtNow
| VtLater
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 5d3c149ab9..57fad85113 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -872,7 +872,7 @@ END;;
mode. *)
VERNAC COMMAND EXTEND GrabEvars
[ "Grab" "Existential" "Variables" ]
- => [ Vernacexpr.VtProofStep false, Vernacexpr.VtLater ]
+ => [ Vernac_classifier.classify_as_proofstep ]
-> [ Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) ]
END
@@ -903,7 +903,7 @@ END
(* Command to add every unshelved variables to the focus *)
VERNAC COMMAND EXTEND Unshelve
[ "Unshelve" ]
- => [ Vernacexpr.VtProofStep false, Vernacexpr.VtLater ]
+ => [ Vernac_classifier.classify_as_proofstep ]
-> [ Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p) ]
END
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 3579fc10f6..c8287a2c8d 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -366,7 +366,8 @@ VERNAC tactic_mode EXTEND VernacSolve
vernac_solve g n t def
]
| [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
- [ VtProofStep true, VtLater ] -> [
+ [ VtProofStep{ parallel = true; proof_block_detection = None },
+ VtLater ] -> [
vernac_solve SelectAll n t def
]
END
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 78a95143df..4c3bebd65f 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -98,7 +98,7 @@ let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
let classify_proof_instr = function
| { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow
- | _ -> VtProofStep false, VtLater
+ | _ -> Vernac_classifier.classify_as_proofstep
(* We use the VERNAC EXTEND facility with a custom non-terminal
to populate [proof_mode] with a new toplevel interpreter.
diff --git a/stm/stm.ml b/stm/stm.ml
index 492ac99fe1..35f7295dd6 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -171,7 +171,7 @@ type branch_type =
| `Edit of
proof_mode * Stateid.t * Stateid.t * vernac_qed_type * Vcs_.Branch.t ]
type cmd_t = {
- ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *)
+ ctac : bool; (* is a tactic *)
ceff : bool; (* is a side-effecting command in the middle of a proof *)
cast : aast;
cids : Id.t list;
@@ -229,17 +229,22 @@ type 'vcs state_info = { (* TODO: Make this record private to VCS *)
let default_info () =
{ n_reached = 0; n_goals = 0; state = Empty; vcs_backup = None,None }
+module DynBlockData : Dyn.S = Dyn.Make(struct end)
+
(* Clusters of nodes implemented as Dag properties. While Dag and Vcs impose
* no constraint on properties, here we impose boxes to be non overlapping. *)
type box =
| ProofTask of pt
- | ErrorBound of eb
+ | ErrorBound of static_block_declaration * proof_block_name
and pt = { (* TODO: inline records in OCaml 4.03 *)
- start : Stateid.t;
+ lemma : Stateid.t;
qed : Stateid.t;
}
-and eb = {
- stuff : unit;
+and static_block_declaration = {
+ start : Stateid.t;
+ stop : Stateid.t;
+ dynamic_switch : Stateid.t;
+ carry_on_data : DynBlockData.t;
}
(* Functions that work on a Vcs with a specific branch type *)
@@ -346,9 +351,9 @@ module VCS : sig
val nodes_in_slice : start:id -> stop:id -> Stateid.t list
val create_proof_task_box : id list -> qed:id -> start:id -> unit
- val create_error_bound_box : id list -> switch:id -> unit
+ val create_error_bound_box : static_block_declaration -> string -> unit
val box_of : id -> box list
- val delete_proof_task_box_of : id -> unit
+ val delete_boxes_of : id -> unit
val proof_task_box_of : id -> pt option
val proof_nesting : unit -> int
@@ -465,7 +470,12 @@ end = struct (* {{{ *)
nodefmt oc id
end)
(Dag.Property.having_it b);
- fprintf oc "color=blue; }\n" in
+ match Dag.Property.data b with
+ | ErrorBound ({ dynamic_switch = id }, lbl) ->
+ fprintf oc "label=\"%s (test:%s)\";\n" lbl (Stateid.to_string id);
+ fprintf oc "color=red; }\n"
+ | ProofTask _ -> fprintf oc "color=blue; }\n"
+ in
List.iter rec_print (outerboxes !boxes);
Stateid.Set.iter (nodefmt oc) !ids;
@@ -576,6 +586,17 @@ end = struct (* {{{ *)
{ (get_info id) with state = Empty; vcs_backup = None,None } in
let copy_info_w_state v id =
Vcs_.set_info v id { (get_info id) with vcs_backup = None,None } in
+ let copy_error_bound_boxes v =
+ let nodes = Vcs_.Dag.all_nodes (Vcs_.dag v) in
+ let props =
+ Stateid.Set.fold (fun n pl -> Vcs_.property_of !vcs n @ pl) nodes [] in
+ let props = CList.sort_uniquize Vcs_.Dag.Property.compare props in
+ (* XXX check if par: works here, since we copy a single node *)
+ List.fold_left (fun v p ->
+ Vcs_.create_property v
+ (Stateid.Set.elements (Vcs_.Dag.Property.having_it p))
+ (Vcs_.Dag.Property.data p)) v props
+ in
let v = Vcs_.empty start in
let v = copy_info v start in
let v = List.fold_right (fun (id,tr) v ->
@@ -592,7 +613,8 @@ end = struct (* {{{ *)
let v = fill stop in
(* We put in the new dag the first state (since Qed shall run on it,
* see check_task_aux) *)
- copy_info_w_state v start
+ let v = copy_info_w_state v start in
+ copy_error_bound_boxes v
let nodes_in_slice ~start ~stop =
List.rev (List.map fst (nodes_in_slice ~start ~stop))
@@ -606,18 +628,16 @@ end = struct (* {{{ *)
List.for_all (fun s -> Stateid.Set.(subset s all || subset all s)) sets)
l
- let create_proof_task_box l ~qed ~start =
+ let create_proof_task_box l ~qed ~start:lemma =
+ if not (topo_invariant l) then anomaly (str "overlapping boxes");
+ vcs := create_property !vcs l (ProofTask { qed; lemma })
+ let create_error_bound_box ({ start; stop} as decl) name =
+ let l = nodes_in_slice ~start ~stop in
if not (topo_invariant l) then anomaly (str "overlapping boxes");
- vcs := create_property !vcs l (ProofTask { qed; start })
- let create_error_bound_box l ~switch =
- vcs := create_property !vcs l
- (ErrorBound { stuff = () })
+ vcs := create_property !vcs l (ErrorBound (decl, name))
let box_of id = List.map Dag.Property.data (property_of !vcs id)
- let delete_proof_task_box_of id =
- List.iter (fun x -> vcs := delete_property !vcs x)
- (List.filter (fun x ->
- match Dag.Property.data x with ProofTask _ -> true | _ -> false)
- (Vcs_.property_of !vcs id))
+ let delete_boxes_of id =
+ List.iter (fun x -> vcs := delete_property !vcs x) (property_of !vcs id)
let proof_task_box_of id =
match
CList.map_filter (function ProofTask x -> Some x | _ -> None) (box_of id)
@@ -1046,6 +1066,66 @@ let _ = Errors.register_handler (function
| RemoteException ppcmd -> ppcmd
| _ -> raise Unhandled)
+(****************** proof structure for error recovery ************************)
+(******************************************************************************)
+
+type document_node = {
+ indentation : int;
+ ast : Vernacexpr.vernac_expr;
+ id : Stateid.t;
+}
+
+type document_view = {
+ entry_point : document_node;
+ prev_node : document_node -> document_node option;
+}
+
+type static_block_detection =
+ document_view -> static_block_declaration option
+
+type recovery_action = {
+ base_state : Stateid.t;
+ goals_to_admit : Goal.goal list;
+ recovery_command : Vernacexpr.vernac_expr option;
+}
+
+type dynamic_block_error_recovery =
+ static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
+
+let proof_block_delimiters = ref []
+
+let register_proof_block_delimiter name static dynamic =
+ if List.mem_assoc name !proof_block_delimiters then
+ Errors.errorlabstrm "STM" (str "Duplicate block delimiter " ++ str name);
+ proof_block_delimiters := (name, (static,dynamic)) :: !proof_block_delimiters
+
+let mk_doc_node id = function
+ | { step = `Cmd { ctac; cast = { indentation; expr }}; next } when ctac ->
+ Some { indentation; ast = expr; id }
+ | { step = `Sideff (`Ast ({ indentation; expr }, _)); next } ->
+ Some { indentation; ast = expr; id }
+ | _ -> None
+let prev_node { id } =
+ let id = (VCS.visit id).next in
+ mk_doc_node id (VCS.visit id)
+let cur_node id = mk_doc_node id (VCS.visit id)
+
+let detect_proof_block id = function
+ | None -> ()
+ | Some name ->
+ match cur_node id with
+ | None -> ()
+ | Some entry_point -> try
+ let static, _ = List.assoc name !proof_block_delimiters in
+ begin match static { prev_node; entry_point } with
+ | None -> ()
+ | Some ({ start; stop } as decl) ->
+ VCS.create_error_bound_box decl name
+ end
+ with Not_found ->
+ Errors.errorlabstrm "STM"
+ (str "Unknown proof block delimiter " ++ str name)
+
(****************************** THE SCHEDULER *********************************)
(******************************************************************************)
@@ -1601,7 +1681,7 @@ end = struct (* {{{ *)
List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0))
Evd.(evar_context g))
then
- Errors.errorlabstrm "Stm" (strbrk("the par: goal selector supports ground "^
+ Errors.errorlabstrm "STM" (strbrk("the par: goal selector supports ground "^
"goals only"))
else begin
let (i, ast) = r_ast in
@@ -1609,12 +1689,12 @@ end = struct (* {{{ *)
vernac_interp r_state_fb ast;
let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
match Evd.(evar_body (find sigma r_goal)) with
- | Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress")
+ | Evd.Evar_empty -> Errors.errorlabstrm "STM" (str "no progress")
| Evd.Evar_defined t ->
let t = Evarutil.nf_evar sigma t in
if Evarutil.is_ground_term sigma t then
t, Evd.evar_universe_context sigma
- else Errors.errorlabstrm "Stm" (str"The solution is not ground")
+ else Errors.errorlabstrm "STM" (str"The solution is not ground")
end) ()
in
RespBuiltSubProof (t,uc)
@@ -1897,6 +1977,53 @@ let log_processing_sync id name reason = log_string Printf.(sprintf
let wall_clock_last_fork = ref 0.0
let known_state ?(redefine_qed=false) ~cache id =
+
+ let error_absorbing_tactic id exn =
+ let boxes = VCS.box_of id in
+ let valid_boxes = CList.map_filter (function
+ | ErrorBound ({ stop } as decl, name) when Stateid.equal stop id ->
+ Some (decl, name)
+ | _ -> None) boxes in
+ assert(List.length valid_boxes < 2);
+ if valid_boxes = [] then iraise exn
+ else
+ let decl, name = List.hd valid_boxes in
+ try
+ let _, dynamic_check = List.assoc name !proof_block_delimiters in
+ match dynamic_check decl with
+ | `Leaks -> iraise exn
+ | `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin
+ let tac =
+ let open Proofview.Notations in
+ Proofview.Unsafe.tclSETGOALS goals_to_admit <*>
+ Proofview.give_up in
+ match (VCS.get_info base_state).state with
+ | Valid { proof } ->
+ Proof_global.unfreeze proof;
+ Proof_global.with_current_proof (fun _ p ->
+ Pp.feedback ~state_id:id Feedback.AddedAxiom;
+ fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ());
+ Option.iter (fun expr -> vernac_interp id {
+ verbose = true; loc = Loc.ghost; expr; indentation = 0;
+ strlen = 0 })
+ recovery_command
+ | _ -> assert false
+ end
+ with Not_found ->
+ Errors.errorlabstrm "STM"
+ (str "Unknown proof block delimiter " ++ str name)
+ in
+
+ (* Absorb tactic errors from f () *)
+ let resilient_tactic id f =
+ try f ()
+ with e when Errors.noncritical e ->
+ let ie = Errors.push e in
+ error_absorbing_tactic id ie in
+ (* Absorb errors from f x *)
+ let resilient_command f x =
+ try f x
+ with e when Errors.noncritical e -> () in
(* ugly functions to process nested lemmas, i.e. hard to reproduce
* side effects *)
@@ -1928,25 +2055,34 @@ let known_state ?(redefine_qed=false) ~cache id =
| `Cmd { cast = x; cqueue = `SkipQueue } -> (fun () ->
reach view.next), cache, true
| `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () ->
- reach ~cache:`Shallow view.next;
- Hooks.(call tactic_being_run true);
- Partac.vernac_interp
- cancel !Flags.async_proofs_n_tacworkers view.next id x;
- Hooks.(call tactic_being_run false)
+ resilient_tactic id (fun () ->
+ reach ~cache:`Shallow view.next;
+ Hooks.(call tactic_being_run true);
+ Partac.vernac_interp
+ cancel !Flags.async_proofs_n_tacworkers view.next id x;
+ Hooks.(call tactic_being_run false))
), cache, true
| `Cmd { cast = x; cqueue = `QueryQueue cancel }
when Flags.async_proofs_is_master () -> (fun () ->
reach view.next;
Query.vernac_interp cancel view.next id x
), cache, false
- | `Cmd { cast = x; ceff = eff; ctac } -> (fun () ->
- reach view.next;
- if ctac then Hooks.(call tactic_being_run true);
+ | `Cmd { cast = x; ceff = eff; ctac = true } -> (fun () ->
+ resilient_tactic id (fun () ->
+ reach view.next;
+ Hooks.(call tactic_being_run true);
+ vernac_interp id x;
+ Hooks.(call tactic_being_run false));
+ if eff then update_global_env ()
+ ), (if eff then `Yes else cache), true
+ | `Cmd { cast = x; ceff = eff } -> (fun () ->
+ resilient_command reach view.next;
vernac_interp id x;
- if ctac then Hooks.(call tactic_being_run false);
- if eff then update_global_env ()), (if eff then `Yes else cache), true
+ if eff then update_global_env ()
+ ), (if eff then `Yes else cache), true
| `Fork ((x,_,_,_), None) -> (fun () ->
- reach view.next; vernac_interp id x;
+ resilient_command reach view.next;
+ vernac_interp id x;
wall_clock_last_fork := Unix.gettimeofday ()
), `Yes, true
| `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *)
@@ -2337,11 +2473,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
Backtrack.record ();
finish ();
`Ok
- | VtProofStep paral, w ->
+ | VtProofStep { parallel; proof_block_detection }, w ->
let id = VCS.new_node ~id:newtip () in
- let queue = if paral then `TacQueue (ref false) else `MainQueue in
+ let queue = if parallel then `TacQueue (ref false) else `MainQueue in
VCS.commit id (Cmd {
ctac = true;ceff = false;cast = x;cids = [];cqueue = queue });
+ detect_proof_block id proof_block_detection;
Backtrack.record (); if w == VtNow then finish (); `Ok
| VtQed keep, w ->
let valid = if tty then Some(VCS.get_branch_pos head) else None in
@@ -2524,7 +2661,7 @@ let edit_at id =
| _ -> anomaly (str "ProofTask not ending with Qed") in
VCS.branch ~root:master_id ~pos:id
VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch));
- VCS.delete_proof_task_box_of id;
+ VCS.delete_boxes_of id;
cancel_switch := true;
Reach.known_state ~cache:(interactive ()) id;
VCS.checkout_shallowest_proof_branch ();
@@ -2545,7 +2682,7 @@ let edit_at id =
VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos
(Option.default brname bn)
(no_edit brinfo.VCS.kind);
- VCS.delete_proof_task_box_of id;
+ VCS.delete_boxes_of id;
VCS.gc ();
VCS.print ();
if not !Flags.async_proofs_full then
@@ -2562,7 +2699,7 @@ let edit_at id =
| _ -> None in
match focused, VCS.proof_task_box_of id, branch_info with
| _, Some _, None -> assert false
- | false, Some { qed = qed_id ; start }, Some(mode,bn) ->
+ | false, Some { qed = qed_id ; lemma = start }, Some(mode,bn) ->
let tip = VCS.cur_tip () in
if has_failed qed_id && is_pure qed_id && not !Flags.async_proofs_never_reopen_branch
then reopen_branch start id mode qed_id tip bn
diff --git a/stm/stm.mli b/stm/stm.mli
index d825ff33eb..20dd40bcd4 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -20,7 +20,9 @@ open Loc
The sentence [s] is parsed in the state [ontop].
If [newtip] is provided, then the returned state id is guaranteed to be
[newtip] *)
-val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(vernac_expr located -> unit) ->
+val add :
+ ontop:Stateid.t -> ?newtip:Stateid.t ->
+ ?check:(vernac_expr located -> unit) ->
bool -> edit_id -> string ->
Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
@@ -96,6 +98,82 @@ module ProofTask : AsyncTaskQueue.Task
module TacTask : AsyncTaskQueue.Task
module QueryTask : AsyncTaskQueue.Task
+(** document structure customization *************************************** **)
+
+(* A proof block delimiter defines a syntactic delimiter for sub proofs
+ that, when contain an error, do not impact the rest of the proof.
+ While checking a proof, if an error occurs in a (valid) block then
+ processing can skip the entire block and go on to give feedback
+ on the rest of the proof.
+
+ static_block_detection and dynamic_block_validation are run when
+ the closing block marker is parsed/executed respectively.
+
+ static_block_detection is for example called when "}" is parsed and
+ declares a block containing all proof steps between it and the matching
+ "{".
+
+ dynamic_block_validation is called when an error "crosses" the "}" statement.
+ Depending on the nature of the goal focused by "{" the block may absorb the
+ error or not. For example if the focused goal occurs in the type of
+ another goal, then the block is leaky.
+ Note that one can design proof commands that need no dynamic validation.
+
+ Example of document:
+
+ .. { tac1. tac2. } ..
+
+ Corresponding DAG:
+
+ .. (3) <-- { -- (4) <-- tac1 -- (5) <-- tac2 -- (6) <-- } -- (7) ..
+
+ Declaration of block [-------------------------------------------]
+
+ start = 5 the first state_id that could fail in the block
+ stop = 6 the node that may absorb the error
+ dynamic_switch = 4 dynamic check on this node
+ carry_on_data = () no need to carry extra data from static to dynamic
+ checks
+*)
+
+module DynBlockData : Dyn.S
+
+type static_block_declaration = {
+ start : Stateid.t;
+ stop : Stateid.t;
+ dynamic_switch : Stateid.t;
+ carry_on_data : DynBlockData.t;
+}
+
+type document_node = {
+ indentation : int;
+ ast : Vernacexpr.vernac_expr;
+ id : Stateid.t;
+}
+
+type document_view = {
+ entry_point : document_node;
+ prev_node : document_node -> document_node option;
+}
+
+type static_block_detection =
+ document_view -> static_block_declaration option
+
+type recovery_action = {
+ base_state : Stateid.t;
+ goals_to_admit : Goal.goal list;
+ recovery_command : Vernacexpr.vernac_expr option;
+}
+
+type dynamic_block_error_recovery =
+ static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
+
+val register_proof_block_delimiter :
+ Vernacexpr.proof_block_name ->
+ static_block_detection ->
+ dynamic_block_error_recovery ->
+ unit
+
(** customization ********************************************************** **)
(* From the master (or worker, but beware that to install the hook
@@ -122,7 +200,8 @@ type state = {
proof : Proof_global.state;
shallow : bool
}
-val state_of_id : Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
+val state_of_id :
+ Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
(** read-eval-print loop compatible interface ****************************** **)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index b1df3c9ca6..aa9907045d 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -21,8 +21,9 @@ let string_of_vernac_type = function
| VtQed VtKeep -> "Qed(keep)"
| VtQed VtKeepAsAxiom -> "Qed(admitted)"
| VtQed VtDrop -> "Qed(drop)"
- | VtProofStep false -> "ProofStep"
- | VtProofStep true -> "ProofStep (parallel)"
+ | VtProofStep { parallel; proof_block_detection } ->
+ "ProofStep " ^ if parallel then "par " else "" ^
+ Option.default "" proof_block_detection
| VtProofMode s -> "ProofMode " ^ s
| VtQuery (b,(id,route)) ->
"Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^
@@ -93,7 +94,9 @@ let rec classify_vernac e =
(match classify_vernac e with
| ( VtQuery _ | VtProofStep _ | VtSideff _
| VtStm _ | VtProofMode _ ), _ as x -> x
- | VtQed _, _ -> VtProofStep false, VtNow
+ | VtQed _, _ ->
+ VtProofStep { parallel = false; proof_block_detection = None },
+ VtNow
| (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
(* Qed *)
| VernacAbort _ -> VtQed VtDrop, VtLater
@@ -110,7 +113,7 @@ let rec classify_vernac e =
| VernacSubproof _ | VernacEndSubproof
| VernacCheckGuard
| VernacUnfocused
- | VernacSolveExistential _ -> VtProofStep false, VtLater
+ | VernacSolveExistential _ -> VtProofStep { parallel = false; proof_block_detection = None }, VtLater
(* Options changing parser *)
| VernacUnsetOption (["Default";"Proof";"Using"])
| VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
@@ -219,4 +222,4 @@ let rec classify_vernac e =
let classify_as_query =
VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
let classify_as_sideeff = VtSideff [], VtLater
-let classify_as_proofstep = VtProofStep false, VtLater
+let classify_as_proofstep = VtProofStep { parallel = false; proof_block_detection = None}, VtLater
--
cgit v1.2.3
From f6cea698f19766087fa56b16ed8dc8cedf079643 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 May 2016 11:12:28 +0200
Subject: STM: proof block detection for bullets and { block }
---
engine/proofview.mli | 3 ++
stm/proofBlockDelimiter.ml | 127 ++++++++++++++++++++++++++++++++++++++++++++
stm/proofBlockDelimiter.mli | 39 ++++++++++++++
stm/stm.mllib | 1 +
stm/vernac_classifier.ml | 13 +++--
5 files changed, 180 insertions(+), 3 deletions(-)
create mode 100644 stm/proofBlockDelimiter.ml
create mode 100644 stm/proofBlockDelimiter.mli
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 7996b7969c..93ba55c61f 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -303,6 +303,9 @@ val guard_no_unifiable : Names.Name.t list option tactic
goals of p *)
val unshelve : Goal.goal list -> proofview -> proofview
+(** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *)
+val depends_on : Evd.evar_map -> Goal.goal -> Goal.goal -> bool
+
(** [with_shelf tac] executes [tac] and returns its result together with the set
of goals shelved by [tac]. The current shelf is unchanged. *)
val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
new file mode 100644
index 0000000000..1e37209edd
--- /dev/null
+++ b/stm/proofBlockDelimiter.ml
@@ -0,0 +1,127 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* Goal.goal -> Goal.goal list -> bool
+val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ]
+
+type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
+
+val crawl :
+ document_view -> ?init:document_node option ->
+ ('a -> document_node -> 'a until) -> 'a ->
+ static_block_declaration option
+
+val unit_val : Stm.DynBlockData.t
+val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
+val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
+
+end = struct
+
+let unit_tag = DynBlockData.create "unit"
+let unit_val = DynBlockData.Easy.inj () unit_tag
+
+let of_bullet_val, to_bullet_val = DynBlockData.Easy.make_dyn "bullet"
+
+let simple_goal sigma g gs =
+ let open Evar in
+ let open Evd in
+ let open Evarutil in
+ let evi = Evd.find sigma g in
+ Set.is_empty (evars_of_term evi.evar_concl) &&
+ Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) &&
+ not (List.exists (Proofview.depends_on sigma g) gs)
+
+let is_focused_goal_simple id =
+ match state_of_id id with
+ | `Expired | `Error _ | `Valid None -> `Not
+ | `Valid (Some { 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
+ if List.for_all (fun x -> simple_goal sigma x rest) focused
+ then `Simple focused
+ else `Not
+
+type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
+
+let crawl { entry_point; prev_node } ?(init=Some entry_point) f acc =
+ let rec crawl node acc =
+ match node with
+ | None -> None
+ | Some node ->
+ match f acc node with
+ | `Stop -> None
+ | `Found x -> Some x
+ | `Cont acc -> crawl (prev_node node) acc in
+ crawl init acc
+
+end
+
+include Util
+
+(* ****************** - foo - bar - baz *********************************** *)
+
+let static_bullet ({ entry_point; prev_node } as view) =
+ match entry_point.ast with
+ | Vernacexpr.VernacBullet b ->
+ let base = entry_point.indentation in
+ let last_tac = prev_node entry_point in
+ crawl view ~init:last_tac (fun prev node ->
+ if node.indentation < base then `Stop else
+ if node.indentation > base then `Cont node else
+ match node.ast with
+ | Vernacexpr.VernacBullet b' when b = b' ->
+ `Found { stop = entry_point.id; start = prev.id;
+ dynamic_switch = node.id; carry_on_data = of_bullet_val b }
+ | _ -> `Stop) entry_point
+ | _ -> assert false
+
+let dynamic_bullet { dynamic_switch = id; carry_on_data = b } =
+ match is_focused_goal_simple id with
+ | `Simple focused ->
+ `ValidBlock {
+ base_state = id;
+ goals_to_admit = focused;
+ recovery_command = Some (Vernacexpr.VernacBullet (to_bullet_val b))
+ }
+ | `Not -> `Leaks
+
+let () = register_proof_block_delimiter
+ "bullet" static_bullet dynamic_bullet
+
+(* ******************** { block } ***************************************** *)
+
+let static_curly_brace ({ entry_point; prev_node } as view) =
+ assert(entry_point.ast = Vernacexpr.VernacEndSubproof);
+ crawl view (fun (nesting,prev) node ->
+ match node.ast with
+ | Vernacexpr.VernacSubproof _ when nesting = 0 ->
+ `Found { stop = entry_point.id; start = prev.id;
+ dynamic_switch = node.id; carry_on_data = unit_val }
+ | Vernacexpr.VernacSubproof _ ->
+ `Cont (nesting - 1,node)
+ | Vernacexpr.VernacEndSubproof ->
+ `Cont (nesting + 1,node)
+ | _ -> `Cont (nesting,node)) (-1, entry_point)
+
+let dynamic_curly_brace { dynamic_switch = id } =
+ match is_focused_goal_simple id with
+ | `Simple focused ->
+ `ValidBlock {
+ base_state = id;
+ goals_to_admit = focused;
+ recovery_command = Some Vernacexpr.VernacEndSubproof
+ }
+ | `Not -> `Leaks
+
+let () = register_proof_block_delimiter
+ "proof-block" static_curly_brace dynamic_curly_brace
diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli
new file mode 100644
index 0000000000..8455c18485
--- /dev/null
+++ b/stm/proofBlockDelimiter.mli
@@ -0,0 +1,39 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* Goal.goal -> Goal.goal list -> bool
+val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ]
+
+type 'a until = [ `Stop | `Found of Stm.static_block_declaration | `Cont of 'a ]
+
+(* Simpler function to crawl the document backward to detect the block.
+ * ?init is the entry point of the document view if not given *)
+val crawl :
+ Stm.document_view -> ?init:Stm.document_node option ->
+ ('a -> Stm.document_node -> 'a until) -> 'a ->
+ Stm.static_block_declaration option
+
+(* Dummy value for static_block_declaration when no real value is needed *)
+val unit_val : Stm.DynBlockData.t
+
+(* Bullets *)
+val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
+val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
diff --git a/stm/stm.mllib b/stm/stm.mllib
index bd792b01f6..939ee187ae 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -8,4 +8,5 @@ Lemmas
CoqworkmgrApi
AsyncTaskQueue
Stm
+ProofBlockDelimiter
Vio_checking
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index aa9907045d..11e973bf56 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -108,12 +108,19 @@ let rec classify_vernac e =
VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
(* ProofStep *)
| VernacProof _
- | VernacBullet _
| VernacFocus _ | VernacUnfocus
- | VernacSubproof _ | VernacEndSubproof
+ | VernacSubproof _
| VernacCheckGuard
| VernacUnfocused
- | VernacSolveExistential _ -> VtProofStep { parallel = false; proof_block_detection = None }, VtLater
+ | VernacSolveExistential _ ->
+ VtProofStep { parallel = false; proof_block_detection = None }, VtLater
+ | VernacBullet _ ->
+ VtProofStep { parallel = false; proof_block_detection = Some "bullet" },
+ VtLater
+ | VernacEndSubproof ->
+ VtProofStep { parallel = false;
+ proof_block_detection = Some "proof-block" },
+ VtLater
(* Options changing parser *)
| VernacUnsetOption (["Default";"Proof";"Using"])
| VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
--
cgit v1.2.3
From 8baf120d5cf5045d188f7d926162643a6e7ebcd0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 May 2016 13:46:43 +0200
Subject: STM: proof block detection for par:
"par: tac" is a terminator, if it fails we can admit all focused goals
and continue.
---
ltac/g_ltac.ml4 | 2 +-
stm/proofBlockDelimiter.ml | 22 ++++++++++++++++++++++
stm/proofBlockDelimiter.mli | 2 ++
3 files changed, 25 insertions(+), 1 deletion(-)
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index c8287a2c8d..7c161e5cdc 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -366,7 +366,7 @@ VERNAC tactic_mode EXTEND VernacSolve
vernac_solve g n t def
]
| [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
- [ VtProofStep{ parallel = true; proof_block_detection = None },
+ [ VtProofStep{ parallel = true; proof_block_detection = Some "par" },
VtLater ] -> [
vernac_solve SelectAll n t def
]
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 1e37209edd..8c50ad9697 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -125,3 +125,25 @@ let dynamic_curly_brace { dynamic_switch = id } =
let () = register_proof_block_delimiter
"proof-block" static_curly_brace dynamic_curly_brace
+
+(* ***************** par: ************************************************* *)
+
+let static_par { entry_point; prev_node } =
+ match prev_node entry_point with
+ | None -> None
+ | Some { id = pid } ->
+ Some { stop = entry_point.id; start = pid;
+ dynamic_switch = pid; carry_on_data = unit_val }
+
+let dynamic_par { dynamic_switch = id } =
+ match is_focused_goal_simple id with
+ | `Simple focused ->
+ `ValidBlock {
+ base_state = id;
+ goals_to_admit = focused;
+ recovery_command = None;
+ }
+ | `Not -> `Leaks
+
+let () = register_proof_block_delimiter "par" static_par dynamic_par
+
diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli
index 8455c18485..a55032a470 100644
--- a/stm/proofBlockDelimiter.mli
+++ b/stm/proofBlockDelimiter.mli
@@ -9,6 +9,7 @@
(* This file implements proof block detection for:
- blocks delimited by { and }
- bullets with indentation
+ - par: terminator
It exports utility functions to ease the development of other proof block
detection code.
@@ -37,3 +38,4 @@ val unit_val : Stm.DynBlockData.t
(* Bullets *)
val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
+
--
cgit v1.2.3
From 821937aee71bf9439158e27e06f7b4f74289b209 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 May 2016 16:57:31 +0200
Subject: STM: proof block detection made optional + simple test
---
lib/flags.ml | 2 ++
lib/flags.mli | 2 ++
stm/stm.ml | 31 +++++++++++++-------
stm/stm.mli | 2 +-
test-suite/interactive/proof_block.v | 56 ++++++++++++++++++++++++++++++++++++
toplevel/coqtop.ml | 4 +++
6 files changed, 86 insertions(+), 11 deletions(-)
create mode 100644 test-suite/interactive/proof_block.v
diff --git a/lib/flags.ml b/lib/flags.ml
index c1ec9738ca..ecf3c3f168 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -68,6 +68,8 @@ let priority_of_string = function
| "low" -> Low
| "high" -> High
| _ -> raise (Invalid_argument "priority_of_string")
+let async_proofs_tac_error_resilience = ref true
+let async_proofs_cmd_error_resilience = ref true
let async_proofs_is_worker () =
!async_proofs_worker_id <> "master"
diff --git a/lib/flags.mli b/lib/flags.mli
index 24780f0dcc..b26ef027c6 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -34,6 +34,8 @@ type priority = Low | High
val async_proofs_worker_priority : priority ref
val string_of_priority : priority -> string
val priority_of_string : string -> priority
+val async_proofs_tac_error_resilience : bool ref
+val async_proofs_cmd_error_resilience : bool ref
val debug : bool ref
val in_debugger : bool ref
diff --git a/stm/stm.ml b/stm/stm.ml
index 35f7295dd6..c1158928df 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1111,9 +1111,9 @@ let prev_node { id } =
let cur_node id = mk_doc_node id (VCS.visit id)
let detect_proof_block id = function
- | None -> ()
- | Some name ->
- match cur_node id with
+ | Some name when !Flags.async_proofs_tac_error_resilience &&
+ !Flags.async_proofs_mode != Flags.APoff ->
+ begin match cur_node id with
| None -> ()
| Some entry_point -> try
let static, _ = List.assoc name !proof_block_delimiters in
@@ -1124,7 +1124,8 @@ let detect_proof_block id = function
end
with Not_found ->
Errors.errorlabstrm "STM"
- (str "Unknown proof block delimiter " ++ str name)
+ (str "Unknown proof block delimiter " ++ str name) end
+ | _ -> ()
(****************************** THE SCHEDULER *********************************)
(******************************************************************************)
@@ -2016,14 +2017,24 @@ let known_state ?(redefine_qed=false) ~cache id =
(* Absorb tactic errors from f () *)
let resilient_tactic id f =
- try f ()
- with e when Errors.noncritical e ->
- let ie = Errors.push e in
- error_absorbing_tactic id ie in
+ if not !Flags.async_proofs_tac_error_resilience ||
+ (Flags.async_proofs_is_master () &&
+ !Flags.async_proofs_mode = Flags.APoff)
+ then f ()
+ else
+ try f ()
+ with e when Errors.noncritical e ->
+ let ie = Errors.push e in
+ error_absorbing_tactic id ie in
(* Absorb errors from f x *)
let resilient_command f x =
- try f x
- with e when Errors.noncritical e -> () in
+ if not !Flags.async_proofs_cmd_error_resilience ||
+ (Flags.async_proofs_is_master () &&
+ !Flags.async_proofs_mode = Flags.APoff)
+ then f x
+ else
+ try f x
+ with e when Errors.noncritical e -> () in
(* ugly functions to process nested lemmas, i.e. hard to reproduce
* side effects *)
diff --git a/stm/stm.mli b/stm/stm.mli
index 20dd40bcd4..37ec1f0a13 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -130,7 +130,7 @@ module QueryTask : AsyncTaskQueue.Task
Declaration of block [-------------------------------------------]
start = 5 the first state_id that could fail in the block
- stop = 6 the node that may absorb the error
+ stop = 7 the node that may absorb the error
dynamic_switch = 4 dynamic check on this node
carry_on_data = () no need to carry extra data from static to dynamic
checks
diff --git a/test-suite/interactive/proof_block.v b/test-suite/interactive/proof_block.v
new file mode 100644
index 0000000000..ff920b671e
--- /dev/null
+++ b/test-suite/interactive/proof_block.v
@@ -0,0 +1,56 @@
+
+Lemma baz : (exists n, n = 3 /\ n = 3) /\ True.
+Proof.
+split. { eexists. split. par: trivial. }
+trivial.
+Qed.
+
+Lemma baz1 : (True /\ False) /\ True.
+Proof.
+split. { split. par: trivial. }
+trivial.
+Qed.
+
+Lemma foo : (exists n, n = 3 /\ n = 3) /\ True.
+Proof.
+split.
+ { idtac.
+ unshelve eexists.
+ { apply 3. }
+ { split.
+ { idtac. trivialx. }
+ { reflexivity. } } }
+ trivial.
+Qed.
+
+Lemma foo1 : False /\ True.
+Proof.
+split.
+ exact I.
+ { exact I. }
+Qed.
+
+Definition banana := true + 4.
+
+Check banana.
+
+Lemma bar : (exists n, n = 3 /\ n = 3) /\ True.
+Proof.
+split.
+ - idtac.
+ unshelve eexists.
+ + apply 3.
+ + split.
+ * idtacx. trivial.
+ * reflexivity.
+ - trivial.
+Qed.
+
+Lemma baz2 : ((1=0 /\ False) /\ True) /\ False.
+Proof.
+split. split. split.
+ - solve [ auto ].
+ - solve [ trivial ].
+ - solve [ trivial ].
+ - exact 6.
+Qed.
\ No newline at end of file
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 869f6bb931..c52830ea76 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -492,6 +492,10 @@ let parse_args arglist =
Flags.async_proofs_worker_priority := get_priority opt (next ())
|"-async-proofs-private-flags" ->
Flags.async_proofs_private_flags := Some (next ());
+ |"-async-proofs-tactic-error-resilience" ->
+ Flags.async_proofs_tac_error_resilience := get_bool opt (next ())
+ |"-async-proofs-command-error-resilience" ->
+ Flags.async_proofs_cmd_error_resilience := get_bool opt (next ())
|"-worker-id" -> set_worker_id opt (next ())
|"-compat" -> let v = get_compat_version (next ()) in Flags.compat_version := v; add_compat_require v
|"-compile" -> add_compile false (next ())
--
cgit v1.2.3
From ca833edfb9ce2a40b0b83b11a825ae5dc833c4cb Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 May 2016 18:08:43 +0200
Subject: STM: fix error reporting of par:
---
stm/stm.ml | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/stm/stm.ml b/stm/stm.ml
index c1158928df..a3e380c7b7 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1653,8 +1653,7 @@ end = struct (* {{{ *)
match resp with
| RespBuiltSubProof o -> t_assign (`Val o); `Stay ((),[])
| RespError msg ->
- let info = Stateid.add ~valid:t_state Exninfo.null t_state_fb in
- let e = (RemoteException msg, info) in
+ let e = (RemoteException msg, Exninfo.null) in
t_assign (`Exn e);
t_kill ();
`Stay ((),[])
--
cgit v1.2.3
From e47f9b21b656fa31154bd52b1e155ccf059e89a3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sun, 5 Jun 2016 14:00:43 +0200
Subject: rebase on trunk
---
stm/stm.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/stm/stm.ml b/stm/stm.ml
index a3e380c7b7..89d384fdd3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2001,7 +2001,7 @@ let known_state ?(redefine_qed=false) ~cache id =
| Valid { proof } ->
Proof_global.unfreeze proof;
Proof_global.with_current_proof (fun _ p ->
- Pp.feedback ~state_id:id Feedback.AddedAxiom;
+ feedback ~id:(State id) Feedback.AddedAxiom;
fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ());
Option.iter (fun expr -> vernac_interp id {
verbose = true; loc = Loc.ghost; expr; indentation = 0;
--
cgit v1.2.3
From 0307140281395e8ffa16f2af9f946cc53d540b17 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 6 Jun 2016 05:50:45 -0400
Subject: STM: proof block detection for indentation
---
stm/proofBlockDelimiter.ml | 32 ++++++++++++++++++++++++++++++++
1 file changed, 32 insertions(+)
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 8c50ad9697..7dec43d1a4 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -147,3 +147,35 @@ let dynamic_par { dynamic_switch = id } =
let () = register_proof_block_delimiter "par" static_par dynamic_par
+(* ***************** simple indentation *********************************** *)
+
+let static_indent ({ entry_point; prev_node } as view) =
+ Printf.eprintf "@%d\n" (Stateid.to_int entry_point.id);
+ match prev_node entry_point with
+ | None -> None
+ | Some last_tac ->
+ if last_tac.indentation <= entry_point.indentation then None
+ else
+ crawl view ~init:(Some last_tac) (fun prev node ->
+ if node.indentation >= last_tac.indentation then `Cont node
+ else
+ `Found { stop = entry_point.id; start = node.id;
+ dynamic_switch = node.id;
+ carry_on_data = of_vernac_expr_val entry_point.ast }
+ ) last_tac
+
+let dynamic_indent { dynamic_switch = id; carry_on_data = e } =
+ Printf.eprintf "%s\n" (Stateid.to_string id);
+ match is_focused_goal_simple id with
+ | `Simple [] -> `Leaks
+ | `Simple focused ->
+ let but_last = List.tl (List.rev focused) in
+ `ValidBlock {
+ base_state = id;
+ goals_to_admit = but_last;
+ recovery_command = Some (to_vernac_expr_val e);
+ }
+ | `Not -> `Leaks
+
+let () = register_proof_block_delimiter "indent" static_indent dynamic_indent
+
--
cgit v1.2.3
From e4d66a03148243f7611f4d7c164e775877184e03 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 6 Jun 2016 05:50:07 -0400
Subject: Error box detection run only on error
Advantage: 0 cost if no error occurs
Disadvantage: a box *must* end with the error absorbing command
---
stm/proofBlockDelimiter.ml | 3 ++
stm/stm.ml | 87 +++++++++++++++++++++---------------
test-suite/interactive/proof_block.v | 12 ++++-
3 files changed, 64 insertions(+), 38 deletions(-)
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 7dec43d1a4..ed8553d4b9 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -23,6 +23,8 @@ val crawl :
val unit_val : Stm.DynBlockData.t
val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
+val of_vernac_expr_val : Vernacexpr.vernac_expr -> Stm.DynBlockData.t
+val to_vernac_expr_val : Stm.DynBlockData.t -> Vernacexpr.vernac_expr
end = struct
@@ -30,6 +32,7 @@ let unit_tag = DynBlockData.create "unit"
let unit_val = DynBlockData.Easy.inj () unit_tag
let of_bullet_val, to_bullet_val = DynBlockData.Easy.make_dyn "bullet"
+let of_vernac_expr_val, to_vernac_expr_val = DynBlockData.Easy.make_dyn "vernac_expr"
let simple_goal sigma g gs =
let open Evar in
diff --git a/stm/stm.ml b/stm/stm.ml
index 89d384fdd3..0e33bea3b2 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -170,11 +170,13 @@ type branch_type =
| `Proof of proof_mode * depth
| `Edit of
proof_mode * Stateid.t * Stateid.t * vernac_qed_type * Vcs_.Branch.t ]
+(* TODO 8.7 : split commands and tactics, since this type is too messy now *)
type cmd_t = {
ctac : bool; (* is a tactic *)
ceff : bool; (* is a side-effecting command in the middle of a proof *)
cast : aast;
cids : Id.t list;
+ cblock : proof_block_name option;
cqueue : [ `MainQueue
| `TacQueue of cancel_switch
| `QueryQueue of cancel_switch
@@ -204,6 +206,10 @@ type step =
| `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 }
(* Parts of the system state that are morally part of the proof state *)
let summary_pstate = [ Evarutil.meta_counter_summary_name;
@@ -591,7 +597,6 @@ end = struct (* {{{ *)
let props =
Stateid.Set.fold (fun n pl -> Vcs_.property_of !vcs n @ pl) nodes [] in
let props = CList.sort_uniquize Vcs_.Dag.Property.compare props in
- (* XXX check if par: works here, since we copy a single node *)
List.fold_left (fun v p ->
Vcs_.create_property v
(Stateid.Set.elements (Vcs_.Dag.Property.having_it p))
@@ -1110,22 +1115,24 @@ let prev_node { id } =
mk_doc_node id (VCS.visit id)
let cur_node id = mk_doc_node id (VCS.visit id)
-let detect_proof_block id = function
- | Some name when !Flags.async_proofs_tac_error_resilience &&
- !Flags.async_proofs_mode != Flags.APoff ->
- begin match cur_node id with
+let detect_proof_block id name =
+ let name = match name with None -> "indent" | Some x -> x in
+ if !Flags.async_proofs_tac_error_resilience &&
+ (if Flags.async_proofs_is_master () then
+ !Flags.async_proofs_mode != Flags.APoff else true)
+ then
+ match cur_node id with
+ | None -> ()
+ | Some entry_point -> try
+ let static, _ = List.assoc name !proof_block_delimiters in
+ begin match static { prev_node; entry_point } with
| None -> ()
- | Some entry_point -> try
- let static, _ = List.assoc name !proof_block_delimiters in
- begin match static { prev_node; entry_point } with
- | None -> ()
- | Some ({ start; stop } as decl) ->
- VCS.create_error_bound_box decl name
- end
- with Not_found ->
- Errors.errorlabstrm "STM"
- (str "Unknown proof block delimiter " ++ str name) end
- | _ -> ()
+ | Some ({ start; stop } as decl) ->
+ VCS.create_error_bound_box decl name
+ end
+ with Not_found ->
+ Errors.errorlabstrm "STM"
+ (str "Unknown proof block delimiter " ++ str name)
(****************************** THE SCHEDULER *********************************)
(******************************************************************************)
@@ -1978,7 +1985,12 @@ let wall_clock_last_fork = ref 0.0
let known_state ?(redefine_qed=false) ~cache id =
- let error_absorbing_tactic id exn =
+ let error_absorbing_tactic id blockname exn =
+ (* We keep the static/dynamic part of block detection separate, since
+ the static part could be performed earlier. As of today there is
+ no advantage in doing so since no UI can exploit such piece of info *)
+ detect_proof_block id blockname;
+
let boxes = VCS.box_of id in
let valid_boxes = CList.map_filter (function
| ErrorBound ({ stop } as decl, name) when Stateid.equal stop id ->
@@ -1995,8 +2007,11 @@ let known_state ?(redefine_qed=false) ~cache id =
| `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin
let tac =
let open Proofview.Notations in
- Proofview.Unsafe.tclSETGOALS goals_to_admit <*>
- Proofview.give_up in
+ Proofview.Goal.nf_enter { enter = fun gl ->
+ if CList.mem_f Evar.equal
+ (Proofview.Goal.goal gl) goals_to_admit then
+ Proofview.give_up else Proofview.tclUNIT ()
+ } in
match (VCS.get_info base_state).state with
| Valid { proof } ->
Proof_global.unfreeze proof;
@@ -2015,7 +2030,7 @@ let known_state ?(redefine_qed=false) ~cache id =
in
(* Absorb tactic errors from f () *)
- let resilient_tactic id f =
+ let resilient_tactic id blockname f =
if not !Flags.async_proofs_tac_error_resilience ||
(Flags.async_proofs_is_master () &&
!Flags.async_proofs_mode = Flags.APoff)
@@ -2024,7 +2039,7 @@ let known_state ?(redefine_qed=false) ~cache id =
try f ()
with e when Errors.noncritical e ->
let ie = Errors.push e in
- error_absorbing_tactic id ie in
+ error_absorbing_tactic id blockname ie in
(* Absorb errors from f x *)
let resilient_command f x =
if not !Flags.async_proofs_cmd_error_resilience ||
@@ -2064,8 +2079,8 @@ let known_state ?(redefine_qed=false) ~cache id =
), cache, true
| `Cmd { cast = x; cqueue = `SkipQueue } -> (fun () ->
reach view.next), cache, true
- | `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () ->
- resilient_tactic id (fun () ->
+ | `Cmd { cast = x; cqueue = `TacQueue cancel; cblock } -> (fun () ->
+ resilient_tactic id cblock (fun () ->
reach ~cache:`Shallow view.next;
Hooks.(call tactic_being_run true);
Partac.vernac_interp
@@ -2077,8 +2092,8 @@ let known_state ?(redefine_qed=false) ~cache id =
reach view.next;
Query.vernac_interp cancel view.next id x
), cache, false
- | `Cmd { cast = x; ceff = eff; ctac = true } -> (fun () ->
- resilient_tactic id (fun () ->
+ | `Cmd { cast = x; ceff = eff; ctac = true; cblock } -> (fun () ->
+ resilient_tactic id cblock (fun () ->
reach view.next;
Hooks.(call tactic_being_run true);
vernac_interp id x;
@@ -2443,8 +2458,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
may_pierce_opaque x
then `SkipQueue
else `MainQueue in
- VCS.commit id (Cmd {
- ctac=false;ceff=false;cast = x; cids = []; cqueue = queue });
+ VCS.commit id (mkTransCmd x [] false queue);
Backtrack.record (); if w == VtNow then finish (); `Ok
| VtQuery (false,_), VtLater ->
anomaly(str"classifier: VtQuery + VtLater must imply part_of_script")
@@ -2467,8 +2481,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
anomaly(str"VtProofMode must be executed VtNow")
| VtProofMode mode, VtNow ->
let id = VCS.new_node ~id:newtip () in
- VCS.commit id (Cmd {
- ctac=false;ceff=false;cast = x;cids=[];cqueue = `MainQueue});
+ VCS.commit id (mkTransCmd x [] false `MainQueue);
List.iter
(fun bn -> match VCS.get_branch bn with
| { VCS.root; kind = `Master; pos } -> ()
@@ -2483,12 +2496,14 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
Backtrack.record ();
finish ();
`Ok
- | VtProofStep { parallel; proof_block_detection }, w ->
+ | VtProofStep { parallel; proof_block_detection = cblock }, w ->
let id = VCS.new_node ~id:newtip () in
let queue = if parallel then `TacQueue (ref false) else `MainQueue in
- VCS.commit id (Cmd {
- ctac = true;ceff = false;cast = x;cids = [];cqueue = queue });
- detect_proof_block id proof_block_detection;
+ VCS.commit id (mkTransTac x cblock queue);
+ (* Static proof block detection delayed until an error really occurs.
+ If/when and UI will make something useful with this piece of info,
+ detection should occur here.
+ detect_proof_block id cblock; *)
Backtrack.record (); if w == VtNow then finish (); `Ok
| VtQed keep, w ->
let valid = if tty then Some(VCS.get_branch_pos head) else None in
@@ -2505,8 +2520,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
let id = VCS.new_node ~id:newtip () in
VCS.checkout VCS.Branch.master;
- VCS.commit id (Cmd {
- ctac=false;ceff=in_proof;cast=x;cids=l;cqueue=`MainQueue });
+ VCS.commit id (mkTransCmd x l in_proof `MainQueue);
(* We can't replay a Definition since universes may be differently
* inferred. This holds in Coq >= 8.5 *)
let replay = match x.expr with
@@ -2541,8 +2555,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1));
Proof_global.activate_proof_mode proof_mode;
end else begin
- VCS.commit id (Cmd {
- ctac=false;ceff=in_proof;cast=x;cids=[];cqueue=`MainQueue });
+ VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
(* We hope it can be replayed, but we can't really know *)
VCS.propagate_sideff ~replay:(Some x);
VCS.checkout_shallowest_proof_branch ();
diff --git a/test-suite/interactive/proof_block.v b/test-suite/interactive/proof_block.v
index ff920b671e..31e3493768 100644
--- a/test-suite/interactive/proof_block.v
+++ b/test-suite/interactive/proof_block.v
@@ -1,3 +1,13 @@
+Goal False /\ True.
+Proof.
+split.
+ idtac.
+ idtac.
+ exact I.
+idtac.
+idtac.
+exact I.
+Qed.
Lemma baz : (exists n, n = 3 /\ n = 3) /\ True.
Proof.
@@ -26,7 +36,7 @@ Qed.
Lemma foo1 : False /\ True.
Proof.
split.
- exact I.
+ { exact I. }
{ exact I. }
Qed.
--
cgit v1.2.3
From 845dd3dd17b880999a956839c0d84d46de9e27b8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sun, 5 Jun 2016 21:21:43 +0200
Subject: STM: each proof block can be enabled separately
By default we enable only {} and par: that are detectable in
a complete way.
---
lib/flags.ml | 3 ++-
lib/flags.mli | 3 ++-
stm/stm.ml | 10 ++++++++--
toplevel/coqtop.ml | 7 ++++++-
4 files changed, 18 insertions(+), 5 deletions(-)
diff --git a/lib/flags.ml b/lib/flags.ml
index ecf3c3f168..e78fa7c0c9 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -68,7 +68,8 @@ let priority_of_string = function
| "low" -> Low
| "high" -> High
| _ -> raise (Invalid_argument "priority_of_string")
-let async_proofs_tac_error_resilience = ref true
+type tac_error_filter = [ `None | `Only of string list | `All ]
+let async_proofs_tac_error_resilience = ref (`Only [ "par" ; "proof-block" ])
let async_proofs_cmd_error_resilience = ref true
let async_proofs_is_worker () =
diff --git a/lib/flags.mli b/lib/flags.mli
index b26ef027c6..d729be385b 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -34,7 +34,8 @@ type priority = Low | High
val async_proofs_worker_priority : priority ref
val string_of_priority : priority -> string
val priority_of_string : string -> priority
-val async_proofs_tac_error_resilience : bool ref
+type tac_error_filter = [ `None | `Only of string list | `All ]
+val async_proofs_tac_error_resilience : tac_error_filter ref
val async_proofs_cmd_error_resilience : bool ref
val debug : bool ref
diff --git a/stm/stm.ml b/stm/stm.ml
index 0e33bea3b2..1fd8325e86 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1115,9 +1115,15 @@ let prev_node { id } =
mk_doc_node id (VCS.visit id)
let cur_node id = mk_doc_node id (VCS.visit id)
+let is_block_name_enabled name =
+ match !Flags.async_proofs_tac_error_resilience with
+ | `None -> false
+ | `All -> true
+ | `Only l -> List.mem name l
+
let detect_proof_block id name =
let name = match name with None -> "indent" | Some x -> x in
- if !Flags.async_proofs_tac_error_resilience &&
+ if is_block_name_enabled name &&
(if Flags.async_proofs_is_master () then
!Flags.async_proofs_mode != Flags.APoff else true)
then
@@ -2031,7 +2037,7 @@ let known_state ?(redefine_qed=false) ~cache id =
(* Absorb tactic errors from f () *)
let resilient_tactic id blockname f =
- if not !Flags.async_proofs_tac_error_resilience ||
+ if !Flags.async_proofs_tac_error_resilience = `None ||
(Flags.async_proofs_is_master () &&
!Flags.async_proofs_mode = Flags.APoff)
then f ()
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c52830ea76..e1f5a70c2a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -379,6 +379,11 @@ let get_host_port opt s =
prerr_endline ("Error: host:port or stdfds expected after option "^opt);
exit 1
+let get_error_resilience opt = function
+ | "on" | "all" | "yes" -> `All
+ | "off" | "no" -> `None
+ | s -> `Only (String.split ',' s)
+
let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
let vio_tasks = ref []
@@ -493,7 +498,7 @@ let parse_args arglist =
|"-async-proofs-private-flags" ->
Flags.async_proofs_private_flags := Some (next ());
|"-async-proofs-tactic-error-resilience" ->
- Flags.async_proofs_tac_error_resilience := get_bool opt (next ())
+ Flags.async_proofs_tac_error_resilience := get_error_resilience opt (next ())
|"-async-proofs-command-error-resilience" ->
Flags.async_proofs_cmd_error_resilience := get_bool opt (next ())
|"-worker-id" -> set_worker_id opt (next ())
--
cgit v1.2.3
From 7a9462ce9a3d70ca43c363da3a0782f59c16a120 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 6 Jun 2016 14:06:59 -0400
Subject: Renaming: ErrorBlock -> ProofBlock
Since this is really what they are.
Squashing this renaming back to the root of the feature branch is hard.
---
stm/stm.ml | 18 +++++++++---------
1 file changed, 9 insertions(+), 9 deletions(-)
diff --git a/stm/stm.ml b/stm/stm.ml
index 1fd8325e86..3ac1f98925 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -241,7 +241,7 @@ module DynBlockData : Dyn.S = Dyn.Make(struct end)
* no constraint on properties, here we impose boxes to be non overlapping. *)
type box =
| ProofTask of pt
- | ErrorBound of static_block_declaration * proof_block_name
+ | ProofBlock of static_block_declaration * proof_block_name
and pt = { (* TODO: inline records in OCaml 4.03 *)
lemma : Stateid.t;
qed : Stateid.t;
@@ -357,7 +357,7 @@ module VCS : sig
val nodes_in_slice : start:id -> stop:id -> Stateid.t list
val create_proof_task_box : id list -> qed:id -> start:id -> unit
- val create_error_bound_box : static_block_declaration -> string -> unit
+ val create_proof_block : static_block_declaration -> string -> unit
val box_of : id -> box list
val delete_boxes_of : id -> unit
val proof_task_box_of : id -> pt option
@@ -477,7 +477,7 @@ end = struct (* {{{ *)
end)
(Dag.Property.having_it b);
match Dag.Property.data b with
- | ErrorBound ({ dynamic_switch = id }, lbl) ->
+ | ProofBlock ({ dynamic_switch = id }, lbl) ->
fprintf oc "label=\"%s (test:%s)\";\n" lbl (Stateid.to_string id);
fprintf oc "color=red; }\n"
| ProofTask _ -> fprintf oc "color=blue; }\n"
@@ -592,7 +592,7 @@ end = struct (* {{{ *)
{ (get_info id) with state = Empty; vcs_backup = None,None } in
let copy_info_w_state v id =
Vcs_.set_info v id { (get_info id) with vcs_backup = None,None } in
- let copy_error_bound_boxes v =
+ let copy_proof_blockes v =
let nodes = Vcs_.Dag.all_nodes (Vcs_.dag v) in
let props =
Stateid.Set.fold (fun n pl -> Vcs_.property_of !vcs n @ pl) nodes [] in
@@ -619,7 +619,7 @@ end = struct (* {{{ *)
(* We put in the new dag the first state (since Qed shall run on it,
* see check_task_aux) *)
let v = copy_info_w_state v start in
- copy_error_bound_boxes v
+ copy_proof_blockes v
let nodes_in_slice ~start ~stop =
List.rev (List.map fst (nodes_in_slice ~start ~stop))
@@ -636,10 +636,10 @@ end = struct (* {{{ *)
let create_proof_task_box l ~qed ~start:lemma =
if not (topo_invariant l) then anomaly (str "overlapping boxes");
vcs := create_property !vcs l (ProofTask { qed; lemma })
- let create_error_bound_box ({ start; stop} as decl) name =
+ let create_proof_block ({ start; stop} as decl) name =
let l = nodes_in_slice ~start ~stop in
if not (topo_invariant l) then anomaly (str "overlapping boxes");
- vcs := create_property !vcs l (ErrorBound (decl, name))
+ vcs := create_property !vcs l (ProofBlock (decl, name))
let box_of id = List.map Dag.Property.data (property_of !vcs id)
let delete_boxes_of id =
List.iter (fun x -> vcs := delete_property !vcs x) (property_of !vcs id)
@@ -1134,7 +1134,7 @@ let detect_proof_block id name =
begin match static { prev_node; entry_point } with
| None -> ()
| Some ({ start; stop } as decl) ->
- VCS.create_error_bound_box decl name
+ VCS.create_proof_block decl name
end
with Not_found ->
Errors.errorlabstrm "STM"
@@ -1999,7 +1999,7 @@ let known_state ?(redefine_qed=false) ~cache id =
let boxes = VCS.box_of id in
let valid_boxes = CList.map_filter (function
- | ErrorBound ({ stop } as decl, name) when Stateid.equal stop id ->
+ | ProofBlock ({ stop } as decl, name) when Stateid.equal stop id ->
Some (decl, name)
| _ -> None) boxes in
assert(List.length valid_boxes < 2);
--
cgit v1.2.3
From 4dcd50dd2767c60f8f773fb4ca1c3d4bc68819c8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 7 Jun 2016 09:57:09 -0400
Subject: Documentation
---
doc/refman/AsyncProofs.tex | 37 +++++++++++++++++++++++++++++++++++++
lib/flags.ml | 2 +-
stm/proofBlockDelimiter.ml | 2 +-
stm/stm.ml | 5 ++++-
stm/vernac_classifier.ml | 2 +-
5 files changed, 44 insertions(+), 4 deletions(-)
diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index 7cf5004003..ebd11c168b 100644
--- a/doc/refman/AsyncProofs.tex
+++ b/doc/refman/AsyncProofs.tex
@@ -46,6 +46,43 @@ proof does not begin with \texttt{Proof using}, the system records in an
auxiliary file, produced along with the \texttt{.vo} file, the list of
section variables used.
+\section{Proof blocks and error resilience}
+
+Coq 8.6 introduces a mechanism for error resiliency: in interactive mode Coq
+is able to completely check a document containing errors instead of bailing
+out at the first failure.
+
+Two kind of errors are supported: errors occurring in vernacular commands and
+errors occurring in proofs.
+
+To properly recover from a failing tactic, Coq needs to recognize the structure of
+the proof in order to confine the error to a sub proof. Proof block detection
+is performed by looking at the syntax of the proof script (i.e. also looking at indentation).
+Coq comes with four kind of proof blocks, and an ML API to add new ones.
+
+\begin{description}
+\item[curly] blocks are delimited by \texttt{\{} and \texttt{\}}, see \ref{Proof-handling}
+\item[par] blocks are atomic, i.e. just one tactic introduced by the \texttt{par:} goal selector
+\item[indent] blocks end with a tactic indented less than the previous one
+\item[bullet] blocks are delimited by two equal bullet signs at the same indentation level
+\end{description}
+
+\subsection{Caveats}
+
+When a vernacular command fails the subsequent error messages may be bogus, i.e. caused by
+the first error. Error resiliency for vernacular commands can be switched off passing
+\texttt{-async-proofs-command-error-resilience off} to CoqIDE.
+
+An incorrect proof block detection can result into an incorrect error recovery and
+hence in bogus errors. Proof block detection cannot be precise for bullets or
+any other non well parenthesized proof structure. Error resiliency can be
+turned off or selectively activated for any set of block kind passing to
+CoqIDE one of the following options:
+\texttt{-async-proofs-tactic-error-resilience off},
+\texttt{-async-proofs-tactic-error-resilience all},
+\texttt{-async-proofs-tactic-error-resilience $blocktype_1$,..., $blocktype_n$}.
+Valid proof block types are: ``curly'', ``par'', ``indent'', ``bullet''.
+
\subsubsection{Automatic suggestion of proof annotations}
The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a
diff --git a/lib/flags.ml b/lib/flags.ml
index e78fa7c0c9..16996c144b 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -69,7 +69,7 @@ let priority_of_string = function
| "high" -> High
| _ -> raise (Invalid_argument "priority_of_string")
type tac_error_filter = [ `None | `Only of string list | `All ]
-let async_proofs_tac_error_resilience = ref (`Only [ "par" ; "proof-block" ])
+let async_proofs_tac_error_resilience = ref (`Only [ "par" ; "curly" ])
let async_proofs_cmd_error_resilience = ref true
let async_proofs_is_worker () =
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index ed8553d4b9..ce12185cba 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -127,7 +127,7 @@ let dynamic_curly_brace { dynamic_switch = id } =
| `Not -> `Leaks
let () = register_proof_block_delimiter
- "proof-block" static_curly_brace dynamic_curly_brace
+ "curly" static_curly_brace dynamic_curly_brace
(* ***************** par: ************************************************* *)
diff --git a/stm/stm.ml b/stm/stm.ml
index 3ac1f98925..75d2e070ae 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -238,7 +238,10 @@ let default_info () =
module DynBlockData : Dyn.S = Dyn.Make(struct end)
(* Clusters of nodes implemented as Dag properties. While Dag and Vcs impose
- * no constraint on properties, here we impose boxes to be non overlapping. *)
+ * no constraint on properties, here we impose boxes to be non overlapping.
+ * Such invariant makes sense for the current kinds of boxes (proof blocks and
+ * entire proofs) but may make no sense and dropped/refined in the future.
+ * Such invariant is useful to detect broken proof block detection code *)
type box =
| ProofTask of pt
| ProofBlock of static_block_declaration * proof_block_name
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 11e973bf56..a602d6b8a8 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -119,7 +119,7 @@ let rec classify_vernac e =
VtLater
| VernacEndSubproof ->
VtProofStep { parallel = false;
- proof_block_detection = Some "proof-block" },
+ proof_block_detection = Some "curly" },
VtLater
(* Options changing parser *)
| VernacUnsetOption (["Default";"Proof";"Using"])
--
cgit v1.2.3
From 1334a657052a2385c3f3b01cc65c3ccae448fa96 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 7 Jun 2016 11:47:13 -0400
Subject: CoqIDE: remove useless print
There is little point in telling the user the error report is sub optimal.
In this particular case, such error has already been reported (on
the correct location) so reminding it in a non-localized way is not
even that bad.
---
ide/coqOps.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 9301359957..6ffe771da3 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -741,7 +741,7 @@ object(self)
self#cleanup (Doc.cut_at document to_id);
conclusion ()
| Fail (safe_id, loc, msg) ->
- if loc <> None then messages#push Feedback.Error (Richpp.richpp_of_string "Fixme LOC");
+(* if loc <> None then messages#push Feedback.Error (Richpp.richpp_of_string "Fixme LOC"); *)
messages#push Feedback.Error msg;
if Stateid.equal safe_id Stateid.dummy then self#show_goals
else undo safe_id
--
cgit v1.2.3