aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/asyncTaskQueue.ml9
-rw-r--r--stm/dag.ml94
-rw-r--r--stm/dag.mli50
-rw-r--r--stm/lemmas.ml20
-rw-r--r--stm/lemmas.mli1
-rw-r--r--stm/proofBlockDelimiter.ml184
-rw-r--r--stm/proofBlockDelimiter.mli41
-rw-r--r--stm/spawned.ml13
-rw-r--r--stm/stm.ml831
-rw-r--r--stm/stm.mli91
-rw-r--r--stm/stm.mllib2
-rw-r--r--stm/texmacspp.ml762
-rw-r--r--stm/texmacspp.mli12
-rw-r--r--stm/vcs.ml75
-rw-r--r--stm/vcs.mli66
-rw-r--r--stm/vernac_classifier.ml38
16 files changed, 1063 insertions, 1226 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index c7faef3333..a7b381ad62 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -104,7 +104,8 @@ module Make(T : Task) = struct
marshal_err ("unmarshal_more_data: "^s)
let report_status ?(id = !Flags.async_proofs_worker_id) s =
- Pp.feedback ~state_id:Stateid.initial (Feedback.WorkerStatus(id, s))
+ let open Feedback in
+ feedback ~id:(State Stateid.initial) (WorkerStatus(id, s))
module Worker = Spawn.Sync(struct end)
@@ -123,7 +124,7 @@ module Make(T : Task) = struct
"-async-proofs-worker-priority";
Flags.string_of_priority !Flags.async_proofs_worker_priority]
| ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
- | ("-async-proofs" |"-toploop" |"-vi2vo"
+ | ("-async-proofs" |"-toploop" |"-vio2vo"
|"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv"
|"-compile" |"-compile-verbose"
|"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl ->
@@ -302,8 +303,8 @@ module Make(T : Task) = struct
let main_loop () =
let slave_feeder oc fb =
Marshal.to_channel oc (RespFeedback fb) []; flush oc in
- Pp.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
- Pp.log_via_feedback (fun msg -> Richpp.repr (Richpp.richpp_of_pp msg));
+ Feedback.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
+ Feedback.set_logger Feedback.feedback_logger;
Universes.set_remote_new_univ_level (bufferize (fun () ->
marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
match unmarshal_more_data (Option.get !slave_ic) with
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/lemmas.ml b/stm/lemmas.ml
index 80b3fef196..0a63a3a0fe 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -150,7 +150,7 @@ let find_mutually_recursive_statements thms =
assert (List.is_empty rest);
(* One occ. of common coind ccls and no common inductive hyps *)
if not (List.is_empty common_same_indhyp) then
- if_verbose msg_info (str "Assuming mutual coinductive statements.");
+ if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
flush_all ();
indccl, true, []
| [], _::_ ->
@@ -158,7 +158,7 @@ let find_mutually_recursive_statements thms =
| ind :: _ ->
if List.distinct_f ind_ord (List.map pi1 ind)
then
- if_verbose msg_info
+ if_verbose Feedback.msg_info
(strbrk
("Coinductive statements do not follow the order of "^
"definition, assuming the proof to be by induction."));
@@ -306,7 +306,7 @@ let admit (id,k,e) pl hook () =
let () = match k with
| Global, _, _ -> ()
| Local, _, _ | Discharge, _, _ ->
- msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
+ Feedback.msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
str "declared as an axiom.")
in
let () = assumption_message id in
@@ -336,7 +336,7 @@ let universe_proof_terminator compute_guard hook =
make_terminator begin function
| Admitted (id,k,pe,(ctx,pl)) ->
admit (id,k,pe) pl (hook (Some ctx)) ();
- Pp.feedback Feedback.AddedAxiom
+ Feedback.feedback Feedback.AddedAxiom
| Proved (opaque,idopt,proof) ->
let is_opaque, export_seff, exports = match opaque with
| Vernacexpr.Transparent -> false, true, []
@@ -403,7 +403,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
| Anonymous -> Tactics.intro) (List.rev ids) in
let init_tac,guard = match recguard with
| Some (finite,guard,init_tac) ->
- let rec_tac = Proofview.V82.tactic (rec_tac_initializer finite guard thms snl) in
+ let rec_tac = rec_tac_initializer finite guard thms snl in
Some (match init_tac with
| None ->
if Flags.is_auto_intros () then
@@ -520,13 +520,5 @@ let save_proof ?proof = function
(* Miscellaneous *)
let get_current_context () =
- try Pfedit.get_current_goal_context ()
- with e when Logic.catchable_exception e ->
- try (* No more focused goals ? *)
- let p = Pfedit.get_pftreestate () in
- let evd = Proof.in_proof p (fun x -> x) in
- (evd, Global.env ())
- with Proof_global.NoCurrentProof ->
- let env = Global.env () in
- (Evd.from_env env, env)
+ Pfedit.get_current_context ()
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index 9120787d1c..f751598f04 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -65,4 +65,3 @@ val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> uni
and the current global env *)
val get_current_context : unit -> Evd.evar_map * Environ.env
-
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
new file mode 100644
index 0000000000..ce12185cba
--- /dev/null
+++ b/stm/proofBlockDelimiter.ml
@@ -0,0 +1,184 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Stm
+
+module Util : sig
+
+val simple_goal : Evd.evar_map -> 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
+val of_vernac_expr_val : Vernacexpr.vernac_expr -> Stm.DynBlockData.t
+val to_vernac_expr_val : Stm.DynBlockData.t -> Vernacexpr.vernac_expr
+
+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 of_vernac_expr_val, to_vernac_expr_val = DynBlockData.Easy.make_dyn "vernac_expr"
+
+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
+ "curly" 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
+
+(* ***************** 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
+
diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli
new file mode 100644
index 0000000000..a55032a470
--- /dev/null
+++ b/stm/proofBlockDelimiter.mli
@@ -0,0 +1,41 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* 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.
+*)
+
+(** A goal is simple if it nor depends on nor impacts on any other goal.
+ This function is used to detect, dynamically, if a proof block leaks,
+ i.e. if skipping it could impact other goals (like not instantiating their
+ type). `Simple carries the list of focused goals.
+*)
+val simple_goal : Evd.evar_map -> 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/spawned.ml b/stm/spawned.ml
index c6df872679..2eae6f5e24 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -13,19 +13,6 @@ let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
type chandescr = AnonPipe | Socket of string * int * int
-let handshake cin cout =
- try
- match input_value cin with
- | Hello(v, pid) when v = proto_version ->
- prerr_endline (Printf.sprintf "Handshake with %d OK" pid);
- output_value cout (Hello (proto_version,Unix.getpid ())); flush cout
- | _ -> raise (Failure "handshake protocol")
- with
- | Failure s | Invalid_argument s | Sys_error s ->
- pr_err ("Handshake failed: " ^ s); raise (Failure "handshake")
- | End_of_file ->
- pr_err "Handshake failed: End_of_file"; raise (Failure "handshake")
-
let open_bin_connection h pr pw =
let open Unix in
let _, cout = open_connection (ADDR_INET (inet_addr_of_string h,pr)) in
diff --git a/stm/stm.ml b/stm/stm.ml
index 92032e9bc3..c0813827de 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -8,8 +8,8 @@
let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
-let prerr_endline s = if false then begin pr_err s end else ()
-let prerr_debug s = if !Flags.debug then begin pr_err s end else ()
+let prerr_endline s = if false then begin pr_err (s ()) end else ()
+let prerr_debug s = if !Flags.debug then begin pr_err (s ()) end else ()
open Vernacexpr
open Errors
@@ -18,6 +18,7 @@ open Names
open Util
open Ppvernac
open Vernac_classifier
+open Feedback
module Hooks = struct
@@ -27,28 +28,23 @@ let with_fail, with_fail_hook = Hook.make ()
let state_computed, state_computed_hook = Hook.make
~default:(fun state_id ~in_cache ->
- feedback ~state_id Feedback.Processed) ()
+ feedback ~id:(State state_id) Processed) ()
let state_ready, state_ready_hook = Hook.make
~default:(fun state_id -> ()) ()
let forward_feedback, forward_feedback_hook = Hook.make
~default:(function
- | { Feedback.id = Feedback.Edit edit_id; route; contents } ->
- feedback ~edit_id ~route contents
- | { Feedback.id = Feedback.State state_id; route; contents } ->
- feedback ~state_id ~route contents) ()
+ | { id = id; route; contents } ->
+ feedback ~id:id ~route contents) ()
let parse_error, parse_error_hook = Hook.make
- ~default:(function
- | Feedback.Edit edit_id -> fun loc msg ->
- feedback ~edit_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))
- | Feedback.State state_id -> fun loc msg ->
- feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) ()
+ ~default:(fun id loc msg ->
+ feedback ~id (ErrorMsg (loc, Pp.string_of_ppcmds msg))) ()
let execution_error, execution_error_hook = Hook.make
~default:(fun state_id loc msg ->
- feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) ()
+ feedback ~id:(State state_id) (ErrorMsg (loc, Pp.string_of_ppcmds msg))) ()
let unreachable_state, unreachable_state_hook = Hook.make
~default:(fun _ _ -> ()) ()
@@ -80,12 +76,20 @@ 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 ()
(* Commands piercing opaque *)
let may_pierce_opaque = function
- | { expr = VernacPrint (PrintName _) } -> true
+ | { expr = VernacPrint _ } -> true
| { expr = VernacExtend (("Extraction",_), _) } -> true
| { expr = VernacExtend (("SeparateExtraction",_), _) } -> true
| { expr = VernacExtend (("ExtractionLibrary",_), _) } -> true
@@ -101,14 +105,14 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
| VernacResetName _ | VernacResetInitial | VernacBack _
| VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
| VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
- | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> internal_command e
+ | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> internal_command e
| _ -> false in
if internal_command expr then begin
- prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr))
+ prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr))
end else begin
- set_id_for_feedback ?route (Feedback.State id);
+ set_id_for_feedback ?route (State id);
Aux_file.record_in_aux_set_at loc;
- prerr_endline ("interpreting " ^ string_of_ppcmds(pr_vernac expr));
+ prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr))
with e ->
let e = Errors.push e in
@@ -116,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 Feedback.Edit eid
- else Feedback.State (Option.get newtip) in
+ 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
@@ -136,13 +154,13 @@ let vernac_parse ?newtip ?route eid s =
let pr_open_cur_subgoals () =
try Printer.pr_open_subgoals ()
- with Proof_global.NoCurrentProof -> str""
+ with Proof_global.NoCurrentProof -> Pp.str ""
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
@@ -152,22 +170,27 @@ 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, needed by the 8.4 semantics of Undo *)
- ceff : bool; (* is a side-effecting command *)
- cast : ast;
+ ctac : bool; (* is a tactic *)
+ ceff : bool; (* is a side-effecting command in the middle of a proof *)
+ 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
+ cblock : proof_block_name option;
+ 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
@@ -179,40 +202,69 @@ 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 }
+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;
Evd.evar_counter_summary_name;
"program-tcc-table" ]
-type state = {
- system : States.state;
- proof : Proof_global.state;
- shallow : bool
+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 = { (* 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 }
+
+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.
+ * 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
+and pt = { (* TODO: inline records in OCaml 4.03 *)
+ lemma : Stateid.t;
+ qed : Stateid.t;
+}
+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 *)
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 (* {{{ *)
@@ -228,7 +280,7 @@ end = struct (* {{{ *)
let find_proof_at_depth vcs pl =
try List.find (function
| _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl
- | _, { Vcs_.kind = `Edit _ } -> anomaly(str"find_proof_at_depth")
+ | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth")
| _ -> false)
(List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs))
with Not_found -> failwith "find_proof_at_depth"
@@ -236,9 +288,9 @@ end = struct (* {{{ *)
exception Expired
let visit vcs id =
if Stateid.equal id Stateid.initial then
- anomaly(str"Visiting the initial state id")
+ anomaly(Pp.str "Visiting the initial state id")
else if Stateid.equal id Stateid.dummy then
- anomaly(str"Visiting the dummy state id")
+ anomaly(Pp.str "Visiting the dummy state id")
else
try
match Vcs_.Dag.from_node (Vcs_.dag vcs) id with
@@ -254,7 +306,7 @@ end = struct (* {{{ *)
| [n, Sideff (Some x); p, Noop]
| [p, Noop; n, Sideff (Some x)]-> { step = `Sideff(`Ast (x,p)); next = n }
| [n, Sideff (Some x)]-> {step = `Sideff(`Ast (x,Stateid.dummy)); next=n}
- | _ -> anomaly (str ("Malformed VCS at node "^Stateid.to_string id))
+ | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id))
with Not_found -> raise Expired
end (* }}} *)
@@ -276,7 +328,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
@@ -290,30 +342,32 @@ 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
- val reachable : id -> Vcs_.NodeSet.t
+ val reachable : id -> Stateid.Set.t
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
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_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
val proof_nesting : unit -> int
val checkout_shallowest_proof_branch : unit -> unit
- val propagate_sideff : ast option -> unit
+ val propagate_sideff : replay:aast option -> unit
val gc : unit -> unit
@@ -329,7 +383,6 @@ end = struct (* {{{ *)
include Vcs_
exception Expired = Vcs_aux.Expired
- module StateidSet = Set.Make(Stateid)
open Printf
let print_dag vcs () =
@@ -337,21 +390,21 @@ end = struct (* {{{ *)
"stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in
let string_of_transaction = function
| Cmd { cast = t } | Fork (t, _,_,_) ->
- (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
+ (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR")
| Sideff (Some t) ->
sprintf "Sideff(%s)"
- (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
+ (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR")
| Sideff None -> "EnvChange"
| Noop -> " "
| Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id)
| 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 =
@@ -371,8 +424,6 @@ end = struct (* {{{ *)
let edge tr =
sprintf "<<FONT POINT-SIZE=\"12\" FACE=\"sans\">%s</FONT>>"
(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 -> ""
@@ -385,39 +436,71 @@ 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);
+ match Dag.Property.data b with
+ | 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"
+ 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 =
@@ -454,13 +537,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 ())
@@ -478,14 +560,14 @@ end = struct (* {{{ *)
let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with
| h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in
checkout branch;
- prerr_endline ("mode:" ^ mode);
+ prerr_endline (fun () -> "mode:" ^ mode);
Proof_global.activate_proof_mode mode
with Failure _ ->
checkout Branch.master;
- Proof_global.disactivate_proof_mode "Classic"
+ Proof_global.disactivate_current_proof_mode ()
(* copies the transaction on every open branch *)
- let propagate_sideff t =
+ let propagate_sideff ~replay:t =
List.iter (fun b ->
checkout b;
let id = new_node () in
@@ -510,9 +592,19 @@ 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 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
+ let props = CList.sort_uniquize Vcs_.Dag.Property.compare props in
+ 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 ->
@@ -520,28 +612,52 @@ 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) *)
- copy_info_w_state v start
+ let v = copy_info_w_state v start in
+ copy_proof_blockes v
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:lemma =
+ if not (topo_invariant l) then anomaly (str "overlapping boxes");
+ vcs := create_property !vcs l (ProofTask { qed; lemma })
+ 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 (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)
+ 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 }
@@ -598,7 +714,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
@@ -618,6 +737,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
@@ -663,51 +783,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
@@ -716,7 +845,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) =
@@ -738,12 +867,12 @@ end = struct (* {{{ *)
let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
f id
=
- feedback ~state_id:id Feedback.(ProcessingIn !Flags.async_proofs_worker_id);
+ feedback ~id:(State id) (ProcessingIn !Flags.async_proofs_worker_id);
let str_id = Stateid.to_string id in
if is_cached id && not redefine then
anomaly (str"defining state "++str str_id++str" twice");
try
- prerr_endline("defining "^str_id^" (cache="^
+ prerr_endline (fun () -> "defining "^str_id^" (cache="^
if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
let good_id = match safe_id with None -> !cur_id | Some id -> id in
fix_exn_ref := exn_on id ~valid:good_id;
@@ -751,24 +880,26 @@ end = struct (* {{{ *)
fix_exn_ref := (fun x -> x);
if cache = `Yes then freeze `No id
else if cache = `Shallow then freeze `Shallow id;
- prerr_endline ("setting cur id to "^str_id);
+ prerr_endline (fun () -> "setting cur id to "^str_id);
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 (* }}} *)
@@ -844,7 +975,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
@@ -943,6 +1074,75 @@ 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 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 is_block_name_enabled name &&
+ (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 ({ start; stop } as decl) ->
+ VCS.create_proof_block decl name
+ end
+ with Not_found ->
+ Errors.errorlabstrm "STM"
+ (str "Unknown proof block delimiter " ++ str name)
+
(****************************** THE SCHEDULER *********************************)
(******************************************************************************)
@@ -1060,7 +1260,7 @@ end = struct (* {{{ *)
List.iter (fun (id,s) -> State.assign id s) l; `End
| `Fresh, BuildProof { t_assign; t_loc; t_name; t_states; t_drop },
RespBuiltProof (pl, time) ->
- feedback (Feedback.InProgress ~-1);
+ feedback (InProgress ~-1);
t_assign (`Val pl);
record_pb_time t_name t_loc time;
if !Flags.async_proofs_full || t_drop
@@ -1068,7 +1268,7 @@ end = struct (* {{{ *)
else `End
| `Fresh, BuildProof { t_assign; t_loc; t_name; t_states },
RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } ->
- feedback (Feedback.InProgress ~-1);
+ feedback (InProgress ~-1);
let info = Stateid.add ~valid Exninfo.null e_error_at in
let e = (RemoteException e_msg, info) in
t_assign (`Exn e);
@@ -1084,7 +1284,7 @@ end = struct (* {{{ *)
let e = (RemoteException (strbrk s), info) in
t_assign (`Exn e);
Hooks.(call execution_error start Loc.ghost (strbrk s));
- feedback (Feedback.InProgress ~-1)
+ feedback (InProgress ~-1)
let build_proof_here ~drop_pt (id,valid) loc eop =
Future.create (State.exn_on id ~valid) (fun () ->
@@ -1095,7 +1295,7 @@ end = struct (* {{{ *)
Aux_file.record_in_aux_at loc "proof_build_time"
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
let p = Proof_global.return_proof ~allow_partial:drop_pt () in
- if drop_pt then Pp.feedback ~state_id:id Feedback.Complete;
+ if drop_pt then feedback ~id:(State id) Complete;
p)
let perform_buildp { Stateid.exn_info; stop; document; loc } drop my_states =
@@ -1119,7 +1319,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;
@@ -1133,9 +1333,9 @@ end = struct (* {{{ *)
| Some (safe, err) -> err, safe
| None -> Stateid.dummy, Stateid.dummy in
let e_msg = iprint (e, info) in
- prerr_endline "failed with the following exception:";
- prerr_endline (string_of_ppcmds e_msg);
- let e_safe_states = List.filter State.is_cached my_states 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_and_valid my_states in
RespError { e_error_at; e_safe_id; e_msg; e_safe_states }
let perform_states query =
@@ -1153,12 +1353,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
@@ -1188,7 +1388,7 @@ end = struct (* {{{ *)
"The system state could not be sent to the worker process. "^
"Falling back to local, lazy, evaluation."));
t_assign(`Comp(build_proof_here ~drop_pt t_exn_info t_loc t_stop));
- feedback (Feedback.InProgress ~-1)
+ feedback (InProgress ~-1)
end (* }}} *)
@@ -1260,7 +1460,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
@@ -1268,7 +1468,7 @@ end = struct (* {{{ *)
let (e, info) = Errors.push e in
(try match Stateid.get info with
| None ->
- pperrnl (
+ msg_error (
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
spc () ++ iprint (e, info))
| Some (_, cur) ->
@@ -1278,12 +1478,12 @@ end = struct (* {{{ *)
| { step = `Qed ( { qast = { loc } }, _) }
| { step = `Sideff (`Ast ( { loc }, _)) } ->
let start, stop = Loc.unloc loc in
- pperrnl (
+ msg_error (
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
str ": chars " ++ int start ++ str "-" ++ int stop ++
spc () ++ iprint (e, info))
| _ ->
- pperrnl (
+ msg_error (
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
spc () ++ iprint (e, info))
with e ->
@@ -1343,7 +1543,6 @@ end = struct (* {{{ *)
let set_perspective idl =
ProofTask.set_perspective idl;
TaskQueue.broadcast (Option.get !queue);
- let open Stateid in
let open ProofTask in
let overlap s1 s2 =
List.exists (fun x -> CList.mem_f Stateid.equal x s2) s1 in
@@ -1377,7 +1576,7 @@ end = struct (* {{{ *)
else
let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in
let t_uuid = Future.uuid f in
- feedback (Feedback.InProgress 1);
+ feedback (InProgress 1);
let task = ProofTask.(BuildProof {
t_exn_info; t_start = start; t_stop = stop; t_assign; t_drop = drop_pt;
t_loc = loc; t_uuid; t_name = pname;
@@ -1400,7 +1599,7 @@ end = struct (* {{{ *)
| Some (ReqBuildProof (r, b, _)) -> Some(r, b)
| _ -> None)
tasks in
- prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length reqs));
+ prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs));
reqs
let reset_task_queue () = TaskQueue.clear (Option.get !queue)
@@ -1414,7 +1613,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 }
@@ -1431,7 +1630,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 }
@@ -1440,7 +1639,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 }
@@ -1470,8 +1669,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 ((),[])
@@ -1499,7 +1697,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
@@ -1507,12 +1705,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)
@@ -1526,13 +1724,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
@@ -1549,7 +1749,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;
@@ -1568,7 +1768,7 @@ end = struct (* {{{ *)
with Not_found -> Errors.anomaly(str"Partac: wrong focus") in
if Future.is_over f then
let pt, uc = Future.join f in
- prerr_endline (string_of_ppcmds(hov 0 (
+ prerr_endline (fun () -> string_of_ppcmds(hov 0 (
str"g=" ++ str gid ++ spc () ++
str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
str"uc=" ++ Evd.pr_evar_universe_context uc)));
@@ -1583,16 +1783,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"
@@ -1624,11 +1824,11 @@ end = struct (* {{{ *)
Reach.known_state ~cache:`No r_where;
try
vernac_interp r_for { r_what with verbose = true };
- feedback ~state_id:r_for Feedback.Processed
+ feedback ~id:(State r_for) Processed
with e when Errors.noncritical e ->
let e = Errors.push e in
let msg = string_of_ppcmds (iprint e) in
- feedback ~state_id:r_for (Feedback.ErrorMsg (Loc.ghost, msg))
+ feedback ~id:(State r_for) (ErrorMsg (Loc.ghost, msg))
let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
let name_of_request { r_what } = string_of_ppcmds (pr_ast r_what)
@@ -1638,7 +1838,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 (* {{{ *)
@@ -1675,12 +1875,12 @@ let async_policy () =
(!compilation_mode = BuildVio || !async_proofs_mode <> APoff)
let delegate name =
- let time = get_hint_bp_time name in
- time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio
- || !Flags.async_proofs_full
+ get_hint_bp_time name >= !Flags.async_proofs_delegation_threshold
+ || !Flags.compilation_mode = Flags.BuildVio
+ || !Flags.async_proofs_full
let collect_proof keep cur hd brkind id =
- prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
+ prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
let no_name = "" in
let name = function
| [] -> no_name
@@ -1727,7 +1927,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
@@ -1763,7 +1963,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
@@ -1781,7 +1981,7 @@ let string_of_reason = function
| `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section"
| `Unknown -> "unsupported case"
-let log_string s = prerr_debug ("STM: " ^ s)
+let log_string s = prerr_debug (fun () -> "STM: " ^ s)
let log_processing_async id name = log_string Printf.(sprintf
"%s: proof %s: asynch" (Stateid.to_string id) name
)
@@ -1793,6 +1993,71 @@ 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 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
+ | ProofBlock ({ 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.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;
+ Proof_global.with_current_proof (fun _ p ->
+ 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;
+ 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 blockname f =
+ if !Flags.async_proofs_tac_error_resilience = `None ||
+ (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 blockname ie in
+ (* Absorb errors from f x *)
+ let resilient_command f x =
+ 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 *)
@@ -1803,17 +2068,17 @@ let known_state ?(redefine_qed=false) ~cache id =
Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env ()
in
let rec pure_cherry_pick_non_pstate id = Future.purify (fun id ->
- prerr_endline ("cherry-pick non pstate " ^ Stateid.to_string id);
+ prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
reach id;
cherry_pick_non_pstate ()) id
(* traverses the dag backward from nodes being already calculated *)
and reach ?(redefine_qed=false) ?(cache=cache) id =
- prerr_endline ("reaching: " ^ Stateid.to_string 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 ("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
@@ -1823,29 +2088,38 @@ 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 () ->
- 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)
+ | `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
+ 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; cblock } -> (fun () ->
+ resilient_tactic id cblock (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 ()), 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 () ->
+ | `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *)
reach ~cache:`Shallow prev;
reach view.next;
(try vernac_interp id x;
@@ -1862,7 +2136,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) ->
@@ -1896,7 +2170,7 @@ let known_state ?(redefine_qed=false) ~cache id =
if not delegate then ignore(Future.compute fp);
reach view.next;
vernac_interp id ~proof x;
- feedback ~state_id:id Feedback.Incomplete
+ feedback ~id:(State id) Incomplete
| { VCS.kind = `Master }, _ -> assert false
end;
Proof_global.discard_all ()
@@ -1951,7 +2225,7 @@ let known_state ?(redefine_qed=false) ~cache id =
else cache_step in
State.define
~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id;
- prerr_endline ("reached: "^ Stateid.to_string id) in
+ prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
reach ~redefine_qed id
end (* }}} *)
@@ -1966,7 +2240,7 @@ let init () =
Backtrack.record ();
Slaves.init ();
if Flags.async_proofs_is_master () then begin
- prerr_endline "Initializing workers";
+ prerr_endline (fun () -> "Initializing workers");
Query.init ();
let opts = match !Flags.async_proofs_private_flags with
| None -> []
@@ -2018,9 +2292,9 @@ let rec join_admitted_proofs id =
let join () =
finish ();
wait ();
- prerr_endline "Joining the environment";
+ prerr_endline (fun () -> "Joining the environment");
Global.join_safe_environment ();
- prerr_endline "Joining Admitted proofs";
+ prerr_endline (fun () -> "Joining Admitted proofs");
join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ()));
VCS.print ();
VCS.print ()
@@ -2033,7 +2307,6 @@ let check_task name (tasks,rcbackup) i =
let vcs = VCS.backup () in
try
let rc = Future.purify (Slaves.check_task name tasks) i in
- pperr_flush ();
VCS.restore vcs;
rc
with e when Errors.noncritical e -> VCS.restore vcs; false
@@ -2043,7 +2316,6 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
let finish_task u (_,_,i) =
let vcs = VCS.backup () in
let u = Future.purify (Slaves.finish_task name u d p t) i in
- pperr_flush ();
VCS.restore vcs;
u in
try
@@ -2051,7 +2323,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
(u,a,true), p
with e ->
let e = Errors.push e in
- pperrnl (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
+ msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
exit 1
let merge_proof_branch ?valid ?id qast keep brname =
@@ -2096,7 +2368,7 @@ let handle_failure (e, info) vcs tty =
anomaly(str"error with no safe_id attached:" ++ spc() ++
Errors.iprint_no_report (e, info))
| Some (safe_id, id) ->
- prerr_endline ("Failed at state " ^ Stateid.to_string id);
+ prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
VCS.restore vcs;
if tty && interactive () = `Yes then begin
(* We stay on a valid state *)
@@ -2107,27 +2379,29 @@ let handle_failure (e, info) vcs tty =
VCS.print ();
iraise (e, info)
-let snapshot_vio ldir long_f_dot_v =
+let snapshot_vio ldir long_f_dot_vo =
finish ();
if List.length (VCS.branches ()) > 1 then
Errors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs");
- Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_v
+ Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo
(Global.opaque_tables ())
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 ("{{{ processing: "^ string_of_ppcmds (pr_ast x));
+ prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x));
let vcs = VCS.backup () in
try
let head = VCS.current_branch () in
VCS.checkout head;
let rc = begin
- prerr_endline (" classified as: " ^ string_of_vernac_classification c);
+ prerr_endline (fun () ->
+ " classified as: " ^ string_of_vernac_classification c);
match c with
(* PG stuff *)
| VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok
@@ -2163,7 +2437,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
VCS.commit id (Alias (oid,x));
Backtrack.record (); if w == VtNow then finish (); `Ok
| VtStm (VtBack id, false), VtNow ->
- prerr_endline ("undo to state " ^ Stateid.to_string id);
+ prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
Backtrack.backto id;
VCS.checkout_shallowest_proof_branch ();
Reach.known_state ~cache:(interactive ()) id; `Ok
@@ -2174,7 +2448,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
@@ -2193,7 +2467,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
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")
@@ -2216,7 +2490,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
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 } -> ()
@@ -2231,10 +2505,14 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
Backtrack.record ();
finish ();
`Ok
- | VtProofStep paral, w ->
+ | VtProofStep { parallel; proof_block_detection = cblock }, w ->
let id = VCS.new_node ~id:newtip () in
- let queue = if paral then `TacQueue (ref false) else `MainQueue in
- VCS.commit id (Cmd {ctac = true;ceff = false;cast = x;cids = [];cqueue = queue });
+ let queue = if parallel then `TacQueue (ref false) else `MainQueue in
+ 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
@@ -2248,15 +2526,22 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
vernac_interp (VCS.get_branch_pos head) x; `Ok
| VtSideff l, w ->
+ 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=true;cast=x;cids=l;cqueue=`MainQueue});
- VCS.propagate_sideff (Some x);
+ 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
+ | VernacDefinition(_, _, DefineBody _) -> None
+ | _ -> Some x in
+ VCS.propagate_sideff ~replay;
VCS.checkout_shallowest_proof_branch ();
Backtrack.record (); if w == VtNow then finish (); `Ok
(* Unknown: we execute it, check for open goals and propagate sideeff *)
| VtUnknown, VtNow ->
+ let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
let id = VCS.new_node ~id:newtip () in
let head_id = VCS.get_branch_pos head in
Reach.known_state ~cache:`Yes head_id; (* ensure it is ok *)
@@ -2266,21 +2551,22 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
Reach.known_state ~cache:(interactive ()) mid;
vernac_interp id x;
(* Vernac x may or may not start a proof *)
- if VCS.Branch.equal head VCS.Branch.master &&
- Proof_global.there_are_pending_proofs ()
- then begin
+ if not in_proof && Proof_global.there_are_pending_proofs () then
+ begin
let bname = VCS.mk_branch_name x in
let opacity_of_produced_term =
match x.expr with
+ (* This AST is ambiguous, hence we check it dynamically *)
| VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity
| _ -> Doesn'tGuaranteeOpacity in
VCS.commit id (Fork (x,bname,opacity_of_produced_term,[]));
- VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1));
- Proof_global.activate_proof_mode "Classic";
+ let proof_mode = default_proof_mode () in
+ 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 = true;
- cast = x; cids = []; cqueue = `MainQueue});
- VCS.propagate_sideff (Some x);
+ 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 ();
end in
State.define ~safe_id:head_id ~cache:`Yes step id;
@@ -2290,49 +2576,55 @@ 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;
- prerr_endline "processed }}}";
+ prerr_endline (fun () -> "processed }}}");
VCS.print ();
rc
with e ->
let e = Errors.push e in
handle_failure e vcs tty
-let print_ast id =
- try
- match VCS.visit id with
- | { step = `Cmd { cast = { loc; expr } } }
- | { step = `Fork (({ loc; expr }, _, _, _), _) }
- | { step = `Qed ({ qast = { loc; expr } }, _) } ->
- let xml =
- try Texmacspp.tmpp expr loc
- with e -> Xml_datatype.PCData ("ERROR " ^ Printexc.to_string e) in
- xml;
- | _ -> Xml_datatype.PCData "ERROR"
- with _ -> Xml_datatype.PCData "ERROR"
+let get_ast id =
+ match VCS.visit id with
+ | { step = `Cmd { cast = { loc; expr } } }
+ | { step = `Fork (({ loc; expr }, _, _, _), _) }
+ | { step = `Qed ({ qast = { loc; expr } }, _) } ->
+ Some (expr, loc)
+ | _ -> None
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
@@ -2342,20 +2634,20 @@ type focus = {
tip : Stateid.t
}
-let query ~at ?(report_with=(Stateid.dummy,Feedback.default_route)) s =
+let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
Future.purify (fun 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 =
@@ -2380,7 +2672,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
@@ -2395,13 +2687,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_boxes_of id;
cancel_switch := true;
Reach.known_state ~cache:(interactive ()) id;
VCS.checkout_shallowest_proof_branch ();
@@ -2415,14 +2707,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_boxes_of id;
VCS.gc ();
VCS.print ();
if not !Flags.async_proofs_full then
@@ -2437,14 +2729,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 ; 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
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
@@ -2476,7 +2768,7 @@ let edit_at id =
anomaly (str ("edit_at "^Stateid.to_string id^": ") ++
Errors.print_no_report e)
| Some (_, id) ->
- prerr_endline ("Failed at state " ^ Stateid.to_string id);
+ prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
VCS.restore vcs;
VCS.print ();
iraise (e, info)
@@ -2487,9 +2779,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 &&
diff --git a/stm/stm.mli b/stm/stm.mli
index 4279921b3b..37ec1f0a13 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 ]
@@ -76,7 +78,9 @@ val get_current_state : unit -> Stateid.t
(* Misc *)
val init : unit -> unit
-val print_ast : Stateid.t -> Xml_datatype.xml
+
+(* This returns the node at that position *)
+val get_ast : Stateid.t -> (Vernacexpr.vernac_expr * Loc.t) option
(* Filename *)
val set_compilation_hints : string -> unit
@@ -94,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 = 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
+*)
+
+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
@@ -120,12 +200,13 @@ 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 ****************************** **)
(* Adds a new line to the document. It replaces the core of Vernac.interp.
- [finish] is called as the last bit of this function is the system
+ [finish] is called as the last bit of this function if the system
is running interactively (-emacs or coqtop). *)
val interp : bool -> vernac_expr located -> unit
@@ -135,7 +216,7 @@ val get_all_proof_names : unit -> Id.t list
val get_current_proof_name : unit -> Id.t option
val show_script : ?proof:Proof_global.closed_proof -> unit -> unit
-(** Reverse dependency hooks *)
+(* Hooks to be set by other Coq components in order to break file cycles *)
val process_error_hook : Future.fix_exn Hook.t
val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof ->
Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 92b3a869a9..939ee187ae 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -7,6 +7,6 @@ Vernac_classifier
Lemmas
CoqworkmgrApi
AsyncTaskQueue
-Texmacspp
Stm
+ProofBlockDelimiter
Vio_checking
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
deleted file mode 100644
index d1d6de9ae8..0000000000
--- a/stm/texmacspp.ml
+++ /dev/null
@@ -1,762 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Xml_datatype
-open Vernacexpr
-open Constrexpr
-open Names
-open Misctypes
-open Bigint
-open Decl_kinds
-open Extend
-open Libnames
-
-let unlock loc =
- let start, stop = Loc.unloc loc in
- (string_of_int start, string_of_int stop)
-
-let xmlWithLoc loc ename attr xml =
- let start, stop = unlock loc in
- Element(ename, [ "begin", start; "end", stop ] @ attr, xml)
-
-let get_fst_attr_in_xml_list attr xml_list =
- let attrs_list =
- List.map (function
- | Element (_, attrs, _) -> (List.filter (fun (a,_) -> a = attr) attrs)
- | _ -> [])
- xml_list in
- match List.flatten attrs_list with
- | [] -> (attr, "")
- | l -> (List.hd l)
-
-let backstep_loc xmllist =
- let start_att = get_fst_attr_in_xml_list "begin" xmllist in
- let stop_att = get_fst_attr_in_xml_list "end" (List.rev xmllist) in
- [start_att ; stop_att]
-
-let compare_begin_att xml1 xml2 =
- let att1 = get_fst_attr_in_xml_list "begin" [xml1] in
- let att2 = get_fst_attr_in_xml_list "begin" [xml2] in
- match att1, att2 with
- | (_, s1), (_, s2) when s1 == "" || s2 == "" -> 0
- | (_, s1), (_, s2) when int_of_string s1 > int_of_string s2 -> 1
- | (_, s1), (_, s2) when int_of_string s1 < int_of_string s2 -> -1
- | _ -> 0
-
-let xmlBeginSection loc name = xmlWithLoc loc "beginsection" ["name", name] []
-
-let xmlEndSegment loc name = xmlWithLoc loc "endsegment" ["name", name] []
-
-let xmlThm typ name loc xml =
- xmlWithLoc loc "theorem" ["type", typ; "name", name] xml
-
-let xmlDef typ name loc xml =
- xmlWithLoc loc "definition" ["type", typ; "name", name] xml
-
-let xmlNotation attr name loc xml =
- xmlWithLoc loc "notation" (("name", name) :: attr) xml
-
-let xmlReservedNotation attr name loc =
- xmlWithLoc loc "reservednotation" (("name", name) :: attr) []
-
-let xmlCst name ?(attr=[]) loc =
- xmlWithLoc loc "constant" (("name", name) :: attr) []
-
-let xmlOperator name ?(attr=[]) ?(pprules=[]) loc =
- xmlWithLoc loc "operator"
- (("name", name) :: List.map (fun (a,b) -> "format"^a,b) pprules @ attr) []
-
-let xmlApply loc ?(attr=[]) xml = xmlWithLoc loc "apply" attr xml
-
-let xmlToken loc ?(attr=[]) xml = xmlWithLoc loc "token" attr xml
-
-let xmlTyped xml = Element("typed", (backstep_loc xml), xml)
-
-let xmlReturn ?(attr=[]) xml = Element("return", attr, xml)
-
-let xmlCase xml = Element("case", [], xml)
-
-let xmlScrutinee ?(attr=[]) xml = Element("scrutinee", attr, xml)
-
-let xmlWith xml = Element("with", [], xml)
-
-let xmlAssign id xml = Element("assign", ["target",string_of_id id], [xml])
-
-let xmlInductive kind loc xml = xmlWithLoc loc "inductive" ["kind",kind] xml
-
-let xmlCoFixpoint xml = Element("cofixpoint", [], xml)
-
-let xmlFixpoint xml = Element("fixpoint", [], xml)
-
-let xmlCheck loc xml = xmlWithLoc loc "check" [] xml
-
-let xmlAssumption kind loc xml = xmlWithLoc loc "assumption" ["kind",kind] xml
-
-let xmlComment loc xml = xmlWithLoc loc "comment" [] xml
-
-let xmlCanonicalStructure attr loc = xmlWithLoc loc "canonicalstructure" attr []
-
-let xmlQed ?(attr=[]) loc = xmlWithLoc loc "qed" attr []
-
-let xmlPatvar id loc = xmlWithLoc loc "patvar" ["id", id] []
-
-let xmlReference ref =
- let name = Libnames.string_of_reference ref in
- let i, j = Loc.unloc (Libnames.loc_of_reference ref) in
- let b, e = string_of_int i, string_of_int j in
- Element("reference",["name", name; "begin", b; "end", e] ,[])
-
-let xmlRequire loc ?(attr=[]) xml = xmlWithLoc loc "require" attr xml
-let xmlImport loc ?(attr=[]) xml = xmlWithLoc loc "import" attr xml
-
-let xmlAddLoadPath loc ?(attr=[]) xml = xmlWithLoc loc "addloadpath" attr xml
-let xmlRemoveLoadPath loc ?(attr=[]) = xmlWithLoc loc "removeloadpath" attr
-let xmlAddMLPath loc ?(attr=[]) = xmlWithLoc loc "addmlpath" attr
-
-let xmlExtend loc xml = xmlWithLoc loc "extend" [] xml
-
-let xmlScope loc action ?(attr=[]) name xml =
- xmlWithLoc loc "scope" (["name",name;"action",action] @ attr) xml
-
-let xmlProofMode loc name = xmlWithLoc loc "proofmode" ["name",name] []
-
-let xmlProof loc xml = xmlWithLoc loc "proof" [] xml
-
-let xmlRawTactic name rtac =
- Element("rawtactic", ["name",name],
- [PCData (Pp.string_of_ppcmds (Pptactic.pr_raw_tactic rtac))])
-
-let xmlSectionSubsetDescr name ssd =
- Element("sectionsubsetdescr",["name",name],
- [PCData (Proof_using.to_string ssd)])
-
-let xmlDeclareMLModule loc s =
- xmlWithLoc loc "declarexmlmodule" []
- (List.map (fun x -> Element("path",["value",x],[])) s)
-
-(* tactics *)
-let xmlLtac loc xml = xmlWithLoc loc "ltac" [] xml
-
-(* toplevel commands *)
-let xmlGallina loc xml = xmlWithLoc loc "gallina" [] xml
-
-let xmlTODO loc x =
- xmlWithLoc loc "todo" [] [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
-let string_of_name n =
- match n with
- | Anonymous -> "_"
- | Name id -> Id.to_string id
-
-let string_of_glob_sort s =
- match s with
- | GProp -> "Prop"
- | GSet -> "Set"
- | GType _ -> "Type"
-
-let string_of_cast_sort c =
- match c with
- | CastConv _ -> "CastConv"
- | CastVM _ -> "CastVM"
- | CastNative _ -> "CastNative"
- | CastCoerce -> "CastCoerce"
-
-let string_of_case_style s =
- match s with
- | LetStyle -> "Let"
- | IfStyle -> "If"
- | LetPatternStyle -> "LetPattern"
- | MatchStyle -> "Match"
- | RegularStyle -> "Regular"
-
-let attribute_of_syntax_modifier sm =
-match sm with
- | SetItemLevel (sl, NumLevel n) ->
- List.map (fun s -> ("itemlevel", s)) sl @ ["level", string_of_int n]
- | SetItemLevel (sl, NextLevel) ->
- List.map (fun s -> ("itemlevel", s)) sl @ ["level", "next"]
- | SetLevel i -> ["level", string_of_int i]
- | SetAssoc a ->
- begin match a with
- | NonA -> ["",""]
- | RightA -> ["associativity", "right"]
- | LeftA -> ["associativity", "left"]
- end
- | SetEntryType (s, _) -> ["entrytype", s]
- | SetOnlyParsing v -> ["compat", Flags.pr_version v]
- | SetFormat (system, (loc, s)) ->
- let start, stop = unlock loc in
- ["format-"^system, s; "begin", start; "end", stop]
-
-let string_of_assumption_kind l a many =
- match l, a, many with
- | (Discharge, Logical, true) -> "Hypotheses"
- | (Discharge, Logical, false) -> "Hypothesis"
- | (Discharge, Definitional, true) -> "Variables"
- | (Discharge, Definitional, false) -> "Variable"
- | (Global, Logical, true) -> "Axioms"
- | (Global, Logical, false) -> "Axiom"
- | (Global, Definitional, true) -> "Parameters"
- | (Global, Definitional, false) -> "Parameter"
- | (Local, Logical, true) -> "Local Axioms"
- | (Local, Logical, false) -> "Local Axiom"
- | (Local, Definitional, true) -> "Local Parameters"
- | (Local, Definitional, false) -> "Local Parameter"
- | (Global, Conjectural, _) -> "Conjecture"
- | ((Discharge | Local), Conjectural, _) -> assert false
-
-let rec pp_bindlist bl =
- let tlist =
- List.flatten
- (List.map
- (fun (loc_names, _, e) ->
- let names =
- (List.map
- (fun (loc, name) ->
- xmlCst (string_of_name name) loc) loc_names) in
- match e with
- | CHole _ -> names
- | _ -> names @ [pp_expr e])
- bl) in
- match tlist with
- | [e] -> e
- | l -> xmlTyped l
-and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *)
- Element ("decl_notation", ["name", s], [pp_expr ce])
-and pp_local_binder lb = (* don't know what it is for now *)
- match lb with
- | LocalRawDef ((_, nam), ce) ->
- let attrs = ["name", string_of_name nam] in
- pp_expr ~attr:attrs ce
- | LocalRawAssum (namll, _, ce) ->
- let ppl =
- List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in
- xmlTyped (ppl @ [pp_expr ce])
-and pp_local_decl_expr lde = (* don't know what it is for now *)
- match lde with
- | AssumExpr (_, ce) -> pp_expr ce
- | DefExpr (_, ce, _) -> pp_expr ce
-and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) =
- (* inductive_expr *)
- let b,e = Loc.unloc l in
- let location = ["begin", string_of_int b; "end", string_of_int e] in
- [Element ("lident", ["name", Id.to_string id] @ location, [])] @ (* inductive name *)
- begin match cl_or_rdexpr with
- | Constructors coel -> List.map (fun (_, (_, ce)) -> pp_expr ce) coel
- | RecordDecl (_, ldewwwl) ->
- List.map (fun (((_, x), _), _) -> pp_local_decl_expr x) ldewwwl
- end @
- begin match ceo with (* don't know what it is for now *)
- | Some ce -> [pp_expr ce]
- | None -> []
- end @
- (List.map pp_local_binder lbl)
-and pp_recursion_order_expr optid roe = (* don't know what it is for now *)
- let attrs =
- match optid with
- | None -> []
- | Some (loc, id) ->
- let start, stop = unlock loc in
- ["begin", start; "end", stop ; "name", Id.to_string id] in
- let kind, expr =
- match roe with
- | CStructRec -> "struct", []
- | CWfRec e -> "rec", [pp_expr e]
- | CMeasureRec (e, None) -> "mesrec", [pp_expr e]
- | CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in
- Element ("recursion_order", ["kind", kind] @ attrs, expr)
-and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) =
- (* fixpoint_expr *)
- let start, stop = unlock loc in
- let id = Id.to_string id in
- [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
- (* fixpoint name *)
- [pp_recursion_order_expr optid roe] @
- (List.map pp_local_binder lbl) @
- [pp_expr ce] @
- begin match ceo with (* don't know what it is for now *)
- | Some ce -> [pp_expr ce]
- | None -> []
- end
-and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
- (* Nota: it is like fixpoint_expr without (optid, roe)
- * so could be merged if there is no more differences *)
- let start, stop = unlock loc in
- let id = Id.to_string id in
- [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
- (* cofixpoint name *)
- (List.map pp_local_binder lbl) @
- [pp_expr ce] @
- begin match ceo with (* don't know what it is for now *)
- | Some ce -> [pp_expr ce]
- | None -> []
- end
-and pp_lident (loc, id) = xmlCst (Id.to_string id) loc
-and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce]
-and pp_cases_pattern_expr cpe =
- match cpe with
- | CPatAlias (loc, cpe, id) ->
- xmlApply loc
- (xmlOperator "alias" ~attr:["name", string_of_id id] loc ::
- [pp_cases_pattern_expr cpe])
- | CPatCstr (loc, ref, None, cpel2) ->
- xmlApply loc
- (xmlOperator "reference"
- ~attr:["name", Libnames.string_of_reference ref] loc ::
- [Element ("impargs", [], []);
- Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
- | CPatCstr (loc, ref, Some cpel1, cpel2) ->
- xmlApply loc
- (xmlOperator "reference"
- ~attr:["name", Libnames.string_of_reference ref] loc ::
- [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1));
- Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
- | CPatAtom (loc, optr) ->
- let attrs = match optr with
- | None -> []
- | Some r -> ["name", Libnames.string_of_reference r] in
- xmlApply loc (xmlOperator "atom" ~attr:attrs loc :: [])
- | CPatOr (loc, cpel) ->
- xmlApply loc (xmlOperator "or" loc :: List.map pp_cases_pattern_expr cpel)
- | CPatNotation (loc, n, (subst_constr, subst_rec), cpel) ->
- xmlApply loc
- (xmlOperator "notation" loc ::
- [xmlOperator n loc;
- Element ("subst", [],
- [Element ("subterms", [],
- List.map pp_cases_pattern_expr subst_constr);
- Element ("recsubterms", [],
- List.map
- (fun (cpel) ->
- Element ("recsubterm", [],
- List.map pp_cases_pattern_expr cpel))
- subst_rec)]);
- Element ("args", [], (List.map pp_cases_pattern_expr cpel))])
- | CPatPrim (loc, tok) -> pp_token loc tok
- | CPatRecord (loc, rcl) ->
- xmlApply loc
- (xmlOperator "record" loc ::
- List.map (fun (r, cpe) ->
- Element ("field",
- ["reference", Libnames.string_of_reference r],
- [pp_cases_pattern_expr cpe]))
- rcl)
- | CPatDelimiters (loc, delim, cpe) ->
- xmlApply loc
- (xmlOperator "delimiter" ~attr:["name", delim] loc ::
- [pp_cases_pattern_expr cpe])
-and pp_case_expr (e, name, pat) =
- match name, pat with
- | None, None -> xmlScrutinee [pp_expr e]
- | Some (loc, name), None ->
- let start, stop= unlock loc in
- xmlScrutinee ~attr:["name", string_of_name name;
- "begin", start; "end", stop] [pp_expr e]
- | Some (loc, name), Some p ->
- let start, stop= unlock loc in
- xmlScrutinee ~attr:["name", string_of_name name;
- "begin", start; "end", stop]
- [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
- | None, Some p ->
- xmlScrutinee [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
-and pp_branch_expr_list bel =
- xmlWith
- (List.map
- (fun (_, cpel, e) ->
- let ppcepl =
- List.map pp_cases_pattern_expr (List.flatten (List.map snd cpel)) in
- let ppe = [pp_expr e] in
- xmlCase (ppcepl @ ppe))
- bel)
-and pp_token loc tok =
- let tokstr =
- match tok with
- | String s -> PCData s
- | Numeral n -> PCData (to_string n) in
- xmlToken loc [tokstr]
-and pp_local_binder_list lbl =
- let l = (List.map pp_local_binder lbl) in
- Element ("recurse", (backstep_loc l), l)
-and pp_const_expr_list cel =
- let l = List.map pp_expr cel in
- Element ("recurse", (backstep_loc l), l)
-and pp_expr ?(attr=[]) e =
- match e with
- | CRef (r, _) ->
- xmlCst ~attr
- (Libnames.string_of_reference r) (Libnames.loc_of_reference r)
- | CProdN (loc, bl, e) ->
- xmlApply loc
- (xmlOperator "forall" loc :: [pp_bindlist bl] @ [pp_expr e])
- | CApp (loc, (_, hd), args) ->
- xmlApply ~attr loc (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args)
- | CAppExpl (loc, (_, r, _), args) ->
- xmlApply ~attr loc
- (xmlCst (Libnames.string_of_reference r)
- (Libnames.loc_of_reference r) :: List.map pp_expr args)
- | CNotation (loc, notation, ([],[],[])) ->
- xmlOperator notation loc
- | CNotation (loc, notation, (args, cell, lbll)) ->
- let fmts = Notation.find_notation_extra_printing_rules notation in
- let oper = xmlOperator notation loc ~pprules:fmts in
- let cels = List.map pp_const_expr_list cell in
- let lbls = List.map pp_local_binder_list lbll in
- let args = List.map pp_expr args in
- xmlApply loc (oper :: (List.sort compare_begin_att (args @ cels @ lbls)))
- | CSort(loc, s) ->
- xmlOperator (string_of_glob_sort s) loc
- | CDelimiters (loc, scope, ce) ->
- xmlApply loc (xmlOperator "delimiter" ~attr:["name", scope] loc ::
- [pp_expr ce])
- | CPrim (loc, tok) -> pp_token loc tok
- | CGeneralization (loc, kind, _, e) ->
- let kind= match kind with
- | Explicit -> "explicit"
- | Implicit -> "implicit" in
- xmlApply loc
- (xmlOperator "generalization" ~attr:["kind", kind] loc :: [pp_expr e])
- | CCast (loc, e, tc) ->
- begin match tc with
- | CastConv t | CastVM t |CastNative t ->
- xmlApply loc
- (xmlOperator ":" loc ~attr:["kind", (string_of_cast_sort tc)] ::
- [pp_expr e; pp_expr t])
- | CastCoerce ->
- xmlApply loc
- (xmlOperator ":" loc ~attr:["kind", "CastCoerce"] ::
- [pp_expr e])
- end
- | CEvar (loc, ek, cel) ->
- let ppcel = List.map (fun (id,e) -> xmlAssign id (pp_expr e)) cel in
- xmlApply loc
- (xmlOperator "evar" loc ~attr:["id", string_of_id ek] ::
- ppcel)
- | CPatVar (loc, id) -> xmlPatvar (string_of_id id) loc
- | CHole (loc, _, _, _) -> xmlCst ~attr "_" loc
- | CIf (loc, test, (_, ret), th, el) ->
- let return = match ret with
- | None -> []
- | Some r -> [xmlReturn [pp_expr r]] in
- xmlApply loc
- (xmlOperator "if" loc ::
- return @ [pp_expr th] @ [pp_expr el])
- | CLetTuple (loc, names, (_, ret), value, body) ->
- let return = match ret with
- | None -> []
- | Some r -> [xmlReturn [pp_expr r]] in
- xmlApply loc
- (xmlOperator "lettuple" loc ::
- return @
- (List.map (fun (loc, var) -> xmlCst (string_of_name var) loc) names) @
- [pp_expr value; pp_expr body])
- | CCases (loc, sty, ret, cel, bel) ->
- let return = match ret with
- | None -> []
- | Some r -> [xmlReturn [pp_expr r]] in
- xmlApply loc
- (xmlOperator "match" loc ~attr:["style", (string_of_case_style sty)] ::
- (return @
- [Element ("scrutinees", [], List.map pp_case_expr cel)] @
- [pp_branch_expr_list bel]))
- | CRecord (_, _) -> assert false
- | CLetIn (loc, (varloc, var), value, body) ->
- xmlApply loc
- (xmlOperator "let" loc ::
- [xmlCst (string_of_name var) varloc; pp_expr value; pp_expr body])
- | CLambdaN (loc, bl, e) ->
- xmlApply loc
- (xmlOperator "lambda" loc :: [pp_bindlist bl] @ [pp_expr e])
- | CCoFix (_, _, _) -> assert false
- | CFix (loc, lid, fel) ->
- xmlApply loc
- (xmlOperator "fix" loc ::
- List.flatten (List.map
- (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d))
- fel))
-
-let pp_comment (c) =
- match c with
- | CommentConstr e -> [pp_expr e]
- | CommentString s -> [Element ("string", [], [PCData s])]
- | CommentInt i -> [PCData (string_of_int i)]
-
-let rec tmpp v loc =
- match v with
- (* Control *)
- | VernacLoad (verbose,f) ->
- xmlWithLoc loc "load" ["verbose",string_of_bool verbose;"file",f] []
- | VernacTime (loc,e) ->
- xmlApply loc (Element("time",[],[]) ::
- [tmpp e loc])
- | VernacRedirect (s, (loc,e)) ->
- xmlApply loc (Element("redirect",["path", s],[]) ::
- [tmpp e loc])
- | VernacTimeout (s,e) ->
- xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
- [tmpp e loc])
- | VernacFail e -> xmlApply loc (Element("fail",[],[]) :: [tmpp e loc])
- | VernacError _ -> xmlWithLoc loc "error" [] []
-
- (* Syntax *)
- | VernacSyntaxExtension (_, ((_, name), sml)) ->
- let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
- xmlReservedNotation attrs name loc
-
- | VernacOpenCloseScope (_,(true,name)) -> xmlScope loc "open" name []
- | VernacOpenCloseScope (_,(false,name)) -> xmlScope loc "close" name []
- | VernacDelimiters (name,Some tag) ->
- xmlScope loc "delimit" name ~attr:["delimiter",tag] []
- | VernacDelimiters (name,None) ->
- xmlScope loc "undelimit" name ~attr:[] []
- | VernacInfix (_,((_,name),sml),ce,sn) ->
- let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
- let sc_attr =
- match sn with
- | Some scope -> ["scope", scope]
- | None -> [] in
- xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
- | VernacNotation (_, ce, (lstr, sml), sn) ->
- let name = snd lstr in
- let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
- let sc_attr =
- match sn with
- | Some scope -> ["scope", scope]
- | None -> [] in
- xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
- | VernacBindScope _ as x -> xmlTODO loc x
- | VernacNotationAddFormat _ as x -> xmlTODO loc x
- | VernacUniverse _
- | VernacConstraint _
- | VernacPolymorphic (_, _) as x -> xmlTODO loc x
- (* Gallina *)
- | VernacDefinition (ldk, ((_,id),_), de) ->
- let l, dk =
- match ldk with
- | Some l, dk -> (l, dk)
- | None, dk -> (Global, dk) in (* Like in ppvernac.ml, l 585 *)
- let e =
- match de with
- | ProveBody (_, ce) -> ce
- | DefineBody (_, Some _, ce, None) -> ce
- | DefineBody (_, None , ce, None) -> ce
- | DefineBody (_, Some _, ce, Some _) -> ce
- | DefineBody (_, None , ce, Some _) -> ce in
- let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
- let str_id = Id.to_string id in
- (xmlDef str_dk str_id loc [pp_expr e])
- | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) ->
- let str_tk = Kindops.string_of_theorem_kind tk in
- let str_id = Id.to_string id in
- (xmlThm str_tk str_id loc [pp_expr statement])
- | VernacStartTheoremProof _ as x -> xmlTODO loc x
- | VernacEndProof pe ->
- begin
- match pe with
- | Admitted -> xmlQed loc
- | Proved (_, Some ((_, id), Some tk)) ->
- let nam = Id.to_string id in
- let typ = Kindops.string_of_theorem_kind tk in
- xmlQed ~attr:["name", nam; "type", typ] loc
- | Proved (_, Some ((_, id), None)) ->
- let nam = Id.to_string id in
- xmlQed ~attr:["name", nam] loc
- | Proved _ -> xmlQed loc
- end
- | VernacExactProof _ as x -> xmlTODO loc x
- | VernacAssumption ((l, a), _, sbwcl) ->
- let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in
- let many =
- List.length (List.flatten (List.map fst binders)) > 1 in
- let exprs =
- List.flatten (List.map pp_simple_binder binders) in
- let l = match l with Some x -> x | None -> Decl_kinds.Global in
- let kind = string_of_assumption_kind l a many in
- xmlAssumption kind loc exprs
- | VernacInductive (_, _, iednll) ->
- let kind =
- let (_, _, _, k, _),_ = List.hd iednll in
- begin
- match k with
- | Record -> "Record"
- | Structure -> "Structure"
- | Inductive_kw -> "Inductive"
- | CoInductive -> "CoInductive"
- | Class _ -> "Class"
- | Variant -> "Variant"
- end in
- let exprs =
- List.flatten (* should probably not be flattened *)
- (List.map
- (fun (ie, dnl) -> (pp_inductive_expr ie) @
- (List.map pp_decl_notation dnl)) iednll) in
- xmlInductive kind loc exprs
- | VernacFixpoint (_, fednll) ->
- let exprs =
- List.flatten (* should probably not be flattened *)
- (List.map
- (fun (fe, dnl) -> (pp_fixpoint_expr fe) @
- (List.map pp_decl_notation dnl)) fednll) in
- xmlFixpoint exprs
- | VernacCoFixpoint (_, cfednll) ->
- (* Nota: it is like VernacFixpoint without so could be merged *)
- let exprs =
- List.flatten (* should probably not be flattened *)
- (List.map
- (fun (cfe, dnl) -> (pp_cofixpoint_expr cfe) @
- (List.map pp_decl_notation dnl)) cfednll) in
- xmlCoFixpoint exprs
- | VernacScheme _ as x -> xmlTODO loc x
- | VernacCombinedScheme _ as x -> xmlTODO loc x
-
- (* Gallina extensions *)
- | VernacBeginSection (_, id) -> xmlBeginSection loc (Id.to_string id)
- | VernacEndSegment (_, id) -> xmlEndSegment loc (Id.to_string id)
- | VernacNameSectionHypSet _ as x -> xmlTODO loc x
- | VernacRequire (from, import, l) ->
- let import = match import with
- | None -> []
- | Some true -> ["export","true"]
- | Some false -> ["import","true"]
- in
- let from = match from with
- | None -> []
- | Some r -> ["from", Libnames.string_of_reference r]
- in
- xmlRequire loc ~attr:(from @ import) (List.map (fun ref ->
- xmlReference ref) l)
- | VernacImport (true,l) ->
- xmlImport loc ~attr:["export","true"] (List.map (fun ref ->
- xmlReference ref) l)
- | VernacImport (false,l) ->
- xmlImport loc (List.map (fun ref ->
- xmlReference ref) l)
- | VernacCanonical r ->
- let attr =
- match r with
- | AN (Qualid (_, q)) -> ["qualid", string_of_qualid q]
- | AN (Ident (_, id)) -> ["id", Id.to_string id]
- | ByNotation (_, s, _) -> ["notation", s] in
- xmlCanonicalStructure attr loc
- | VernacCoercion _ as x -> xmlTODO loc x
- | VernacIdentityCoercion _ as x -> xmlTODO loc x
-
- (* Type classes *)
- | VernacInstance _ as x -> xmlTODO loc x
-
- | VernacContext _ as x -> xmlTODO loc x
-
- | VernacDeclareInstances _ as x -> xmlTODO loc x
-
- | VernacDeclareClass _ as x -> xmlTODO loc x
-
- (* Modules and Module Types *)
- | VernacDeclareModule _ as x -> xmlTODO loc x
- | VernacDefineModule _ as x -> xmlTODO loc x
- | VernacDeclareModuleType _ as x -> xmlTODO loc x
- | VernacInclude _ as x -> xmlTODO loc x
-
- (* Solving *)
-
- | (VernacSolveExistential _) as x ->
- xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
- (* Auxiliary file and library management *)
- | VernacAddLoadPath (recf,name,None) ->
- xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name] []
- | VernacAddLoadPath (recf,name,Some dp) ->
- xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name]
- [PCData (Names.DirPath.to_string dp)]
- | VernacRemoveLoadPath name -> xmlRemoveLoadPath loc ~attr:["path",name] []
- | VernacAddMLPath (recf,name) ->
- xmlAddMLPath loc ~attr:["rec",string_of_bool recf;"path",name] []
- | VernacDeclareMLModule sl -> xmlDeclareMLModule loc sl
- | VernacChdir _ as x -> xmlTODO loc x
-
- (* State management *)
- | VernacWriteState _ as x -> xmlTODO loc x
- | VernacRestoreState _ as x -> xmlTODO loc x
-
- (* Resetting *)
- | VernacResetName _ as x -> xmlTODO loc x
- | VernacResetInitial as x -> xmlTODO loc x
- | VernacBack _ as x -> xmlTODO loc x
- | VernacBackTo _ -> PCData "VernacBackTo"
-
- (* Commands *)
- | VernacCreateHintDb _ as x -> xmlTODO loc x
- | VernacRemoveHints _ as x -> xmlTODO loc x
- | VernacHints _ as x -> xmlTODO loc x
- | VernacSyntacticDefinition ((_, name), (idl, ce), _, _) ->
- let name = Id.to_string name in
- let attrs = List.map (fun id -> ("id", Id.to_string id)) idl in
- xmlNotation attrs name loc [pp_expr ce]
- | VernacDeclareImplicits _ as x -> xmlTODO loc x
- | VernacArguments _ as x -> xmlTODO loc x
- | VernacArgumentsScope _ as x -> xmlTODO loc x
- | VernacReserve _ as x -> xmlTODO loc x
- | VernacGeneralizable _ as x -> xmlTODO loc x
- | VernacSetOpacity _ as x -> xmlTODO loc x
- | VernacSetStrategy _ as x -> xmlTODO loc x
- | VernacUnsetOption _ as x -> xmlTODO loc x
- | VernacSetOption _ as x -> xmlTODO loc x
- | VernacAddOption _ as x -> xmlTODO loc x
- | VernacRemoveOption _ as x -> xmlTODO loc x
- | VernacMemOption _ as x -> xmlTODO loc x
- | VernacPrintOption _ as x -> xmlTODO loc x
- | VernacCheckMayEval (_,_,e) -> xmlCheck loc [pp_expr e]
- | VernacGlobalCheck _ as x -> xmlTODO loc x
- | VernacDeclareReduction _ as x -> xmlTODO loc x
- | VernacPrint _ as x -> xmlTODO loc x
- | VernacSearch _ as x -> xmlTODO loc x
- | VernacLocate _ as x -> xmlTODO loc x
- | VernacRegister _ as x -> xmlTODO loc x
- | VernacComments (cl) ->
- xmlComment loc (List.flatten (List.map pp_comment cl))
-
- (* Stm backdoor *)
- | VernacStm _ as x -> xmlTODO loc x
-
- (* Proof management *)
- | VernacGoal _ as x -> xmlTODO loc x
- | VernacAbort _ as x -> xmlTODO loc x
- | VernacAbortAll -> PCData "VernacAbortAll"
- | VernacRestart as x -> xmlTODO loc x
- | VernacUndo _ as x -> xmlTODO loc x
- | VernacUndoTo _ as x -> xmlTODO loc x
- | VernacBacktrack _ as x -> xmlTODO loc x
- | VernacFocus _ as x -> xmlTODO loc x
- | VernacUnfocus as x -> xmlTODO loc x
- | VernacUnfocused as x -> xmlTODO loc x
- | VernacBullet _ as x -> xmlTODO loc x
- | VernacSubproof _ as x -> xmlTODO loc x
- | VernacEndSubproof as x -> xmlTODO loc x
- | VernacShow _ as x -> xmlTODO loc x
- | VernacCheckGuard as x -> xmlTODO loc x
- | VernacProof (tac,using) ->
- let tac = Option.map (xmlRawTactic "closingtactic") tac in
- let using = Option.map (xmlSectionSubsetDescr "using") using in
- xmlProof loc (Option.List.(cons tac (cons using [])))
- | VernacProofMode name -> xmlProofMode loc name
-
- (* Toplevel control *)
- | VernacToplevelControl _ as x -> xmlTODO loc x
-
- (* For extension *)
- | VernacExtend _ as x ->
- xmlExtend loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
- (* Flags *)
- | VernacProgram e -> xmlApply loc (Element("program",[],[]) :: [tmpp e loc])
- | VernacLocal (b,e) ->
- xmlApply loc (Element("local",["flag",string_of_bool b],[]) ::
- [tmpp e loc])
-
-let tmpp v loc =
- match tmpp v loc with
- | Element("ltac",_,_) as x -> x
- | xml -> xmlGallina loc [xml]
diff --git a/stm/texmacspp.mli b/stm/texmacspp.mli
deleted file mode 100644
index 858847fb6a..0000000000
--- a/stm/texmacspp.mli
+++ /dev/null
@@ -1,12 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Xml_datatype
-open Vernacexpr
-
-val tmpp : vernac_expr -> Loc.t -> xml
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
+
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index ecaf0fb7c5..a602d6b8a8 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -10,6 +10,8 @@ open Vernacexpr
open Errors
open Pp
+let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+
let string_of_in_script b = if b then " (inside script)" else ""
let string_of_vernac_type = function
@@ -19,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 ^
@@ -91,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
@@ -103,39 +108,46 @@ 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 false, 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 "curly" },
+ VtLater
(* Options changing parser *)
| VernacUnsetOption (["Default";"Proof";"Using"])
| VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
(* StartProof *)
| VernacDefinition (
(Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) ->
- VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater
+ VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater
| VernacDefinition (_,((_,i),_),ProveBody _) ->
- VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
+ VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater
| VernacStartTheoremProof (_,l,_) ->
let ids =
CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
- VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
- | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
+ VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
+ | VernacGoal _ -> VtStartProof (default_proof_mode (),GuaranteesOpacity,[]), VtLater
| VernacFixpoint (_,l) ->
let ids, open_proof =
List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
- then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+ then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
else VtSideff ids, VtLater
| VernacCoFixpoint (_,l) ->
let ids, open_proof =
List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
- then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+ then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
else VtSideff ids, VtLater
(* Sideff: apply to all open branches. usually run on master only *)
| VernacAssumption (_,_,l) ->
@@ -217,4 +229,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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 03:50:16 +0000