From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- stm/asyncTaskQueue.ml | 48 +- stm/dag.ml | 94 ++-- stm/dag.mli | 50 +- stm/lemmas.ml | 116 +++-- stm/lemmas.mli | 14 +- stm/proofBlockDelimiter.ml | 184 +++++++ stm/proofBlockDelimiter.mli | 41 ++ stm/spawned.ml | 17 +- stm/stm.ml | 1165 ++++++++++++++++++++++++++++--------------- stm/stm.mli | 94 +++- stm/stm.mllib | 2 +- stm/tQueue.ml | 2 +- stm/texmacspp.ml | 770 ---------------------------- stm/texmacspp.mli | 12 - stm/vcs.ml | 77 ++- stm/vcs.mli | 66 +-- stm/vernac_classifier.ml | 67 +-- stm/vio_checking.ml | 4 +- stm/workerPool.ml | 4 +- 19 files changed, 1391 insertions(+), 1436 deletions(-) create mode 100644 stm/proofBlockDelimiter.ml create mode 100644 stm/proofBlockDelimiter.mli delete mode 100644 stm/texmacspp.ml delete mode 100644 stm/texmacspp.mli (limited to 'stm') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index cc973260..fa6422cd 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Pp open Util @@ -60,9 +60,7 @@ module Make(T : Task) = struct type more_data = | MoreDataUnivLevel of Univ.universe_level list - - let request_expiry_of_task (t, c) = T.request_of_task t, c - + let slave_respond (Request r) = let res = T.perform r in Response res @@ -106,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) @@ -125,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 -> @@ -184,6 +183,13 @@ module Make(T : Task) = struct let () = Unix.sleep 1 in kill_if () in + let kill_if () = + try kill_if () + with Sys.Break -> + let () = stop_waiting := true in + let () = TQueue.broadcast queue in + Worker.kill proc + in let _ = Thread.create kill_if () in try while true do @@ -223,10 +229,8 @@ module Make(T : Task) = struct | (Die | TQueue.BeingDestroyed) -> giveback_exec_token (); kill proc; exit () | Sys_error _ | Invalid_argument _ | End_of_file -> - giveback_exec_token (); T.on_task_cancellation_or_expiration_or_slave_death !last_task; - kill proc; - exit () + giveback_exec_token (); kill proc; exit () end module Pool = WorkerPool.Make(Model) @@ -294,11 +298,27 @@ module Make(T : Task) = struct let slave_handshake () = Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc) + let pp_pid pp = + (* Breaking all abstraction barriers... very nice *) + let get_xml pp = match Richpp.repr pp with + | Xml_datatype.Element("_", [], xml) -> xml + | _ -> assert false in + Richpp.richpp_of_xml (Xml_datatype.Element("_", [], + get_xml (Richpp.richpp_of_pp Pp.(str (System.process_id ()^ " "))) @ + get_xml pp)) + + let debug_with_pid = Feedback.(function + | { contents = Message(Debug, loc, pp) } as fb -> + { fb with contents = Message(Debug,loc,pp_pid pp) } + | x -> x) + let main_loop () = + (* We pass feedback to master *) 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 (); + Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in + Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x); + Feedback.set_logger Feedback.feedback_logger; + (* We ask master to allocate universe identifiers *) Universes.set_remote_new_univ_level (bufferize (fun () -> marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; match unmarshal_more_data (Option.get !slave_ic) with @@ -314,7 +334,7 @@ module Make(T : Task) = struct let response = slave_respond request in report_status "Idle"; marshal_response (Option.get !slave_oc) response; - Ephemeron.clear () + CEphemeron.clear () with | MarshalError s -> pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2 @@ -337,7 +357,7 @@ module Make(T : Task) = struct let with_n_workers n f = let q = create n in try let rc = f q in destroy q; rc - with e -> let e = Errors.push e in destroy q; iraise e + with e -> let e = CErrors.push e in destroy q; iraise e let n_workers { active } = Pool.n_workers active diff --git a/stm/dag.ml b/stm/dag.ml index 0c7f9f34..99e7c926 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 6b4442df..e783cd8e 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 f06abfcc..022c89ad 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -9,7 +9,7 @@ (* Created by Hugo Herbelin from contents related to lemma proofs in file command.ml, Aug 2009 *) -open Errors +open CErrors open Util open Flags open Pp @@ -31,20 +31,22 @@ open Reductionops open Constrexpr open Constrintern open Impargs +open Context.Rel.Declaration type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a let mk_hook hook = hook let call_hook fix_exn hook l c = try hook l c - with e when Errors.noncritical e -> - let e = Errors.push e in + with e when CErrors.noncritical e -> + let e = CErrors.push e in iraise (fix_exn e) (* Support for mutually proved theorems *) let retrieve_first_recthm = function | VarRef id -> - (pi2 (Global.lookup_named id),variable_opacity id) + let open Context.Named.Declaration in + (get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in (Global.body_of_constant_body cb, is_opaque cb) @@ -77,7 +79,7 @@ let adjust_guardness_conditions const = function List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l) env (Safe_typing.side_effects_of_private_constants eff) in let indexes = - search_guard Loc.ghost env + search_guard Loc.ghost env possible_indexes fixdecls in (mkFix ((indexes,0),fixdecls), ctx), eff | _ -> (body, ctx), eff) } @@ -104,20 +106,21 @@ let find_mutually_recursive_statements thms = (* Cofixpoint or fixpoint w/o explicit decreasing argument *) | None | Some (None, CStructRec) -> let whnf_hyp_hds = map_rel_context_in_env - (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c)) + (fun env c -> fst (whd_all_stack env Evd.empty c)) (Global.env()) hyps in let ind_hyps = - List.flatten (List.map_i (fun i (_,b,t) -> + List.flatten (List.map_i (fun i decl -> + let t = get_type decl in match kind_of_term t with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in - mind.mind_finite <> Decl_kinds.CoFinite && Option.is_empty b -> + mind.mind_finite <> Decl_kinds.CoFinite && is_local_assum decl -> [ind,x,i] | _ -> []) 0 (List.rev whnf_hyp_hds)) in let ind_ccl = let cclenv = push_rel_context hyps (Global.env()) in - let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in + let whnf_ccl,_ = whd_all_stack cclenv Evd.empty ccl in match kind_of_term whnf_ccl with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in @@ -147,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, [] | [], _::_ -> @@ -155,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.")); @@ -207,8 +210,8 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook = definition_message id; Option.iter (Universes.register_universe_binders r) pl; call_hook (fun exn -> exn) hook l r - with e when Errors.noncritical e -> - let e = Errors.push e in + with e when CErrors.noncritical e -> + let e = CErrors.push e in iraise (fix_exn e) let default_thm_id = Id.of_string "Unnamed_thm" @@ -249,10 +252,14 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i, | Some body -> let body = norm body in let k = Kindops.logical_kind_of_goal_kind kind in - let body_i = match kind_of_term body with + let rec body_i t = match kind_of_term t with | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) | CoFix (0,decls) -> mkCoFix (i,decls) + | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) + | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t) + | App (t, args) -> mkApp (body_i t, args) | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body) in + let body_i = body_i body in match locality with | Discharge -> let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p @@ -298,13 +305,16 @@ let save_anonymous_with_strength ?export_seff proof kind save_ident = (* Admitted *) +let warn_let_as_axiom = + CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" + (fun id -> strbrk "Let definition" ++ spc () ++ pr_id id ++ + spc () ++ strbrk "declared as an axiom.") + let admit (id,k,e) pl hook () = let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in let () = match k with | Global, _, _ -> () - | Local, _, _ | Discharge, _, _ -> - msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++ - str "declared as an axiom.") + | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id in let () = assumption_message id in Option.iter (Universes.register_universe_binders (ConstRef kn)) pl; @@ -329,10 +339,11 @@ let check_exist = ) let universe_proof_terminator compute_guard hook = - let open Proof_global in function + let open Proof_global in + 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, [] @@ -347,12 +358,16 @@ let universe_proof_terminator compute_guard hook = save_anonymous_with_strength ~export_seff proof kind id end; check_exist exports + end let standard_proof_terminator compute_guard hook = universe_proof_terminator compute_guard (fun _ -> hook) -let start_proof id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = - let terminator = standard_proof_terminator compute_guard hook in +let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook = + let terminator = match terminator with + | None -> standard_proof_terminator compute_guard hook + | Some terminator -> terminator compute_guard hook + in let sign = match sign with | Some sign -> sign @@ -361,8 +376,11 @@ let start_proof id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = !start_hook c; Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator -let start_proof_univs id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = - let terminator = universe_proof_terminator compute_guard hook in +let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook = + let terminator = match terminator with + | None -> universe_proof_terminator compute_guard hook + | Some terminator -> terminator compute_guard hook + in let sign = match sign with | Some sign -> sign @@ -392,7 +410,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 @@ -422,7 +440,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = let body,opaq = retrieve_first_recthm ref in let subst = Evd.evar_universe_context_subst ctx in let norm c = Universes.subst_opt_univs_constr subst c in - let ctx = Evd.evar_universe_context_set (*FIXME*) Univ.UContext.empty ctx in + let ctx = UState.context_set (*FIXME*) ctx in let body = Option.map norm body in List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in @@ -431,7 +449,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = call_hook (fun exn -> exn) hook strength ref) thms_data in start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard -let start_proof_com kind thms hook = +let start_proof_com ?inference_hook kind thms hook = let env0 = Global.env () in let levels = Option.map snd (fst (List.hd thms)) in let evdref = ref (match levels with @@ -441,8 +459,10 @@ let start_proof_com kind thms hook = let thms = List.map (fun (sopt,(bl,t,guard)) -> let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in - evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref); - let ids = List.map pi1 ctx in + let flags = all_and_fail_flags in + let flags = { flags with use_hook = inference_hook } in + evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); + let ids = List.map get_name ctx in (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), (ids, imps @ lift_implicits (List.length ids) imps'), @@ -451,6 +471,11 @@ let start_proof_com kind thms hook = let recguard,thms,snl = look_for_possibly_mutual_statements thms in let evd, nf = Evarutil.nf_evars_and_universes !evdref in let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in + let () = + match levels with + | None -> () + | Some l -> ignore (Evd.universe_context evd ?names:l) + in let evd = if pi2 kind then evd else (* We fix the variables to ensure they won't be lowered to Set *) @@ -461,6 +486,18 @@ let start_proof_com kind thms hook = (* Saving a proof *) +let keep_admitted_vars = ref true + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "keep section variables in admitted proofs"; + optkey = ["Keep"; "Admitted"; "Variables"]; + optread = (fun () -> !keep_admitted_vars); + optwrite = (fun b -> keep_admitted_vars := b) } + let save_proof ?proof = function | Vernacexpr.Admitted -> let pe = @@ -474,14 +511,18 @@ let save_proof ?proof = function error "Admitted requires an explicit statement"; let typ = Option.get const_entry_type in let ctx = Evd.evar_context_universe_context (fst universes) in - Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes) + let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in + Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes) | None -> + let pftree = Pfedit.get_pftreestate () in let id, k, typ = Pfedit.current_proof_statement () in + let universes = Proof.initial_euctx pftree in (* This will warn if the proof is complete *) - let pproofs, universes = + let pproofs, _univs = Proof_global.return_proof ~allow_partial:true () in let sec_vars = - match Pfedit.get_used_variables(), pproofs with + if not !keep_admitted_vars then None + else match Pfedit.get_used_variables(), pproofs with | Some _ as x, _ -> x | None, (pproof, _) :: _ -> let env = Global.env () in @@ -490,11 +531,12 @@ let save_proof ?proof = function Some (Environ.keep_hyps env (Idset.union ids_typ ids_def)) | _ -> None in let names = Pfedit.get_universe_binders () in - let binders, ctx = Evd.universe_context ?names (Evd.from_ctx universes) in + let evd = Evd.from_ctx universes in + let binders, ctx = Evd.universe_context ?names evd in Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None), (universes, Some binders)) in - Proof_global.get_terminator() pe + Proof_global.apply_terminator (Proof_global.get_terminator ()) pe | Vernacexpr.Proved (is_opaque,idopt) -> let (proof_obj,terminator) = match proof with @@ -504,12 +546,10 @@ let save_proof ?proof = function in (* if the proof is given explicitly, nothing has to be deleted *) if Option.is_empty proof then Pfedit.delete_current_proof (); - terminator (Proof_global.Proved (is_opaque,idopt,proof_obj)) + Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj))) (* Miscellaneous *) let get_current_context () = - try Pfedit.get_current_goal_context () - with e when Logic.catchable_exception e -> - 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 16e54e31..39c089be 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -9,8 +9,6 @@ open Names open Term open Decl_kinds -open Constrexpr -open Vernacexpr open Pfedit type 'a declaration_hook @@ -24,16 +22,20 @@ val call_hook : val set_start_hook : (types -> unit) -> unit val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> + ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> unit declaration_hook -> unit val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> + ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> unit -val start_proof_com : goal_kind -> Vernacexpr.proof_expr list -> +val start_proof_com : + ?inference_hook:Pretyping.inference_hook -> + goal_kind -> Vernacexpr.proof_expr list -> unit declaration_hook -> unit val start_proof_with_initialization : @@ -43,6 +45,11 @@ val start_proof_with_initialization : (types * (Name.t list * Impargs.manual_explicitation list))) list -> int list option -> unit declaration_hook -> unit +val universe_proof_terminator : + Proof_global.lemma_possible_guards -> + (Evd.evar_universe_context option -> unit declaration_hook) -> + Proof_global.proof_terminator + val standard_proof_terminator : Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator @@ -60,4 +67,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 00000000..8162fc3b --- /dev/null +++ b/stm/proofBlockDelimiter.ml @@ -0,0 +1,184 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Goal.goal -> Goal.goal list -> bool +val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ] + +type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ] + +val crawl : + document_view -> ?init:document_node option -> + ('a -> document_node -> 'a until) -> 'a -> + static_block_declaration option + +val unit_val : Stm.DynBlockData.t +val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t +val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet +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 { block_stop = entry_point.id; block_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 { block_stop = entry_point.id; block_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 { block_stop = entry_point.id; block_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 { block_stop = entry_point.id; block_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 00000000..a55032a4 --- /dev/null +++ b/stm/proofBlockDelimiter.mli @@ -0,0 +1,41 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Goal.goal -> Goal.goal list -> bool +val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ] + +type 'a until = [ `Stop | `Found of Stm.static_block_declaration | `Cont of 'a ] + +(* Simpler function to crawl the document backward to detect the block. + * ?init is the entry point of the document view if not given *) +val crawl : + Stm.document_view -> ?init:Stm.document_node option -> + ('a -> Stm.document_node -> 'a until) -> 'a -> + Stm.static_block_declaration option + +(* Dummy value for static_block_declaration when no real value is needed *) +val unit_val : Stm.DynBlockData.t + +(* Bullets *) +val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t +val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet + diff --git a/stm/spawned.ml b/stm/spawned.ml index c6df8726..c5bd5f6f 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 @@ -59,7 +46,7 @@ let control_channel = ref None let channels = ref None let init_channels () = - if !channels <> None then Errors.anomaly(Pp.str "init_channels called twice"); + if !channels <> None then CErrors.anomaly(Pp.str "init_channels called twice"); let () = match !main_channel with | None -> () | Some (Socket(mh,mpr,mpw)) -> @@ -78,7 +65,7 @@ let init_channels () = | Some (Socket (ch, cpr, cpw)) -> controller ch cpr cpw | Some AnonPipe -> - Errors.anomaly (Pp.str "control channel cannot be a pipe") + CErrors.anomaly (Pp.str "control channel cannot be a pipe") let get_channels () = match !channels with diff --git a/stm/stm.ml b/stm/stm.ml index d8b2de4a..b4331dc4 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -8,16 +8,21 @@ 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 () + +(* Opening ppvernac below aliases Richpp, see PR#185 *) +let pp_to_richpp = Richpp.richpp_of_pp +let str_to_richpp = Richpp.richpp_of_string open Vernacexpr -open Errors +open CErrors open Pp open Names open Util open Ppvernac open Vernac_classifier +open Feedback module Hooks = struct @@ -27,28 +32,25 @@ 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) () +let forward_feedback, forward_feedback_hook = + let m = Mutex.create () in + Hook.make ~default:(function + | { id = id; route; contents } -> + try Mutex.lock m; feedback ~id:id ~route contents; Mutex.unlock m + with e -> Mutex.unlock m; raise e) () 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 (Message(Error, Some loc, pp_to_richpp 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) (Message(Error, Some loc, pp_to_richpp msg))) () let unreachable_state, unreachable_state_hook = Hook.make ~default:(fun _ _ -> ()) () @@ -80,8 +82,28 @@ 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 _ } -> true + | { expr = VernacExtend (("Extraction",_), _) } -> true + | { expr = VernacExtend (("SeparateExtraction",_), _) } -> true + | { expr = VernacExtend (("ExtractionLibrary",_), _) } -> true + | { expr = VernacExtend (("RecursiveExtractionLibrary",_), _) } -> true + | { expr = VernacExtend (("ExtractionConstant",_), _) } -> true + | { expr = VernacExtend (("ExtractionInlinedConstant",_), _) } -> true + | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true + | _ -> false (* Wrapper for Vernacentries.interp to set the feedback id *) let vernac_interp ?proof id ?route { verbose; loc; expr } = @@ -89,34 +111,48 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } = | VernacResetName _ | VernacResetInitial | VernacBack _ | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true - | VernacTime el | VernacRedirect (_,el) -> List.for_all (fun (_,e) -> internal_command e) el + | 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 + let e = CErrors.push e in iraise Hooks.(call_process_error_once e) 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 - with e when Errors.noncritical e -> - let (e, info) = Errors.push e in + | Some (loc, ast) -> indentation, strlen, loc, ast + with e when CErrors.noncritical e -> + let (e, info) = CErrors.push e in let loc = Option.default Loc.ghost (Loc.get_loc info) in Hooks.(call parse_error feedback_id loc (iprint (e, info))); iraise (e, info)) @@ -124,13 +160,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 @@ -140,22 +176,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 ] } -type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list + cblock : proof_block_name option; + cqueue : [ `MainQueue + | `TacQueue of solving_tac * anon_abstracting_tac * 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 @@ -167,40 +208,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; - Evarutil.evar_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 = { + block_start : Stateid.t; + block_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 (* {{{ *) @@ -216,7 +286,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" @@ -224,9 +294,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 @@ -242,7 +312,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 (* }}} *) @@ -264,7 +334,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 @@ -278,30 +348,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 slice : block_start:id -> block_stop:id -> vcs + val nodes_in_slice : block_start:id -> block_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 -> block_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 @@ -317,7 +389,6 @@ end = struct (* {{{ *) include Vcs_ exception Expired = Vcs_aux.Expired - module StateidSet = Set.Make(Stateid) open Printf let print_dag vcs () = @@ -325,21 +396,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 = @@ -359,8 +430,6 @@ end = struct (* {{{ *) let edge tr = sprintf "<%s>" (quote (string_of_transaction tr)) in - let ids = ref StateidSet.empty in - let clus = Hashtbl.create 13 in let node_info id = match get_info vcs id with | None -> "" @@ -373,39 +442,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 = @@ -442,13 +543,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 ()) @@ -466,14 +566,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 @@ -482,54 +582,91 @@ end = struct (* {{{ *) let visit id = Vcs_aux.visit !vcs id - let nodes_in_slice ~start ~stop = + let nodes_in_slice ~block_start ~block_stop = let rec aux id = - if Stateid.equal id start then [] else + if Stateid.equal id block_start then [] else match visit id with | { next = n; step = `Cmd x } -> (id,Cmd x) :: aux n | { next = n; step = `Alias x } -> (id,Alias x) :: aux n | { next = n; step = `Sideff (`Ast (x,_)) } -> (id,Sideff (Some x)) :: aux n - | _ -> anomaly(str("Cannot slice from "^ Stateid.to_string start ^ - " to "^Stateid.to_string stop)) - in aux stop + | _ -> anomaly(str("Cannot slice from "^ Stateid.to_string block_start ^ + " to "^Stateid.to_string block_stop)) + in aux block_stop - let slice ~start ~stop = - let l = nodes_in_slice ~start ~stop in + let slice ~block_start ~block_stop = + let l = nodes_in_slice ~block_start ~block_stop in let copy_info v id = Vcs_.set_info v id - { (get_info id) with state = None; vcs_backup = None,None } in + { (get_info id) with state = Empty; vcs_backup = None,None } in let copy_info_w_state v id = Vcs_.set_info v id { (get_info id) with vcs_backup = None,None } in - let v = Vcs_.empty start in - let v = copy_info v start 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 block_start in + let v = copy_info v block_start in let v = List.fold_right (fun (id,tr) v -> let v = Vcs_.commit v id tr in 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 block_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 - fill stop - - 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) + 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 block_stop in + (* We put in the new dag the first state (since Qed shall run on it, + * see check_task_aux) *) + let v = copy_info_w_state v block_start in + copy_proof_blockes v + + let nodes_in_slice ~block_start ~block_stop = + List.rev (List.map fst (nodes_in_slice ~block_start ~block_stop)) + + 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 ~block_start:lemma = + if not (topo_invariant l) then anomaly (str "overlapping boxes"); + vcs := create_property !vcs l (ProofTask { qed; lemma }) + let create_proof_block ({ block_start; block_stop} as decl) name = + let l = nodes_in_slice ~block_start ~block_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 } + | `Cmd { cqueue = `TacQueue (_,_,cancel_switch) } | `Cmd { cqueue = `QueryQueue cancel_switch } -> cancel_switch := true | _ -> ()) @@ -583,7 +720,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 @@ -603,9 +743,10 @@ 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 + val exn_on : Stateid.t -> valid:Stateid.t -> iexn -> iexn (* to send states across worker/master *) type frozen_state val get_cached : Stateid.t -> frozen_state @@ -634,10 +775,9 @@ end = struct (* {{{ *) States.unfreeze system; Proof_global.unfreeze proof (* hack to make futures functional *) - let in_t, out_t = Dyn.create "state4future" let () = Future.set_freeze - (fun () -> in_t (freeze_global_state `No, !cur_id)) - (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i) + (fun () -> Obj.magic (freeze_global_state `No, !cur_id)) + (fun t -> let s,i = Obj.magic t in unfreeze_global_state s; cur_id := i) type frozen_state = state type proof_part = @@ -649,51 +789,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 @@ -702,17 +851,17 @@ 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) = + let exn_on id ~valid (e, info) = match Stateid.get info with | Some _ -> (e, info) | None -> let loc = Option.default Loc.ghost (Loc.get_loc info) in let (e, info) = Hooks.(call_process_error_once (e, info)) in Hooks.(call execution_error id loc (iprint (e, info))); - (e, Stateid.add info ?valid id) + (e, Stateid.add info ~valid id) let same_env { system = s1 } { system = s2 } = let s1 = States.summary_of_state s1 in @@ -724,12 +873,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; @@ -737,24 +886,27 @@ 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 (e, info) = CErrors.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 (* }}} *) @@ -830,7 +982,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 @@ -840,8 +992,6 @@ end = struct (* {{{ *) | VernacResetInitial -> VtStm (VtBack Stateid.initial, true), VtNow | VernacResetName (_,name) -> - msg_warning - (str"Reset not implemented for automatically generated constants"); let id = VCS.get_branch_pos (VCS.current_branch ()) in (try let oid = @@ -891,8 +1041,8 @@ end = struct (* {{{ *) | _ -> VtUnknown, VtNow with | Not_found -> - msg_warning(str"undo_vernac_classifier: going back to the initial state."); - VtStm (VtBack Stateid.initial, true), VtNow + CErrors.errorlabstrm "undo_vernac_classifier" + (str "Cannot undo") end (* }}} *) @@ -925,10 +1075,78 @@ let record_pb_time proof_name loc time = end exception RemoteException of std_ppcmds -let _ = Errors.register_handler (function +let _ = CErrors.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 + CErrors.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 && + (Flags.async_proofs_is_master () || Flags.async_proofs_is_worker ()) + 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 ({ block_start; block_stop } as decl) -> + VCS.create_proof_block decl name + end + with Not_found -> + CErrors.errorlabstrm "STM" + (str "Unknown proof block delimiter " ++ str name) + ) (****************************** THE SCHEDULER *********************************) (******************************************************************************) @@ -1034,7 +1252,7 @@ end = struct (* {{{ *) try Some (ReqBuildProof ({ Stateid.exn_info = t_exn_info; stop = t_stop; - document = VCS.slice ~start:t_start ~stop:t_stop; + document = VCS.slice ~block_start:t_start ~block_stop:t_stop; loc = t_loc; uuid = t_uuid; name = t_name }, t_drop, t_states)) @@ -1046,7 +1264,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 @@ -1054,7 +1272,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); @@ -1070,7 +1288,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 () -> @@ -1081,7 +1299,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 = @@ -1105,30 +1323,31 @@ 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; RespBuiltProof(proof,time) with - | e when Errors.noncritical e || e = Stack_overflow -> - let (e, info) = Errors.push e in + | e when CErrors.noncritical e || e = Stack_overflow -> + let (e, info) = CErrors.push e in (* This can happen if the proof is broken. The error has also been * signalled as a feedback, hence we can silently recover *) let e_error_at, e_safe_id = match Stateid.get info with | 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 = if query = [] then [] else - let is_tac = function - | VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _ -> true - | _ -> false in + let is_tac e = match classify_vernac e with + | VtProofStep _, _ -> true + | _ -> false + in let initial = let rec aux id = try match VCS.visit id with { next } -> aux next @@ -1138,19 +1357,19 @@ 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 when is_tac expr && State.same_env o n -> (* A pure tactic *) Some (id, `Proof (prev, State.proof_part_of_frozen n)) | Some _, Some s -> - msg_warning (str "STM: sending back a fat state"); + msg_debug (str "STM: sending back a fat state"); Some (id, `Full s) | _, Some s -> Some (id, `Full s) in let rec aux seen = function @@ -1173,7 +1392,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 (* }}} *) @@ -1183,7 +1402,7 @@ and Slaves : sig (* (eventually) remote calls *) val build_proof : loc:Loc.t -> drop_pt:bool -> - exn_info:(Stateid.t * Stateid.t) -> start:Stateid.t -> stop:Stateid.t -> + exn_info:(Stateid.t * Stateid.t) -> block_start:Stateid.t -> block_stop:Stateid.t -> name:string -> future_proof * cancel_switch (* blocking function that waits for the task queue to be empty *) @@ -1221,8 +1440,8 @@ end = struct (* {{{ *) let check_task_aux extra name l i = let { Stateid.stop; document; loc; name = r_name }, drop = List.nth l i in - msg_info( - str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name)); + Flags.if_verbose msg_info + (str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name)); VCS.restore document; let start = let rec aux cur = @@ -1245,15 +1464,15 @@ 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 with e -> - let (e, info) = Errors.push e in + let (e, info) = CErrors.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) -> @@ -1263,12 +1482,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 -> @@ -1328,7 +1547,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 @@ -1343,7 +1561,7 @@ end = struct (* {{{ *) BuildProof { t_states = s2 } -> overlap_rel s1 s2 | _ -> 0) - let build_proof ~loc ~drop_pt ~exn_info ~start ~stop ~name:pname = + let build_proof ~loc ~drop_pt ~exn_info ~block_start ~block_stop ~name:pname = let id, valid as t_exn_info = exn_info in let cancel_switch = ref false in if TaskQueue.n_workers (Option.get !queue) = 0 then @@ -1352,21 +1570,21 @@ end = struct (* {{{ *) Future.create_delegate ~blocking:true ~name:pname (State.exn_on id ~valid) in let t_uuid = Future.uuid f in let task = ProofTask.(BuildProof { - t_exn_info; t_start = start; t_stop = stop; t_drop = drop_pt; + t_exn_info; t_start = block_start; t_stop = block_stop; t_drop = drop_pt; t_assign = assign; t_loc = loc; t_uuid; t_name = pname; - t_states = VCS.nodes_in_slice ~start ~stop }) in + t_states = VCS.nodes_in_slice ~block_start ~block_stop }) in TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch); f, cancel_switch end else - ProofTask.build_proof_here ~drop_pt t_exn_info loc stop, cancel_switch + ProofTask.build_proof_here ~drop_pt t_exn_info loc block_stop, cancel_switch 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_exn_info; t_start = block_start; t_stop = block_stop; t_assign; t_drop = drop_pt; t_loc = loc; t_uuid; t_name = pname; - t_states = VCS.nodes_in_slice ~start ~stop }) in + t_states = VCS.nodes_in_slice ~block_start ~block_stop }) in TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch); f, cancel_switch @@ -1385,7 +1603,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) @@ -1399,10 +1617,11 @@ and TacTask : sig t_state : Stateid.t; t_state_fb : Stateid.t; t_assign : output Future.assignement -> unit; - t_ast : ast; + t_ast : int * aast; t_goal : Goal.goal; t_kill : unit -> unit; t_name : string } + exception NoProgress include AsyncTaskQueue.Task with type task := task @@ -1416,7 +1635,7 @@ end = struct (* {{{ *) t_state : Stateid.t; t_state_fb : Stateid.t; t_assign : output Future.assignement -> unit; - t_ast : ast; + t_ast : int * aast; t_goal : Goal.goal; t_kill : unit -> unit; t_name : string } @@ -1425,13 +1644,15 @@ end = struct (* {{{ *) r_state : Stateid.t; r_state_fb : Stateid.t; r_document : VCS.vcs option; - r_ast : ast; + r_ast : int * aast; r_goal : Goal.goal; r_name : string } type response = | RespBuiltSubProof of output | RespError of std_ppcmds + | RespNoProgress + exception NoProgress let name = ref "tacworker" let extra_env () = [||] @@ -1445,7 +1666,7 @@ end = struct (* {{{ *) r_state_fb = t_state_fb; r_document = if age <> `Fresh then None - else Some (VCS.slice ~start:t_state ~stop:t_state); + else Some (VCS.slice ~block_start:t_state ~block_stop:t_state); r_ast = t_ast; r_goal = t_goal; r_name = t_name } @@ -1454,9 +1675,13 @@ end = struct (* {{{ *) let use_response _ { t_assign; t_state; t_state_fb; t_kill } resp = match resp with | RespBuiltSubProof o -> t_assign (`Val o); `Stay ((),[]) + | RespNoProgress -> + let e = (NoProgress, Exninfo.null) in + t_assign (`Exn e); + t_kill (); + `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 ((),[]) @@ -1469,36 +1694,37 @@ end = struct (* {{{ *) | Some { t_kill } -> t_kill () | _ -> () + let command_focus = Proof.new_focus_kind () + let focus_cond = Proof.no_cond command_focus + let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } = Option.iter VCS.restore vcs; try Reach.known_state ~cache:`No id; - let t, uc = Future.purify (fun () -> + Future.purify (fun () -> let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in let g = Evd.find sigma0 r_goal in if not ( Evarutil.is_ground_term sigma0 Evd.(evar_concl g) && - List.for_all (fun (_,bo,ty) -> - Evarutil.is_ground_term sigma0 ty && - Option.cata (Evarutil.is_ground_term sigma0) true bo) - Evd.(evar_context g)) + 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 "^ + CErrors.errorlabstrm "STM" (strbrk("the par: goal selector supports ground "^ "goals only")) else begin - vernac_interp r_state_fb r_ast; + let (i, ast) = r_ast in + Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p); + 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 -> RespNoProgress | 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") + RespBuiltSubProof (t, Evd.evar_universe_context sigma) + else CErrors.errorlabstrm "STM" (str"The solution is not ground") end) () - in - RespBuiltSubProof (t,uc) - with e when Errors.noncritical e -> RespError (Errors.print e) + with e when CErrors.noncritical e -> RespError (CErrors.print e) let name_of_task { t_name } = t_name let name_of_request { r_name } = r_name @@ -1508,19 +1734,22 @@ end (* }}} *) and Partac : sig val vernac_interp : - cancel_switch -> int -> Stateid.t -> Stateid.t -> ast -> unit + solve:bool -> abstract:bool -> 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 e, etac, time, fail = + let vernac_interp ~solve ~abstract cancel nworkers safe_id id + { indentation; verbose; loc; expr = e; strlen } + = + let e, time, fail = let rec find time fail = function - | VernacSolve(_,_,re,b) -> re, b, time, fail - | VernacTime [_,e] | VernacRedirect (_,[_,e]) -> find true fail e + | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e | VernacFail e -> find time true e - | _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in + | _ -> e, time, fail in find false false e in Hooks.call Hooks.with_fail fail (fun () -> (if time then System.with_time false else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> @@ -1532,51 +1761,58 @@ end = struct (* {{{ *) Future.create_delegate ~name:(Printf.sprintf "subgoal %d" i) (State.exn_on id ~valid:safe_id) in - let t_ast = - { verbose;loc;expr = VernacSolve(SelectNth i,None,e,etac) } 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; t_assign = assign; t_ast; t_goal = g; t_name; - t_kill = (fun () -> TaskQueue.cancel_all queue) }, cancel); - Goal.uid g,f) + t_kill = (fun () -> if solve then TaskQueue.cancel_all queue) }, + cancel); + g,f) 1 goals in TaskQueue.join queue; let assign_tac : unit Proofview.tactic = - Proofview.V82.tactic (fun gl -> - let open Tacmach in - let sigma, g = project gl, sig_it gl in - let gid = Goal.uid g in - let f = - try List.assoc gid res - with Not_found -> Errors.anomaly(str"Partac: wrong focus") in - if Future.is_over f then + Proofview.(Goal.nf_enter { Goal.enter = fun g -> + let gid = Goal.goal g in + let f = + try List.assoc gid res + with Not_found -> CErrors.anomaly(str"Partac: wrong focus") in + if not (Future.is_over f) then + (* One has failed and cancelled the others, but not this one *) + if solve then Tacticals.New.tclZEROMSG + (str"Interrupted by the failure of another goal") + else tclUNIT () + else + let open Notations in + try let pt, uc = Future.join f in - prerr_endline (string_of_ppcmds(hov 0 ( - str"g=" ++ str gid ++ spc () ++ + prerr_endline (fun () -> string_of_ppcmds(hov 0 ( + str"g=" ++ int (Evar.repr gid) ++ spc () ++ str"t=" ++ (Printer.pr_constr pt) ++ spc () ++ str"uc=" ++ Evd.pr_evar_universe_context uc))); - let sigma = Goal.V82.partial_solution sigma g pt in - let sigma = Evd.merge_universe_context sigma uc in - re_sig [] sigma - else (* One has failed and cancelled the others, but not this one *) - re_sig [g] sigma) in + (if abstract then Tactics.tclABSTRACT None else (fun x -> x)) + (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*> + Tactics.exact_no_check pt) + with TacTask.NoProgress -> + if solve then Tacticals.New.tclSOLVE [] else tclUNIT () + }) + in Proof.run_tactic (Global.env()) assign_tac p)))) ()) 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" @@ -1588,7 +1824,7 @@ end = struct (* {{{ *) try Some { r_where = t_where; r_for = t_for; - r_doc = VCS.slice ~start:t_where ~stop:t_where; + r_doc = VCS.slice ~block_start:t_where ~block_stop:t_where; r_what = t_what } with VCS.Expired -> None @@ -1608,11 +1844,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 - 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) Processed + with e when CErrors.noncritical e -> + let e = CErrors.push e in + let msg = pp_to_richpp (iprint e) in + feedback ~id:(State r_for) (Message (Error, None, 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) @@ -1622,7 +1858,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 (* {{{ *) @@ -1633,7 +1869,7 @@ end = struct (* {{{ *) let vernac_interp switch prev id q = assert(TaskQueue.n_workers (Option.get !queue) > 0); TaskQueue.enqueue_task (Option.get !queue) - QueryTask.({ QueryTask.t_where = prev; t_for = id; t_what = q }, switch) + QueryTask.({ t_where = prev; t_for = id; t_what = q }, switch) let init () = queue := Some (TaskQueue.create (if !Flags.async_proofs_full then 1 else 0)) @@ -1659,12 +1895,18 @@ 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 warn_deprecated_nested_proofs = + CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated" + (fun () -> + strbrk ("Nested proofs are deprecated and will "^ + "stop working in a future Coq version")) 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 @@ -1684,16 +1926,20 @@ let collect_proof keep cur hd brkind id = let has_proof_no_using = function | Some (_, { expr = VernacProof(_,None) }) -> true | _ -> false in - let may_pierce_opaque = function - | { expr = VernacPrint (PrintName _) } -> true - | _ -> false in + let too_complex_to_delegate = function + | { expr = (VernacDeclareModule _ + | VernacDefineModule _ + | VernacDeclareModuleType _ + | VernacInclude _) } -> true + | { expr = (VernacRequire _ | VernacImport _) } -> true + | ast -> may_pierce_opaque ast in let parent = function Some (p, _) -> p | None -> assert false in let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in let rec collect last accn id = let view = VCS.visit id in match view.step with | (`Sideff (`Ast(x,_)) | `Cmd { cast = x }) - when may_pierce_opaque x -> `Sync(no_name,None,`Print) + when too_complex_to_delegate x -> `Sync(no_name,None,`Print) | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next | `Sideff (`Ast(x,_)) -> collect (Some (id,x)) (id::accn) view.next (* An Alias could jump everywhere... we hope we can ignore it*) @@ -1707,7 +1953,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 @@ -1723,8 +1969,7 @@ let collect_proof keep cur hd brkind id = let name = name ids in `MaybeASync (parent last, None, accn, name, delegate name) | `Sideff _ -> - Pp.(msg_warning (strbrk ("Nested proofs are deprecated and will "^ - "stop working in the next Coq version"))); + warn_deprecated_nested_proofs (); `Sync (no_name,None,`NestedProof) | _ -> `Sync (no_name,None,`Unknown) in let make_sync why = function @@ -1743,7 +1988,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 @@ -1761,7 +2006,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 ) @@ -1773,6 +2018,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 ({ block_stop } as decl, name) when Stateid.equal block_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 -> + CErrors.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 CErrors.noncritical e -> + let ie = CErrors.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 CErrors.noncritical e -> () in (* ugly functions to process nested lemmas, i.e. hard to reproduce * side effects *) @@ -1782,18 +2092,18 @@ let known_state ?(redefine_qed=false) ~cache id = let inject_non_pstate (s,l) = Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env () in - let rec pure_cherry_pick_non_pstate id = Future.purify (fun id -> - prerr_endline ("cherry-pick non pstate " ^ Stateid.to_string id); - reach id; + let rec pure_cherry_pick_non_pstate safe_id id = Future.purify (fun id -> + prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id); + reach ~safe_id id; cherry_pick_non_pstate ()) id (* traverses the dag backward from nodes being already calculated *) - and reach ?(redefine_qed=false) ?(cache=cache) id = - prerr_endline ("reaching: " ^ Stateid.to_string id); + and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id = + prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id); if not redefine_qed && State.is_cached ~cache id then begin - State.install_cached id; Hooks.(call state_computed id ~in_cache:true); - prerr_endline ("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 @@ -1801,46 +2111,58 @@ let known_state ?(redefine_qed=false) ~cache id = | `Alias (id,_) -> (fun () -> reach view.next; reach id ), 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 = `SkipQueue } -> (fun () -> + reach view.next), cache, true + | `Cmd { cast = x; cqueue = `TacQueue (solve,abstract,cancel); cblock } -> + (fun () -> + resilient_tactic id cblock (fun () -> + reach ~cache:`Shallow view.next; + Hooks.(call tactic_being_run true); + Partac.vernac_interp ~solve ~abstract + 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; - with e when Errors.noncritical e -> - let (e, info) = Errors.push e in + with e when CErrors.noncritical e -> + let (e, info) = CErrors.push e in let info = Stateid.add info ~valid:prev id in iraise (e, info)); wall_clock_last_fork := Unix.gettimeofday () ), `Yes, true | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) -> let rec aux = function - | `ASync (start, pua, nodes, name, delegate) -> (fun () -> + | `ASync (block_start, pua, nodes, name, delegate) -> (fun () -> assert(keep == VtKeep || keep == VtKeepAsAxiom); let drop_pt = keep == VtKeepAsAxiom in - let stop, exn_info, loc = eop, (id, eop), x.loc in + let block_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 ~block_start; begin match brinfo, qed.fproof with | { VCS.kind = `Edit _ }, None -> assert false | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) -> @@ -1854,19 +2176,22 @@ let known_state ?(redefine_qed=false) ~cache id = ^"the proof's statement to avoid that.")); let fp, cancel = Slaves.build_proof - ~loc ~drop_pt ~exn_info ~start ~stop ~name in + ~loc ~drop_pt ~exn_info ~block_start ~block_stop ~name in Future.replace ofp fp; - qed.fproof <- Some (fp, cancel) + qed.fproof <- Some (fp, cancel); + (* We don't generate a new state, but we still need + * to install the right one *) + State.install_cached id | { VCS.kind = `Proof _ }, Some _ -> assert false | { VCS.kind = `Proof _ }, None -> - reach ~cache:`Shallow start; + reach ~cache:`Shallow block_start; let fp, cancel = if delegate then Slaves.build_proof - ~loc ~drop_pt ~exn_info ~start ~stop ~name + ~loc ~drop_pt ~exn_info ~block_start ~block_stop ~name else ProofTask.build_proof_here - ~drop_pt exn_info loc stop, ref false + ~drop_pt exn_info loc block_stop, ref false in qed.fproof <- Some (fp, cancel); let proof = @@ -1874,7 +2199,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 () @@ -1921,15 +2246,15 @@ let known_state ?(redefine_qed=false) ~cache id = ), cache, true | `Sideff (`Id origin) -> (fun () -> reach view.next; - inject_non_pstate (pure_cherry_pick_non_pstate origin); + inject_non_pstate (pure_cherry_pick_non_pstate view.next origin); ), cache, true in let cache_step = if !Flags.async_proofs_cache = Some Flags.Force then `Yes else cache_step in - State.define + State.define ?safe_id ~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 (* }}} *) @@ -1944,7 +2269,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 -> [] @@ -1963,7 +2288,7 @@ let observe id = Reach.known_state ~cache:(interactive ()) id; VCS.print () with e -> - let e = Errors.push e in + let e = CErrors.push e in VCS.print (); VCS.restore vcs; iraise e @@ -1996,9 +2321,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 () @@ -2011,28 +2336,26 @@ 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 + with e when CErrors.noncritical e -> VCS.restore vcs; false let info_tasks (tasks,_) = Slaves.info_tasks tasks let finish_tasks name u d p (t,rcbackup as tasks) = RemoteCounter.restore rcbackup; let finish_task u (_,_,i) = let vcs = VCS.backup () in let u = Future.purify (Slaves.finish_task name u d p t) i in - pperr_flush (); VCS.restore vcs; u in try let u, a, _ = List.fold_left finish_task u (info_tasks tasks) in (u,a,true), p with e -> - let e = Errors.push e in - pperrnl (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); + let e = CErrors.push e in + msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); exit 1 -let merge_proof_branch ?valid ?id qast keep brname = +let merge_proof_branch ~valid ?id qast keep brname = let brinfo = VCS.get_branch brname in let qed fproof = { qast; keep; brname; brinfo; fproof } in match brinfo with @@ -2041,7 +2364,7 @@ let merge_proof_branch ?valid ?id qast keep brname = let id = VCS.new_node ?id () in VCS.merge id ~ours:(Qed (qed None)) brname; VCS.delete_branch brname; - if keep <> VtDrop then VCS.propagate_sideff None; + VCS.propagate_sideff None; `Ok | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } -> let ofp = @@ -2055,12 +2378,12 @@ let merge_proof_branch ?valid ?id qast keep brname = VCS.checkout VCS.Branch.master; `Unfocus qed_id | { VCS.kind = `Master } -> - iraise (State.exn_on ?valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null)) + iraise (State.exn_on ~valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null)) (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) let handle_failure (e, info) vcs tty = - if e = Errors.Drop then iraise (e, info) else + if e = CErrors.Drop then iraise (e, info) else match Stateid.get info with | None -> VCS.restore vcs; @@ -2072,9 +2395,9 @@ let handle_failure (e, info) vcs tty = end; VCS.print (); anomaly(str"error with no safe_id attached:" ++ spc() ++ - Errors.iprint_no_report (e, info)) + CErrors.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 *) @@ -2085,38 +2408,37 @@ 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 + CErrors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs"); + 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 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)); +let process_transaction ?(newtip=Stateid.fresh ()) ~tty + ({ verbose; loc; expr } as x) c = + 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 | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater") (* Joining various parts of the document *) - | VtStm (VtJoinDocument, b), VtNow -> warn_if_pos x b; join (); `Ok - | VtStm (VtFinish, b), VtNow -> warn_if_pos x b; finish (); `Ok - | VtStm (VtWait, b), VtNow -> warn_if_pos x b; finish (); wait (); `Ok + | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok + | VtStm (VtFinish, b), VtNow -> finish (); `Ok + | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok | VtStm (VtPrintDag, b), VtNow -> - warn_if_pos x b; VCS.print ~now:true (); `Ok - | VtStm (VtObserve id, b), VtNow -> warn_if_pos x b; observe id; `Ok + VCS.print ~now:true (); `Ok + | VtStm (VtObserve id, b), VtNow -> observe id; `Ok | VtStm ((VtObserve _ | VtFinish | VtJoinDocument |VtPrintDag |VtWait),_), VtLater -> anomaly(str"classifier: join actions cannot be classified as VtLater") @@ -2125,9 +2447,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = | VtStm (VtBack oid, true), w -> let id = VCS.new_node ~id:newtip () in let { mine; others } = Backtrack.branches_of oid in + let valid = VCS.get_branch_pos head in List.iter (fun branch -> if not (List.mem_assoc branch (mine::others)) then - ignore(merge_proof_branch x VtDrop branch)) + ignore(merge_proof_branch ~valid x VtDrop branch)) (VCS.branches ()); VCS.checkout_shallowest_proof_branch (); let head = VCS.current_branch () in @@ -2141,7 +2464,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 @@ -2152,22 +2475,26 @@ 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 } - with e when Errors.noncritical e -> - let e = Errors.push e in - iraise (State.exn_on report_id e)); `Ok + {x with verbose = true } + with e when CErrors.noncritical e -> + let e = CErrors.push e in + iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok | VtQuery (false,(report_id,route)), VtNow -> (try vernac_interp report_id ~route x with e -> - let e = Errors.push e in - iraise (State.exn_on report_id e)); `Ok + let e = CErrors.push e in + iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok | VtQuery (true,(report_id,_)), w -> assert(Stateid.equal report_id Stateid.dummy); let id = VCS.new_node ~id:newtip () in let queue = if !Flags.async_proofs_full then `QueryQueue (ref false) + else if Flags.(!compilation_mode = BuildVio) && + VCS.((get_branch head).kind = `Master) && + 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") @@ -2190,7 +2517,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 } -> () @@ -2205,14 +2532,21 @@ 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 = + match parallel with + | `Yes(solve,abstract) -> `TacQueue (solve, abstract, ref false) + | `No -> `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 - let rc = merge_proof_branch ?valid ~id:newtip x keep head in + let valid = VCS.get_branch_pos head in + let rc = merge_proof_branch ~valid ~id:newtip x keep head in VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then finish (); rc @@ -2222,15 +2556,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 *) @@ -2240,17 +2581,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 - VCS.commit id (Fork (x,bname,Doesn'tGuaranteeOpacity,[])); - VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1)); - Proof_global.activate_proof_mode "Classic"; + 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,[])); + 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; @@ -2260,49 +2606,56 @@ 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 + let e = CErrors.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 + CWarnings.set_current_loc loc; + 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 @@ -2312,20 +2665,21 @@ 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 + CWarnings.set_current_loc loc; 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 = @@ -2350,7 +2704,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 @@ -2365,13 +2719,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 (); @@ -2385,14 +2739,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 @@ -2407,14 +2761,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 @@ -2439,14 +2793,14 @@ let edit_at id = VCS.print (); rc with e -> - let (e, info) = Errors.push e in + let (e, info) = CErrors.push e in match Stateid.get info with | None -> VCS.print (); anomaly (str ("edit_at "^Stateid.to_string id^": ") ++ - Errors.print_no_report e) + CErrors.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) @@ -2457,9 +2811,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 && @@ -2472,7 +2827,7 @@ let interp verb (_,e as lexpr) = | _ -> not !Flags.coqtop_ui in try finish ~print_goals () with e -> - let e = Errors.push e in + let e = CErrors.push e in handle_failure e vcs true let finish () = finish () diff --git a/stm/stm.mli b/stm/stm.mli index ad89eb71..b8a2a385 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -9,6 +9,7 @@ open Vernacexpr open Names open Feedback +open Loc (** state-transaction-machine interface *) @@ -19,7 +20,9 @@ open Feedback 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:(located_vernac_expr -> 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 ] @@ -75,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 @@ -93,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 = { + block_start : Stateid.t; + block_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 @@ -119,14 +200,15 @@ 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 -> located_vernac_expr -> unit +val interp : bool -> vernac_expr located -> unit (* Queries for backward compatibility *) val current_proof_depth : unit -> int @@ -134,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 92b3a869..939ee187 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/tQueue.ml b/stm/tQueue.ml index ee121c46..a0b08778 100644 --- a/stm/tQueue.ml +++ b/stm/tQueue.ml @@ -87,7 +87,7 @@ let broadcast { lock = m; cond = c } = Mutex.unlock m let push { queue = q; lock = m; cond = c; release } x = - if release then Errors.anomaly(Pp.str + if release then CErrors.anomaly(Pp.str "TQueue.push while being destroyed! Only 1 producer/destroyer allowed"); Mutex.lock m; PriorityQueue.push q x; diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml deleted file mode 100644 index 85cb4570..00000000 --- a/stm/texmacspp.ml +++ /dev/null @@ -1,770 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (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, 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 l -> - xmlApply loc (Element("time",[],[]) :: - List.map (fun(loc,e) ->tmpp e loc) l) - | VernacRedirect (s, l) -> - xmlApply loc (Element("redirect",["path", s],[]) :: - List.map (fun(loc,e) ->tmpp e loc) l) - | 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 *) - | VernacTacticNotation _ as x -> - xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] - - | 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:[] [] - | VernacBindScope (name,l) -> - xmlScope loc "bind" name - (List.map (function - | ByNotation(loc,name,None) -> xmlNotation [] name loc [] - | ByNotation(loc,name,Some d) -> - xmlNotation ["delimiter",d] name loc [] - | AN ref -> xmlReference ref) l) - | 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] - | 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 *) - - | (VernacSolve _ | 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 *) - | VernacDeclareTacticDefinition _ as x -> xmlTODO loc x - | 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)) - | VernacNop as x -> xmlTODO loc x - - (* 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 858847fb..00000000 --- a/stm/texmacspp.mli +++ /dev/null @@ -1,12 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Loc.t -> xml diff --git a/stm/vcs.ml b/stm/vcs.ml index 38c02990..d3886464 100644 --- a/stm/vcs.ml +++ b/stm/vcs.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors module type S = sig @@ -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 8f22fee8..46b40f8a 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 edb54ece..dc5be08a 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -7,11 +7,18 @@ (************************************************************************) open Vernacexpr -open Errors +open CErrors 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_parallel = function + | `Yes (solve,abs) -> + "par" ^ if solve then "solve" else "" ^ if abs then "abs" else "" + | `No -> "" + let string_of_vernac_type = function | VtUnknown -> "Unknown" | VtStartProof _ -> "StartProof" @@ -19,8 +26,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 " ^ string_of_parallel parallel ^ + Option.default "" proof_block_detection | VtProofMode s -> "ProofMode " ^ s | VtQuery (b,(id,route)) -> "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^ @@ -60,7 +68,7 @@ let undo_classifier = ref (fun _ -> assert false) let set_undo_classifier f = undo_classifier := f let rec classify_vernac e = - let rec static_classifier e = match e with + let static_classifier e = match e with (* PG compatibility *) | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"]) | VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_) @@ -86,12 +94,14 @@ let rec classify_vernac e = make_polymorphic (classify_vernac e) else classify_vernac e | VernacTimeout (_,e) -> classify_vernac e - | VernacTime e | VernacRedirect (_, e) -> classify_vernac_list e + | VernacTime (_,e) | VernacRedirect (_, (_,e)) -> classify_vernac e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match classify_vernac e with | ( VtQuery _ | VtProofStep _ | VtSideff _ | VtStm _ | VtProofMode _ ), _ as x -> x - | VtQed _, _ -> VtProofStep false, VtNow + | VtQed _, _ -> + VtProofStep { parallel = `No; proof_block_detection = None }, + VtNow | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) (* Qed *) | VernacAbort _ -> VtQed VtDrop, VtLater @@ -102,42 +112,47 @@ let rec classify_vernac e = | VernacCheckMayEval _ -> VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater (* ProofStep *) - | VernacSolve (SelectAllParallel,_,_,_) -> VtProofStep true, VtLater | VernacProof _ - | VernacBullet _ | VernacFocus _ | VernacUnfocus - | VernacSubproof _ | VernacEndSubproof - | VernacSolve _ + | VernacSubproof _ | VernacCheckGuard | VernacUnfocused - | VernacSolveExistential _ -> VtProofStep false, VtLater + | VernacSolveExistential _ -> + VtProofStep { parallel = `No; proof_block_detection = None }, VtLater + | VernacBullet _ -> + VtProofStep { parallel = `No; proof_block_detection = Some "bullet" }, + VtLater + | VernacEndSubproof -> + VtProofStep { parallel = `No; + 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) -> @@ -166,7 +181,7 @@ let rec classify_vernac e = | VernacReserve _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ - | VernacUnsetOption _ | VernacSetOption _ + | VernacUnsetOption _ | VernacSetOption _ | VernacSetAppendOption _ | VernacAddOption _ | VernacRemoveOption _ | VernacMemOption _ | VernacPrintOption _ | VernacGlobalCheck _ @@ -175,11 +190,6 @@ let rec classify_vernac e = | VernacRegister _ | VernacNameSectionHypSet _ | VernacComments _ -> VtSideff [], VtLater - | VernacDeclareTacticDefinition (_,l) -> - let open Libnames in - VtSideff (List.map (function - | (Ident (_,r),_,_) -> r - | (Qualid (_,q),_,_) -> snd(repr_qualid q)) l), VtLater (* Who knows *) | VernacLoad _ -> VtSideff [], VtNow (* (Local) Notations have to disappear *) @@ -195,7 +205,6 @@ let rec classify_vernac e = | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ | VernacSyntaxExtension _ | VernacSyntacticDefinition _ - | VernacTacticNotation _ | VernacRequire _ | VernacImport _ | VernacInclude _ | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) @@ -208,7 +217,6 @@ let rec classify_vernac e = | VernacResetName _ | VernacResetInitial | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e (* What are these? *) - | VernacNop | VernacToplevelControl _ | VernacRestoreState _ | VernacWriteState _ -> VtUnknown, VtNow @@ -217,13 +225,6 @@ let rec classify_vernac e = | VernacExtend (s,l) -> try List.assoc s !classifiers l () with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)) - and classify_vernac_list = function - (* spiwack: It would be better to define a monoid on classifiers. - So that the classifier of the list would be the composition of - the classifier of the individual commands. Currently: special - case for singleton lists.*) - | [_,c] -> static_classifier c - | l -> VtUnknown,VtNow in let res = static_classifier e in if Flags.is_universe_polymorphism () then @@ -233,4 +234,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 = `No; proof_block_detection = None}, VtLater diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index d4dcf72c..a6237daa 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -24,7 +24,7 @@ end module Pool = Map.Make(IntOT) let schedule_vio_checking j fs = - if j < 1 then Errors.error "The number of workers must be bigger than 0"; + if j < 1 then CErrors.error "The number of workers must be bigger than 0"; let jobs = ref [] in List.iter (fun f -> let f = @@ -98,7 +98,7 @@ let schedule_vio_checking j fs = exit !rc let schedule_vio_compilation j fs = - if j < 1 then Errors.error "The number of workers must be bigger than 0"; + if j < 1 then CErrors.error "The number of workers must be bigger than 0"; let jobs = ref [] in List.iter (fun f -> let f = diff --git a/stm/workerPool.ml b/stm/workerPool.ml index b94fae54..9623765d 100644 --- a/stm/workerPool.ml +++ b/stm/workerPool.ml @@ -52,7 +52,7 @@ let master_handshake worker_id ic oc = Printf.eprintf "Handshake with %s failed: protocol mismatch\n" worker_id; exit 1; end - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> Printf.eprintf "Handshake with %s failed: %s\n" worker_id (Printexc.to_string e); exit 1 @@ -65,7 +65,7 @@ let worker_handshake slave_ic slave_oc = exit 1; end; Marshal.to_channel slave_oc v []; flush slave_oc; - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> prerr_endline ("Handshake failed: " ^ Printexc.to_string e); exit 1 -- cgit v1.2.3