From fa9df2efe5666789bf91bb7761567cd53e6c451f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 18 Dec 2016 18:14:58 +0100 Subject: [stm] Break stm/toplevel dependency loop. Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore. --- stm/lemmas.ml | 557 --------------------------------------------------------- stm/lemmas.mli | 69 ------- stm/stm.ml | 59 +++--- stm/stm.mli | 5 - stm/stm.mllib | 1 - 5 files changed, 32 insertions(+), 659 deletions(-) delete mode 100644 stm/lemmas.ml delete mode 100644 stm/lemmas.mli (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml deleted file mode 100644 index 55f33be399..0000000000 --- a/stm/lemmas.ml +++ /dev/null @@ -1,557 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Globnames.global_reference -> 'a -let mk_hook hook = hook -let call_hook fix_exn hook l c = - try hook l c - 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 -> - (NamedDecl.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) - | _ -> assert false - -let adjust_guardness_conditions const = function - | [] -> const (* Not a recursive statement *) - | possible_indexes -> - (* Try all combinations... not optimal *) - let env = Global.env() in - { const with const_entry_body = - Future.chain ~greedy:true ~pure:true const.const_entry_body - (fun ((body, ctx), eff) -> - match kind_of_term body with - | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> -(* let possible_indexes = - List.map2 (fun i c -> match i with Some i -> i | None -> - List.interval 0 (List.length ((lam_assum c)))) - lemma_guard (Array.to_list fixdefs) in -*) - let add c cb e = - let exists c e = - try ignore(Environ.lookup_constant c e); true - with Not_found -> false in - if exists c e then e else Environ.add_constant c cb e in - let env = List.fold_left (fun env { eff } -> - match eff with - | SEsubproof (c, cb,_) -> add c cb env - | SEscheme (l,_) -> - 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 - possible_indexes fixdecls in - (mkFix ((indexes,0),fixdecls), ctx), eff - | _ -> (body, ctx), eff) } - -let find_mutually_recursive_statements thms = - let n = List.length thms in - let inds = List.map (fun (id,(t,impls,annot)) -> - let (hyps,ccl) = decompose_prod_assum t in - let x = (id,(t,impls)) in - match annot with - (* Explicit fixpoint decreasing argument is given *) - | Some (Some (_,id),CStructRec) -> - let i,b,typ = lookup_rel_id id hyps 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.Finite && Option.is_empty b -> - [ind,x,i],[] - | _ -> - error "Decreasing argument is not an inductive assumption.") - (* Unsupported cases *) - | Some (_,(CWfRec _|CMeasureRec _)) -> - error "Only structural decreasing is supported for mutual statements." - (* 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_all_stack env Evd.empty c)) - (Global.env()) hyps in - let ind_hyps = - List.flatten (List.map_i (fun i decl -> - let t = RelDecl.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 && 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_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 - Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite -> - [ind,x,0] - | _ -> - [] in - ind_hyps,ind_ccl) thms in - let inds_hyps,ind_ccls = List.split inds in - let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> eq_mind kn kn' in - (* Check if all conclusions are coinductive in the same type *) - (* (degenerated cartesian product since there is at most one coind ccl) *) - let same_indccl = - List.cartesians_filter (fun hyp oks -> - if List.for_all (of_same_mutind hyp) oks - then Some (hyp::oks) else None) [] ind_ccls in - let ordered_same_indccl = - List.filter (List.for_all_i (fun i ((kn,j),_,_) -> Int.equal i j) 0) same_indccl in - (* Check if some hypotheses are inductive in the same type *) - let common_same_indhyp = - List.cartesians_filter (fun hyp oks -> - if List.for_all (of_same_mutind hyp) oks - then Some (hyp::oks) else None) [] inds_hyps in - let ordered_inds,finite,guard = - match ordered_same_indccl, common_same_indhyp with - | indccl::rest, _ -> - 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 Feedback.msg_info (str "Assuming mutual coinductive statements."); - flush_all (); - indccl, true, [] - | [], _::_ -> - let () = match same_indccl with - | ind :: _ -> - if List.distinct_f ind_ord (List.map pi1 ind) - then - if_verbose Feedback.msg_info - (strbrk - ("Coinductive statements do not follow the order of "^ - "definition, assuming the proof to be by induction.")); - flush_all () - | _ -> () - in - let possible_guards = List.map (List.map pi3) inds_hyps in - (* assume the largest indices as possible *) - List.last common_same_indhyp, false, possible_guards - | _, [] -> - error - ("Cannot find common (mutual) inductive premises or coinductive" ^ - " conclusions in the statements.") - in - (finite,guard,None), ordered_inds - -let look_for_possibly_mutual_statements = function - | [id,(t,impls,None)] -> - (* One non recursively proved theorem *) - None,[id,(t,impls)],None - | _::_ as thms -> - (* More than one statement and/or an explicit decreasing mark: *) - (* we look for a common inductive hyp or a common coinductive conclusion *) - let recguard,ordered_inds = find_mutually_recursive_statements thms in - let thms = List.map pi2 ordered_inds in - Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds) - | [] -> anomaly (Pp.str "Empty list of theorems.") - -(* Saving a goal *) - -let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook = - let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in - try - let const = adjust_guardness_conditions const do_guard in - let k = Kindops.logical_kind_of_goal_kind kind in - let l,r = match locality with - | Discharge when Lib.sections_are_opened () -> - let c = SectionLocalDef const in - let _ = declare_variable id (Lib.cwd(), c, k) in - (Local, VarRef id) - | Local | Global | Discharge -> - let local = match locality with - | Local | Discharge -> true - | Global -> false - in - let kn = - declare_constant ?export_seff id ~local (DefinitionEntry const, k) in - (locality, ConstRef kn) in - definition_message id; - Option.iter (Universes.register_universe_binders r) pl; - call_hook (fun exn -> exn) hook l r - 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" - -let compute_proof_name locality = function - | Some ((loc,id),pl) -> - (* We check existence here: it's a bit late at Qed time *) - if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || - locality == Global && Nametab.exists_cci (Lib.make_path_except_section id) - then - user_err ~loc (pr_id id ++ str " already exists."); - id, pl - | None -> - next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None - -let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) = - let t_i = norm t_i in - match body with - | None -> - (match locality with - | Discharge -> - let impl = false in (* copy values from Vernacentries *) - let k = IsAssumption Conjectural in - let c = SectionLocalAssum ((t_i,ctx),p,impl) in - let _ = declare_variable id (Lib.cwd(),c,k) in - (Discharge, VarRef id,imps) - | Local | Global -> - let k = IsAssumption Conjectural in - let local = match locality with - | Local -> true - | Global -> false - | Discharge -> assert false - in - let ctx = Univ.ContextSet.to_context ctx in - let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in - let kn = declare_constant id ~local decl in - (locality,ConstRef kn,imps)) - | Some body -> - let body = norm body in - let k = Kindops.logical_kind_of_goal_kind kind in - 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 - ~univs:(Univ.ContextSet.to_context ctx) body_i in - let c = SectionLocalDef const in - let _ = declare_variable id (Lib.cwd(), c, k) in - (Discharge,VarRef id,imps) - | Local | Global -> - let ctx = Univ.ContextSet.to_context ctx in - let local = match locality with - | Local -> true - | Global -> false - | Discharge -> assert false - in - let const = - Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i - in - let kn = declare_constant id ~local (DefinitionEntry const, k) in - (locality,ConstRef kn,imps) - -let save_hook = ref ignore -let set_save_hook f = save_hook := f - -let save_named ?export_seff proof = - let id,const,(cstrs,pl),do_guard,persistence,hook = proof in - save ?export_seff id const cstrs pl do_guard persistence hook - -let check_anonymity id save_ident = - if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then - error "This command can only be used for unnamed theorem." - -let save_anonymous ?export_seff proof save_ident = - let id,const,(cstrs,pl),do_guard,persistence,hook = proof in - check_anonymity id save_ident; - save ?export_seff save_ident const cstrs pl do_guard persistence hook - -let save_anonymous_with_strength ?export_seff proof kind save_ident = - let id,const,(cstrs,pl),do_guard,_,hook = proof in - check_anonymity id save_ident; - (* we consider that non opaque behaves as local for discharge *) - save ?export_seff save_ident const cstrs pl do_guard - (Global, const.const_entry_polymorphic, Proof kind) hook - -(* 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, _, _ -> warn_let_as_axiom id - in - let () = assumption_message id in - Option.iter (Universes.register_universe_binders (ConstRef kn)) pl; - call_hook (fun exn -> exn) hook Global (ConstRef kn) - -(* Starting a goal *) - -let start_hook = ref ignore -let set_start_hook = (:=) start_hook - - -let get_proof proof do_guard hook opacity = - let (id,(const,univs,persistence)) = - Pfedit.cook_this_proof proof - in - id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook - -let check_exist = - List.iter (fun (loc,id) -> - if not (Nametab.exists_cci (Lib.make_path id)) then - user_err ~loc (pr_id id ++ str " does not exist.") - ) - -let universe_proof_terminator compute_guard hook = - let open Proof_global in - make_terminator begin function - | Admitted (id,k,pe,(ctx,pl)) -> - admit (id,k,pe) pl (hook (Some ctx)) (); - Feedback.feedback Feedback.AddedAxiom - | Proved (opaque,idopt,proof) -> - let is_opaque, export_seff, exports = match opaque with - | Vernacexpr.Transparent -> false, true, [] - | Vernacexpr.Opaque None -> true, false, [] - | Vernacexpr.Opaque (Some l) -> true, true, l in - let proof = get_proof proof compute_guard - (hook (Some (fst proof.Proof_global.universes))) is_opaque in - begin match idopt with - | None -> save_named ~export_seff proof - | Some ((_,id),None) -> save_anonymous ~export_seff proof id - | Some ((_,id),Some kind) -> - 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 ?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 - | None -> initialize_named_context_for_proof () - in - !start_hook c; - Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator - -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 - | None -> initialize_named_context_for_proof () - in - !start_hook c; - Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator - -let rec_tac_initializer finite guard thms snl = - if finite then - match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with - | (id,_)::l -> Tactics.mutual_cofix id l 0 - | _ -> assert false - else - (* nl is dummy: it will be recomputed at Qed-time *) - let nl = match snl with - | None -> List.map succ (List.map List.last guard) - | Some nl -> nl - in match List.map2 (fun ((id,_),(t,_)) n -> (id,n,t)) thms nl with - | (id,n,_)::l -> Tactics.mutual_fix id n l 0 - | _ -> assert false - -let start_proof_with_initialization kind ctx recguard thms snl hook = - let intro_tac (_, (_, (ids, _))) = - Tacticals.New.tclMAP (function - | Name id -> Tactics.intro_mustbe_force id - | Anonymous -> Tactics.intro) (List.rev ids) in - let init_tac,guard = match recguard with - | Some (finite,guard,init_tac) -> - let rec_tac = rec_tac_initializer finite guard thms snl in - Some (match init_tac with - | None -> - if Flags.is_auto_intros () then - Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms) - else - rec_tac - | Some tacl -> - Tacticals.New.tclTHENS rec_tac - (if Flags.is_auto_intros () then - List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms - else - tacl)),guard - | None -> - let () = match thms with [_] -> () | _ -> assert false in - (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in - match thms with - | [] -> anomaly (Pp.str "No proof to start") - | ((id,pl),(t,(_,imps)))::other_thms -> - let hook ctx strength ref = - let ctx = match ctx with - | None -> Evd.empty_evar_universe_context - | Some ctx -> ctx - in - let other_thms_data = - if List.is_empty other_thms then [] else - (* there are several theorems defined mutually *) - 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 = 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 - List.iter (fun (strength,ref,imps) -> - maybe_declare_manual_implicits false ref imps; - 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 ?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 - | None -> Evd.from_env env0 - | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l)) - in - 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 - 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 RelDecl.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'), - guard))) - thms in - 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 *) - Evd.fix_undefined_variables evd - in - start_proof_with_initialization kind evd recguard thms snl 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 = - let open Proof_global in - match proof with - | Some ({ id; entries; persistence = k; universes }, _) -> - if List.length entries <> 1 then - error "Admitted does not support multiple statements"; - let { const_entry_secctx; const_entry_type } = List.hd entries in - if const_entry_type = None then - error "Admitted requires an explicit statement"; - let typ = Option.get const_entry_type in - let ctx = Evd.evar_context_universe_context (fst universes) in - 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, _univs = - Proof_global.return_proof ~allow_partial:true () in - let sec_vars = - 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 - let ids_typ = Environ.global_vars_set env typ in - let ids_def = Environ.global_vars_set env pproof in - Some (Environ.keep_hyps env (Idset.union ids_typ ids_def)) - | _ -> None in - let names = Pfedit.get_universe_binders () 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.apply_terminator (Proof_global.get_terminator ()) pe - | Vernacexpr.Proved (is_opaque,idopt) -> - let (proof_obj,terminator) = - match proof with - | None -> - Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x) - | Some proof -> proof - in - (* if the proof is given explicitly, nothing has to be deleted *) - if Option.is_empty proof then Pfedit.delete_current_proof (); - Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj))) - -(* Miscellaneous *) - -let get_current_context () = - Pfedit.get_current_context () - diff --git a/stm/lemmas.mli b/stm/lemmas.mli deleted file mode 100644 index 39c089be9f..0000000000 --- a/stm/lemmas.mli +++ /dev/null @@ -1,69 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Globnames.global_reference -> 'a) -> 'a declaration_hook - -val call_hook : - Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a - -(** A hook start_proof calls on the type of the definition being started *) -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 : - ?inference_hook:Pretyping.inference_hook -> - goal_kind -> Vernacexpr.proof_expr list -> - unit declaration_hook -> unit - -val start_proof_with_initialization : - goal_kind -> Evd.evar_map -> - (bool * lemma_possible_guards * unit Proofview.tactic list option) option -> - ((Id.t * universe_binders option) * - (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 - -(** {6 ... } *) - -(** A hook the next three functions pass to cook_proof *) -val set_save_hook : (Proof.proof -> unit) -> unit - -val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit - - -(** [get_current_context ()] returns the evar context and env of the - current open proof if any, otherwise returns the empty evar context - and the current global env *) - -val get_current_context : unit -> Evd.evar_map * Environ.env diff --git a/stm/stm.ml b/stm/stm.ml index 6f34c8dbc3..be3e841cb9 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -24,11 +24,13 @@ open Ppvernac open Vernac_classifier open Feedback +let execution_error state_id loc msg = + feedback ~id:(State state_id) + (Message (Error, Some loc, pp_to_richpp msg)) + module Hooks = struct let process_error, process_error_hook = Hook.make () -let interp, interp_hook = Hook.make () -let with_fail, with_fail_hook = Hook.make () let state_computed, state_computed_hook = Hook.make ~default:(fun state_id ~in_cache -> @@ -48,10 +50,6 @@ let parse_error, parse_error_hook = Hook.make ~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 ~id:(State state_id) (Message(Error, Some loc, pp_to_richpp msg))) () - let unreachable_state, unreachable_state_hook = Hook.make ~default:(fun _ _ -> ()) () @@ -106,24 +104,36 @@ let may_pierce_opaque = function | _ -> false (* Wrapper for Vernacentries.interp to set the feedback id *) -let vernac_interp ?proof id ?route { verbose; loc; expr } = - let rec internal_command = function - | VernacResetName _ | VernacResetInitial | VernacBack _ - | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ - | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true - | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> internal_command e - | _ -> false in - if internal_command expr then begin +(* It is currently called 19 times, this number should be certainly + reduced... *) +let stm_vernac_interp ?proof id ?route { verbose; loc; expr } = + (* The Stm will gain the capability to interpret commmads affecting + the whole document state, such as backtrack, etc... so we start + to design the stm command interpreter now *) + set_id_for_feedback ?route (State id); + Aux_file.record_in_aux_set_at loc; + (* We need to check if a command should be filtered from + * vernac_entries, as it cannot handle it. This should go away in + * future refactorings. + *) + let rec is_filtered_command = function + | VernacResetName _ | VernacResetInitial | VernacBack _ + | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ + | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true + | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> is_filtered_command e + | _ -> false + in + let aux_interp cmd = + if is_filtered_command cmd then prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr)) - end else begin - set_id_for_feedback ?route (State id); - Aux_file.record_in_aux_set_at loc; + else match cmd with + | expr -> prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr)); - try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr)) + try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr) with e -> let e = CErrors.push e in iraise Hooks.(call_process_error_once e) - end + in aux_interp expr (* Wrapper for Vernac.parse_sentence to set the feedback id *) let indentation_of_string s = @@ -860,7 +870,7 @@ end = struct (* {{{ *) | 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))); + execution_error id loc (iprint (e, info)); (e, Stateid.add info ~valid id) let same_env { system = s1 } { system = s2 } = @@ -910,7 +920,6 @@ end = struct (* {{{ *) end (* }}} *) - (****************************** CRUFT *****************************************) (******************************************************************************) @@ -1287,7 +1296,7 @@ end = struct (* {{{ *) let info = Stateid.add ~valid:start Exninfo.null start in let e = (RemoteException (strbrk s), info) in t_assign (`Exn e); - Hooks.(call execution_error start Loc.ghost (strbrk s)); + execution_error start Loc.ghost (strbrk s); feedback (InProgress ~-1) let build_proof_here ~drop_pt (id,valid) loc eop = @@ -1750,7 +1759,7 @@ end = struct (* {{{ *) | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e | VernacFail e -> find time true e | _ -> e, time, fail in find false false e in - Hooks.call Hooks.with_fail fail (fun () -> + Vernacentries.with_fail fail (fun () -> (if time then System.with_time false else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> Proof_global.with_current_proof (fun _ p -> @@ -2946,12 +2955,8 @@ let show_script ?proof () = let state_computed_hook = Hooks.state_computed_hook let state_ready_hook = Hooks.state_ready_hook let parse_error_hook = Hooks.parse_error_hook -let execution_error_hook = Hooks.execution_error_hook let forward_feedback_hook = Hooks.forward_feedback_hook let process_error_hook = Hooks.process_error_hook -let interp_hook = Hooks.interp_hook -let with_fail_hook = Hooks.with_fail_hook let unreachable_state_hook = Hooks.unreachable_state_hook -let get_fix_exn () = !State.fix_exn_ref let tactic_being_run_hook = Hooks.tactic_being_run_hook (* vim:set foldmethod=marker: *) diff --git a/stm/stm.mli b/stm/stm.mli index b8a2a38596..36341a5d51 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -184,7 +184,6 @@ val register_proof_block_delimiter : val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t val parse_error_hook : (Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t -val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t (* ready means that master has it at hand *) val state_ready_hook : (Stateid.t -> unit) Hook.t @@ -218,7 +217,3 @@ val show_script : ?proof:Proof_global.closed_proof -> unit -> unit (* 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 -val with_fail_hook : (bool -> (unit -> unit) -> unit) Hook.t -val get_fix_exn : unit -> (Exninfo.iexn -> Exninfo.iexn) diff --git a/stm/stm.mllib b/stm/stm.mllib index 939ee187ae..4b254e8113 100644 --- a/stm/stm.mllib +++ b/stm/stm.mllib @@ -4,7 +4,6 @@ Vcs TQueue WorkerPool Vernac_classifier -Lemmas CoqworkmgrApi AsyncTaskQueue Stm -- cgit v1.2.3 From fc6e78be83cef6e9b249ca146ef749ba90eb802c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 23 Jan 2017 22:21:11 +0100 Subject: [stm] Reenable Show Script command. We extend `Stm.vernac_interp` so it can handle the commands it should by level. This reenables `Show Script` handling, and this interpretation function should handle more commands in the future such as Load. However note that we must first refactor the parsing state handling a bit and remove the legacy `Stm.interp` before that. --- stm/stm.ml | 274 +++++++++++++++++++++++++++++++----------------------------- stm/stm.mli | 1 - 2 files changed, 140 insertions(+), 135 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index be3e841cb9..1cd6209aa4 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -103,38 +103,6 @@ let may_pierce_opaque = function | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true | _ -> false -(* Wrapper for Vernacentries.interp to set the feedback id *) -(* It is currently called 19 times, this number should be certainly - reduced... *) -let stm_vernac_interp ?proof id ?route { verbose; loc; expr } = - (* The Stm will gain the capability to interpret commmads affecting - the whole document state, such as backtrack, etc... so we start - to design the stm command interpreter now *) - set_id_for_feedback ?route (State id); - Aux_file.record_in_aux_set_at loc; - (* We need to check if a command should be filtered from - * vernac_entries, as it cannot handle it. This should go away in - * future refactorings. - *) - let rec is_filtered_command = function - | VernacResetName _ | VernacResetInitial | VernacBack _ - | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ - | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true - | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> is_filtered_command e - | _ -> false - in - let aux_interp cmd = - if is_filtered_command cmd then - prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr)) - else match cmd with - | expr -> - prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr)); - try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr) - with e -> - let e = CErrors.push e in - iraise Hooks.(call_process_error_once e) - in aux_interp expr - (* Wrapper for Vernac.parse_sentence to set the feedback id *) let indentation_of_string s = let len = String.length s in @@ -920,6 +888,127 @@ end = struct (* {{{ *) end (* }}} *) +(* indentation code for Show Script, initially contributed + * by D. de Rauglaudre. Should be moved away. + *) + +module ShowScript = struct + +let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) = + (* ng1 : number of goals remaining at the current level (before cmd) + ngl1 : stack of previous levels with their remaining goals + ng : number of goals after the execution of cmd + beginend : special indentation stack for { } *) + let ngprev = List.fold_left (+) ng1 ngl1 in + let new_ngl = + if ng > ngprev then + (* We've branched *) + (ng - ngprev + 1, ng1 - 1 :: ngl1) + else if ng < ngprev then + (* A subgoal have been solved. Let's compute the new current level + by discarding all levels with 0 remaining goals. *) + let rec loop = function + | (0, ng2::ngl2) -> loop (ng2,ngl2) + | p -> p + in loop (ng1-1, ngl1) + else + (* Standard case, same goal number as before *) + (ng1, ngl1) + in + (* When a subgoal have been solved, separate this block by an empty line *) + let new_nl = (ng < ngprev) + in + (* Indentation depth *) + let ind = List.length ngl1 + in + (* Some special handling of bullets and { }, to get a nicer display *) + let pred n = max 0 (n-1) in + let ind, nl, new_beginend = match cmd with + | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend + | VernacEndSubproof -> List.hd beginend, false, List.tl beginend + | VernacBullet _ -> pred ind, nl, beginend + | _ -> ind, nl, beginend + in + let pp = + (if nl then fnl () else mt ()) ++ + (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd)) + in + (new_ngl, new_nl, new_beginend, pp :: ppl) + +let get_script prf = + let branch, test = + match prf with + | None -> VCS.Branch.master, fun _ -> true + | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in + let rec find acc id = + if Stateid.equal id Stateid.initial || + Stateid.equal id Stateid.dummy then acc else + let view = VCS.visit id in + match view.step with + | `Fork((_,_,_,ns), _) when test ns -> acc + | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof + | `Sideff (`Ast (x,_)) -> + find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next + | `Sideff (`Id id) -> find acc id + | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *) + find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next + | `Cmd _ -> find acc view.next + | `Alias (id,_) -> find acc id + | `Fork _ -> find acc view.next + in + find [] (VCS.get_branch_pos branch) + +let show_script ?proof () = + try + let prf = + try match proof with + | None -> Some (Pfedit.get_current_proof_name ()) + | Some (p,_) -> Some (p.Proof_global.id) + with Proof_global.NoCurrentProof -> None + in + let cmds = get_script prf in + let _,_,_,indented_cmds = + List.fold_left indent_script_item ((1,[]),false,[],[]) cmds + in + let indented_cmds = List.rev (indented_cmds) in + msg_notice (v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds)) + with Vcs_aux.Expired -> () + +end + +(* Wrapper for Vernacentries.interp to set the feedback id *) +(* It is currently called 19 times, this number should be certainly + reduced... *) +let stm_vernac_interp ?proof id ?route { verbose; loc; expr } = + (* The Stm will gain the capability to interpret commmads affecting + the whole document state, such as backtrack, etc... so we start + to design the stm command interpreter now *) + set_id_for_feedback ?route (State id); + Aux_file.record_in_aux_set_at loc; + (* We need to check if a command should be filtered from + * vernac_entries, as it cannot handle it. This should go away in + * future refactorings. + *) + let rec is_filtered_command = function + | VernacResetName _ | VernacResetInitial | VernacBack _ + | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ + | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true + | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> is_filtered_command e + | _ -> false + in + let aux_interp cmd = + if is_filtered_command cmd then + prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr)) + else match cmd with + | VernacShow ShowScript -> ShowScript.show_script () + | expr -> + prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr)); + try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr) + with e -> + let e = CErrors.push e in + iraise Hooks.(call_process_error_once e) + in aux_interp expr + (****************************** CRUFT *****************************************) (******************************************************************************) @@ -1330,7 +1419,7 @@ end = struct (* {{{ *) Proof_global.close_future_proof stop (Future.from_val ~fix_exn p) in let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in - vernac_interp stop + stm_vernac_interp stop ~proof:(pobject, terminator) { verbose = false; loc; indentation = 0; strlen = 0; expr = (VernacEndProof (Proved (Opaque None,None))) }) in @@ -1472,7 +1561,7 @@ end = struct (* {{{ *) (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) Reach.known_state ~cache:`No start; - vernac_interp stop ~proof + stm_vernac_interp stop ~proof { verbose = false; loc; indentation = 0; strlen = 0; expr = (VernacEndProof (Proved (Opaque None,None))) }; `OK proof @@ -1723,7 +1812,7 @@ end = struct (* {{{ *) else begin 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; + stm_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 -> RespNoProgress @@ -1852,7 +1941,7 @@ end = struct (* {{{ *) VCS.print (); Reach.known_state ~cache:`No r_where; try - vernac_interp r_for { r_what with verbose = true }; + stm_vernac_interp r_for { r_what with verbose = true }; feedback ~id:(State r_for) Processed with e when CErrors.noncritical e -> let e = CErrors.push e in @@ -2061,7 +2150,7 @@ let known_state ?(redefine_qed=false) ~cache id = 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 { + Option.iter (fun expr -> stm_vernac_interp id { verbose = true; loc = Loc.ghost; expr; indentation = 0; strlen = 0 }) recovery_command @@ -2140,24 +2229,24 @@ let known_state ?(redefine_qed=false) ~cache id = resilient_tactic id cblock (fun () -> reach view.next; Hooks.(call tactic_being_run true); - vernac_interp id x; + stm_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; + stm_vernac_interp id x; if eff then update_global_env () ), (if eff then `Yes else cache), true | `Fork ((x,_,_,_), None) -> (fun () -> resilient_command reach view.next; - vernac_interp id x; + stm_vernac_interp id x; wall_clock_last_fork := Unix.gettimeofday () ), `Yes, true | `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *) reach ~cache:`Shallow prev; reach view.next; - (try vernac_interp id x; + (try stm_vernac_interp id x; with e when CErrors.noncritical e -> let (e, info) = CErrors.push e in let info = Stateid.add info ~valid:prev id in @@ -2207,14 +2296,14 @@ let known_state ?(redefine_qed=false) ~cache id = Proof_global.close_future_proof ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; - vernac_interp id ~proof x; + stm_vernac_interp id ~proof x; feedback ~id:(State id) Incomplete | { VCS.kind = `Master }, _ -> assert false end; Proof_global.discard_all () ), (if redefine_qed then `No else `Yes), true | `Sync (name, _, `Immediate) -> (fun () -> - reach eop; vernac_interp id x; Proof_global.discard_all () + reach eop; stm_vernac_interp id x; Proof_global.discard_all () ), `Yes, true | `Sync (name, pua, reason) -> (fun () -> log_processing_sync id name reason; @@ -2235,7 +2324,7 @@ let known_state ?(redefine_qed=false) ~cache id = if keep != VtKeepAsAxiom then reach view.next; let wall_clock2 = Unix.gettimeofday () in - vernac_interp id ?proof x; + stm_vernac_interp id ?proof x; let wall_clock3 = Unix.gettimeofday () in Aux_file.record_in_aux_at x.loc "proof_check_time" (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2)); @@ -2251,7 +2340,7 @@ let known_state ?(redefine_qed=false) ~cache id = in aux (collect_proof keep (view.next, x) brname brinfo eop) | `Sideff (`Ast (x,_)) -> (fun () -> - reach view.next; vernac_interp id x; update_global_env () + reach view.next; stm_vernac_interp id x; update_global_env () ), cache, true | `Sideff (`Id origin) -> (fun () -> reach view.next; @@ -2439,7 +2528,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty " classified as: " ^ string_of_vernac_classification c); match c with (* PG stuff *) - | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok + | VtStm(VtPG,false), VtNow -> stm_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 -> join (); `Ok @@ -2483,13 +2572,13 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty (* Query *) | VtQuery (false,(report_id,route)), VtNow when tty = true -> finish (); - (try Future.purify (vernac_interp report_id ~route) + (try Future.purify (stm_vernac_interp report_id ~route) {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 + (try stm_vernac_interp report_id ~route x with e -> let e = CErrors.push e in iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok @@ -2562,7 +2651,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty (* Side effect on all branches *) | VtUnknown, _ when expr = VernacToplevelControl Drop -> - vernac_interp (VCS.get_branch_pos head) x; `Ok + stm_vernac_interp (VCS.get_branch_pos head) x; `Ok | VtSideff l, w -> let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in @@ -2588,7 +2677,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty VCS.checkout VCS.Branch.master; let mid = VCS.get_branch_pos VCS.Branch.master in Reach.known_state ~cache:(interactive ()) mid; - vernac_interp id x; + stm_vernac_interp id x; (* Vernac x may or may not start a proof *) if not in_proof && Proof_global.there_are_pending_proofs () then begin @@ -2618,7 +2707,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty begin match expr with | VernacStm (PGLast _) -> if not (VCS.Branch.equal head VCS.Branch.master) then - vernac_interp Stateid.dummy + stm_vernac_interp Stateid.dummy { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0; expr = VernacShow (ShowGoal OpenSubgoals) } | _ -> () @@ -2868,89 +2957,6 @@ let get_all_proof_names () = let get_current_proof_name () = Option.map unmangle (proofname (VCS.current_branch ())) -let get_script prf = - let branch, test = - match prf with - | None -> VCS.Branch.master, fun _ -> true - | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in - let rec find acc id = - if Stateid.equal id Stateid.initial || - Stateid.equal id Stateid.dummy then acc else - let view = VCS.visit id in - match view.step with - | `Fork((_,_,_,ns), _) when test ns -> acc - | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof - | `Sideff (`Ast (x,_)) -> - find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next - | `Sideff (`Id id) -> find acc id - | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *) - find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next - | `Cmd _ -> find acc view.next - | `Alias (id,_) -> find acc id - | `Fork _ -> find acc view.next - in - find [] (VCS.get_branch_pos branch) - -(* indentation code for Show Script, initially contributed - by D. de Rauglaudre *) - -let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) = - (* ng1 : number of goals remaining at the current level (before cmd) - ngl1 : stack of previous levels with their remaining goals - ng : number of goals after the execution of cmd - beginend : special indentation stack for { } *) - let ngprev = List.fold_left (+) ng1 ngl1 in - let new_ngl = - if ng > ngprev then - (* We've branched *) - (ng - ngprev + 1, ng1 - 1 :: ngl1) - else if ng < ngprev then - (* A subgoal have been solved. Let's compute the new current level - by discarding all levels with 0 remaining goals. *) - let rec loop = function - | (0, ng2::ngl2) -> loop (ng2,ngl2) - | p -> p - in loop (ng1-1, ngl1) - else - (* Standard case, same goal number as before *) - (ng1, ngl1) - in - (* When a subgoal have been solved, separate this block by an empty line *) - let new_nl = (ng < ngprev) - in - (* Indentation depth *) - let ind = List.length ngl1 - in - (* Some special handling of bullets and { }, to get a nicer display *) - let pred n = max 0 (n-1) in - let ind, nl, new_beginend = match cmd with - | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend - | VernacEndSubproof -> List.hd beginend, false, List.tl beginend - | VernacBullet _ -> pred ind, nl, beginend - | _ -> ind, nl, beginend - in - let pp = - (if nl then fnl () else mt ()) ++ - (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd)) - in - (new_ngl, new_nl, new_beginend, pp :: ppl) - -let show_script ?proof () = - try - let prf = - try match proof with - | None -> Some (Pfedit.get_current_proof_name ()) - | Some (p,_) -> Some (p.Proof_global.id) - with Proof_global.NoCurrentProof -> None - in - let cmds = get_script prf in - let _,_,_,indented_cmds = - List.fold_left indent_script_item ((1,[]),false,[],[]) cmds - in - let indented_cmds = List.rev (indented_cmds) in - msg_notice (v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds)) - with Vcs_aux.Expired -> () - (* Export hooks *) let state_computed_hook = Hooks.state_computed_hook let state_ready_hook = Hooks.state_ready_hook diff --git a/stm/stm.mli b/stm/stm.mli index 36341a5d51..5d0d05d411 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -213,7 +213,6 @@ val interp : bool -> vernac_expr located -> unit val current_proof_depth : unit -> int 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 (* Hooks to be set by other Coq components in order to break file cycles *) val process_error_hook : Future.fix_exn Hook.t -- cgit v1.2.3 From 4db82417bdda1f9b0c7ea6ba9f6d71c03cc07eba Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 23 Jan 2017 22:48:38 +0100 Subject: [stm] Remove unused legacy stm interface. --- stm/stm.ml | 3 --- stm/stm.mli | 1 - 2 files changed, 4 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 1cd6209aa4..fd1cefa8d1 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2954,9 +2954,6 @@ let proofname b = match VCS.get_branch b with let get_all_proof_names () = List.map unmangle (List.map_filter proofname (VCS.branches ())) -let get_current_proof_name () = - Option.map unmangle (proofname (VCS.current_branch ())) - (* Export hooks *) let state_computed_hook = Hooks.state_computed_hook let state_ready_hook = Hooks.state_ready_hook diff --git a/stm/stm.mli b/stm/stm.mli index 5d0d05d411..0f0a3c4e13 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -212,7 +212,6 @@ val interp : bool -> vernac_expr located -> unit (* Queries for backward compatibility *) val current_proof_depth : unit -> int val get_all_proof_names : unit -> Id.t list -val get_current_proof_name : unit -> Id.t option (* Hooks to be set by other Coq components in order to break file cycles *) val process_error_hook : Future.fix_exn Hook.t -- cgit v1.2.3 From 888d4be3ea2a45cff416fd8896276cfa8fc00518 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 10 Feb 2017 11:07:10 +0100 Subject: Make Obligations see fix_exn --- stm/stm.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index fd1cefa8d1..e698d1c72e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2961,5 +2961,6 @@ let parse_error_hook = Hooks.parse_error_hook let forward_feedback_hook = Hooks.forward_feedback_hook let process_error_hook = Hooks.process_error_hook let unreachable_state_hook = Hooks.unreachable_state_hook +let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref) let tactic_being_run_hook = Hooks.tactic_being_run_hook (* vim:set foldmethod=marker: *) -- cgit v1.2.3 From 3502cc7c3bbad154dbfe76558d411d2c76109668 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 5 Mar 2017 17:30:03 +0100 Subject: [future] Remove unused parameter greedy. It was always set to `greedy:true`. --- stm/stm.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index e698d1c72e..e56db4090a 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1618,9 +1618,9 @@ end = struct (* {{{ *) Future.from_val (Option.get (Global.body_of_constant_body c)) in let uc = Future.chain - ~greedy:true ~pure:true uc Univ.hcons_universe_context_set in - let pr = Future.chain ~greedy:true ~pure:true pr discharge in - let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in + ~pure:true uc Univ.hcons_universe_context_set in + let pr = Future.chain ~pure:true pr discharge in + let pr = Future.chain ~pure:true pr Constr.hcons in Future.sink pr; let extra = Future.join uc in u.(bucket) <- uc; -- cgit v1.2.3 From 5b8bfee9d80e550cd81e326ec134430b2a4797a5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 29 Sep 2016 16:30:21 +0200 Subject: [pp] Make feedback the only logging mechanism. Previously to this patch, Coq featured to distinct logging paths: the console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format` module, and the `Feedback` one, intended to encapsulate message inside a more general, GUI-based feedback protocol. This patch removes the legacy logging path and makes feedback canonical. Thus, the core of Coq has no dependency on console code anymore. Additionally, this patch resolves the duplication of "document" formats present in the same situation. The original console-based printing code relied on an opaque datatype `std_ppcmds`, (mostly a reification of `Format`'s format strings) that could be then rendered to the console. However, the feedback path couldn't reuse this type due to its opaque nature. The first versions just embedded rending of `std_ppcmds` to a string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was introduced. The idea for this type was to be serializable, however it brought several problems: it didn't have proper document manipulation operations, its format was overly verbose and didn't preserve the full layout, and it still relied on `Format` for generation, making client-side rendering difficult. We thus follow the plan outlined in CEP#9, that is to say, we take a public and refactored version of `std_ppcmds` as the canonical "document type", and move feedback to be over there. The toplevel now is implemented as a feedback listener and has ownership of the console. `richpp` is now IDE-specific, and only used for legacy rendering. It could go away in future versions. `std_ppcmds` carries strictly more information and is friendlier to client-side rendering and display control. Thus, the new panorama is: - `Feedback` has become a very module for event dispatching. - `Pp` contains a target-independent box-based document format. It also contains the `Format`-based renderer. - All console access lives in `toplevel`, with console handlers private to coqtop. _NOTE_: After this patch, many printing parameters such as printing width or depth should be set client-side. This works better IMO, clients don't need to notify Coq about resizing anywmore. Indeed, for box-based capable backends such as HTML or LaTeX, the UI can directly render and let the engine perform the word breaking work. _NOTE_: Many messages could benefit from new features of the output format, however we have chosen not to alter them to preserve output. A Future commits will move console tag handling in `Pp_style` to `toplevel/`, where it logically belongs. The only change with regards to printing is that the "Error:" header was added to console output in several different positions, we have removed some of this duplication, now error messages should be a bit more consistent. --- stm/asyncTaskQueue.ml | 12 ++---------- stm/stm.ml | 10 +++------- 2 files changed, 5 insertions(+), 17 deletions(-) (limited to 'stm') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 8acc3c233a..28548ecee9 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -298,18 +298,11 @@ 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 pp_pid pp = Pp.(str (System.process_id () ^ " ") ++ pp) let debug_with_pid = Feedback.(function | { contents = Message(Debug, loc, pp) } as fb -> - { fb with contents = Message(Debug,loc,pp_pid pp) } + { fb with contents = Message(Debug,loc, pp_pid pp) } | x -> x) let main_loop () = @@ -317,7 +310,6 @@ module Make(T : Task) = struct let slave_feeder oc fb = 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; diff --git a/stm/stm.ml b/stm/stm.ml index e56db4090a..75872d633f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -11,10 +11,6 @@ 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 () -(* 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 CErrors open Pp @@ -26,7 +22,7 @@ open Feedback let execution_error state_id loc msg = feedback ~id:(State state_id) - (Message (Error, Some loc, pp_to_richpp msg)) + (Message (Error, Some loc, msg)) module Hooks = struct @@ -48,7 +44,7 @@ let forward_feedback, forward_feedback_hook = let parse_error, parse_error_hook = Hook.make ~default:(fun id loc msg -> - feedback ~id (Message(Error, Some loc, pp_to_richpp msg))) () + feedback ~id (Message(Error, Some loc, msg))) () let unreachable_state, unreachable_state_hook = Hook.make ~default:(fun _ _ -> ()) () @@ -1945,7 +1941,7 @@ end = struct (* {{{ *) 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 + let msg = 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) -- cgit v1.2.3 From 3b3d5937939ac8dc4f152d61391630e62bb0b2e5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 7 Dec 2016 12:12:54 +0100 Subject: [pp] [ide] Minor cleanups in pp code. - We avoid unnecessary use of Pp -> string conversion functions. and the creation of intermediate buffers on logging. - We rename local functions that share the name with the Coq stdlib, this is usually dangerous as if the normal function is removed, code may pick up the one in the stdlib, with different semantics. --- stm/asyncTaskQueue.ml | 25 +++++++++++----------- stm/stm.ml | 58 +++++++++++++++++++++++++-------------------------- 2 files changed, 41 insertions(+), 42 deletions(-) (limited to 'stm') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 28548ecee9..1254919880 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -10,9 +10,9 @@ open CErrors open Pp open Util -let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr +let stm_pr_err pp = Format.eprintf "%s] @[%a@]%!\n" (System.process_id ()) Pp.pp_with pp -let prerr_endline s = if !Flags.debug then begin pr_err s end else () +let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else () type 'a worker_status = [ `Fresh | `Old of 'a ] @@ -147,23 +147,23 @@ module Make(T : Task) = struct let stop_waiting = ref false in let expiration_date = ref (ref false) in let pick_task () = - prerr_endline "waiting for a task"; + stm_prerr_endline "waiting for a task"; let pick age (t, c) = not !c && T.task_match age t in let task, task_expiration = TQueue.pop ~picky:(pick !worker_age) ~destroy:stop_waiting queue in expiration_date := task_expiration; last_task := Some task; - prerr_endline ("got task: "^T.name_of_task task); + stm_prerr_endline ("got task: " ^ T.name_of_task task); task in let add_tasks l = List.iter (fun t -> TQueue.push queue (t,!expiration_date)) l in let get_exec_token () = ignore(CoqworkmgrApi.get 1); got_token := true; - prerr_endline ("got execution token") in + stm_prerr_endline ("got execution token") in let kill proc = Worker.kill proc; - prerr_endline ("Worker exited: " ^ + stm_prerr_endline ("Worker exited: " ^ match Worker.wait proc with | Unix.WEXITED 0x400 -> "exit code unavailable" | Unix.WEXITED i -> Printf.sprintf "exit(%d)" i @@ -196,7 +196,7 @@ module Make(T : Task) = struct report_status ~id "Idle"; let task = pick_task () in match T.request_of_task !worker_age task with - | None -> prerr_endline ("Task expired: " ^ T.name_of_task task) + | None -> stm_prerr_endline ("Task expired: " ^ T.name_of_task task) | Some req -> try get_exec_token (); @@ -222,8 +222,7 @@ module Make(T : Task) = struct raise e (* we pass the exception to the external handler *) | MarshalError s -> T.on_marshal_error s task; raise Die | e -> - pr_err ("Uncaught exception in worker manager: "^ - string_of_ppcmds (print e)); + stm_pr_err Pp.(seq [str "Uncaught exception in worker manager: "; print e]); flush_all (); raise Die done with | (Die | TQueue.BeingDestroyed) -> @@ -261,7 +260,7 @@ module Make(T : Task) = struct let broadcast { queue } = TQueue.broadcast queue let enqueue_task { queue; active } (t, _ as item) = - prerr_endline ("Enqueue task "^T.name_of_task t); + stm_prerr_endline ("Enqueue task "^T.name_of_task t); TQueue.push queue item let cancel_worker { active } n = Pool.cancel n active @@ -329,11 +328,11 @@ module Make(T : Task) = struct CEphemeron.clear () with | MarshalError s -> - pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2 + stm_pr_err Pp.(prlist str ["Fatal marshal error: "; s]); flush_all (); exit 2 | End_of_file -> - prerr_endline "connection lost"; flush_all (); exit 2 + stm_prerr_endline "connection lost"; flush_all (); exit 2 | e -> - pr_err ("Slave: critical exception: " ^ Pp.string_of_ppcmds (print e)); + stm_pr_err Pp.(seq [str "Slave: critical exception: "; print e]); flush_all (); exit 1 done diff --git a/stm/stm.ml b/stm/stm.ml index 75872d633f..ee142b2930 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr +let stm_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 stm_prerr_endline s = if false then begin stm_pr_err (s ()) end else () +let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else () open Vernacexpr open CErrors @@ -540,7 +540,7 @@ 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 (fun () -> "mode:" ^ mode); + stm_prerr_endline (fun () -> "mode:" ^ mode); Proof_global.activate_proof_mode mode with Failure _ -> checkout Branch.master; @@ -852,7 +852,7 @@ end = struct (* {{{ *) if is_cached id && not redefine then anomaly (str"defining state "++str str_id++str" twice"); try - prerr_endline (fun () -> "defining "^str_id^" (cache="^ + stm_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; @@ -860,7 +860,7 @@ 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 (fun () -> "setting cur id to "^str_id); + stm_prerr_endline (fun () -> "setting cur id to "^str_id); cur_id := id; if feedback_processed then Hooks.(call state_computed id ~in_cache:false); @@ -994,11 +994,11 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } = in let aux_interp cmd = if is_filtered_command cmd then - prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr)) + stm_prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr)) else match cmd with | VernacShow ShowScript -> ShowScript.show_script () | expr -> - prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr)); + stm_prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr)); try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr) with e -> let e = CErrors.push e in @@ -1431,8 +1431,8 @@ end = struct (* {{{ *) | Some (safe, err) -> err, safe | None -> Stateid.dummy, Stateid.dummy in let e_msg = iprint (e, info) in - prerr_endline (fun () -> "failed with the following exception:"); - prerr_endline (fun () -> string_of_ppcmds e_msg); + stm_prerr_endline (fun () -> "failed with the following exception:"); + stm_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 } @@ -1697,7 +1697,7 @@ end = struct (* {{{ *) | Some (ReqBuildProof (r, b, _)) -> Some(r, b) | _ -> None) tasks in - prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs)); + stm_prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs)); reqs let reset_task_queue () = TaskQueue.clear (Option.get !queue) @@ -1781,7 +1781,7 @@ end = struct (* {{{ *) `Stay ((),[]) let on_marshal_error err { t_name } = - pr_err ("Fatal marshal error: " ^ t_name ); + stm_pr_err ("Fatal marshal error: " ^ t_name ); flush_all (); exit 1 let on_task_cancellation_or_expiration_or_slave_death = function @@ -1880,7 +1880,7 @@ end = struct (* {{{ *) let open Notations in try let pt, uc = Future.join f in - prerr_endline (fun () -> string_of_ppcmds(hov 0 ( + stm_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))); @@ -1925,7 +1925,7 @@ end = struct (* {{{ *) let use_response _ _ _ = `End let on_marshal_error _ _ = - pr_err ("Fatal marshal error in query"); + stm_pr_err ("Fatal marshal error in query"); flush_all (); exit 1 let on_task_cancellation_or_expiration_or_slave_death _ = () @@ -2000,7 +2000,7 @@ let warn_deprecated_nested_proofs = "stop working in a future Coq version")) let collect_proof keep cur hd brkind id = - prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); + stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); let no_name = "" in let name = function | [] -> no_name @@ -2100,7 +2100,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 (fun () -> "STM: " ^ s) +let log_string s = stm_prerr_debug (fun () -> "STM: " ^ s) let log_processing_async id name = log_string Printf.(sprintf "%s: proof %s: asynch" (Stateid.to_string id) name ) @@ -2187,16 +2187,16 @@ let known_state ?(redefine_qed=false) ~cache id = Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env () in let rec pure_cherry_pick_non_pstate safe_id id = Future.purify (fun id -> - prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id); + stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id); reach ~safe_id id; cherry_pick_non_pstate ()) id (* traverses the dag backward from nodes being already calculated *) and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id = - prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id); + stm_prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id); if not redefine_qed && State.is_cached ~cache id then begin Hooks.(call state_computed id ~in_cache:true); - prerr_endline (fun () -> "reached (cache)"); + stm_prerr_endline (fun () -> "reached (cache)"); State.install_cached id end else let step, cache_step, feedback_processed = @@ -2348,7 +2348,7 @@ let known_state ?(redefine_qed=false) ~cache id = else cache_step in State.define ?safe_id ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id; - prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in + stm_prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in reach ~redefine_qed id end (* }}} *) @@ -2363,7 +2363,7 @@ let init () = Backtrack.record (); Slaves.init (); if Flags.async_proofs_is_master () then begin - prerr_endline (fun () -> "Initializing workers"); + stm_prerr_endline (fun () -> "Initializing workers"); Query.init (); let opts = match !Flags.async_proofs_private_flags with | None -> [] @@ -2415,9 +2415,9 @@ let rec join_admitted_proofs id = let join () = finish (); wait (); - prerr_endline (fun () -> "Joining the environment"); + stm_prerr_endline (fun () -> "Joining the environment"); Global.join_safe_environment (); - prerr_endline (fun () -> "Joining Admitted proofs"); + stm_prerr_endline (fun () -> "Joining Admitted proofs"); join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ())); VCS.print (); VCS.print () @@ -2491,7 +2491,7 @@ let handle_failure (e, info) vcs tty = anomaly(str"error with no safe_id attached:" ++ spc() ++ CErrors.iprint_no_report (e, info)) | Some (safe_id, id) -> - prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); + stm_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 *) @@ -2514,13 +2514,13 @@ let reset_task_queue = Slaves.reset_task_queue (* Document building *) let process_transaction ?(newtip=Stateid.fresh ()) ~tty ({ verbose; loc; expr } as x) c = - prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x)); + stm_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 (fun () -> + stm_prerr_endline (fun () -> " classified as: " ^ string_of_vernac_classification c); match c with (* PG stuff *) @@ -2558,7 +2558,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty VCS.commit id (Alias (oid,x)); Backtrack.record (); if w == VtNow then finish (); `Ok | VtStm (VtBack id, false), VtNow -> - prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id); + stm_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 @@ -2708,7 +2708,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty expr = VernacShow (ShowGoal OpenSubgoals) } | _ -> () end; - prerr_endline (fun () -> "processed }}}"); + stm_prerr_endline (fun () -> "processed }}}"); VCS.print (); rc with e -> @@ -2894,7 +2894,7 @@ let edit_at id = anomaly (str ("edit_at "^Stateid.to_string id^": ") ++ CErrors.print_no_report e) | Some (_, id) -> - prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); + stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); VCS.restore vcs; VCS.print (); iraise (e, info) -- cgit v1.2.3 From 921ea3983d45051ae85b0e20bf13de2eff38e53e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 8 Feb 2017 18:13:25 +0100 Subject: [pp] Remove uses of expensive string_of_ppcmds. In general we want to avoid this as much as we can, as it will need to make choices regarding the output backend (width, etc...) and it is expensive. It is better to serve the printing backends the pretty print document itself. --- stm/stm.ml | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index ee142b2930..b9dbb78917 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -6,11 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -let stm_pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr +let stm_pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr +let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n" (System.process_id ()) Pp.pp_with pp; flush stderr let stm_prerr_endline s = if false then begin stm_pr_err (s ()) end else () let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else () +let stm_pperr_endline s = if false then begin stm_pp_err (s ()) end else () + open Vernacexpr open CErrors open Pp @@ -994,11 +997,11 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } = in let aux_interp cmd = if is_filtered_command cmd then - stm_prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr)) + stm_pperr_endline Pp.(fun () -> str "ignoring " ++ pr_vernac expr) else match cmd with | VernacShow ShowScript -> ShowScript.show_script () | expr -> - stm_prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr)); + stm_pperr_endline Pp.(fun () -> str "interpreting " ++ pr_vernac expr); try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr) with e -> let e = CErrors.push e in @@ -1431,11 +1434,10 @@ end = struct (* {{{ *) | Some (safe, err) -> err, safe | None -> Stateid.dummy, Stateid.dummy in let e_msg = iprint (e, info) in - stm_prerr_endline (fun () -> "failed with the following exception:"); - stm_prerr_endline (fun () -> string_of_ppcmds e_msg); + stm_pperr_endline Pp.(fun () -> str "failed with the following exception: " ++ fnl () ++ 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 e = match classify_vernac e with @@ -1880,10 +1882,10 @@ end = struct (* {{{ *) let open Notations in try let pt, uc = Future.join f in - stm_prerr_endline (fun () -> string_of_ppcmds(hov 0 ( + stm_pperr_endline (fun () -> hov 0 ( str"g=" ++ int (Evar.repr gid) ++ spc () ++ str"t=" ++ (Printer.pr_constr pt) ++ spc () ++ - str"uc=" ++ Evd.pr_evar_universe_context uc))); + str"uc=" ++ Evd.pr_evar_universe_context uc)); (if abstract then Tactics.tclABSTRACT None else (fun x -> x)) (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*> Tactics.exact_no_check pt) @@ -2514,7 +2516,7 @@ let reset_task_queue = Slaves.reset_task_queue (* Document building *) let process_transaction ?(newtip=Stateid.fresh ()) ~tty ({ verbose; loc; expr } as x) c = - stm_prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x)); + stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x); let vcs = VCS.backup () in try let head = VCS.current_branch () in -- cgit v1.2.3 From 6e3fc0992be7ddd841328028dec51d390fffb851 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 25 Jan 2017 01:48:41 +0100 Subject: [stm] Add common toploop for workers. This is a small, but convenient refactoring, as it will allow common argument parsing. --- stm/proofworkertop.ml | 6 +----- stm/queryworkertop.ml | 6 +----- stm/tacworkertop.ml | 6 +----- stm/workerLoop.ml | 15 +++++++++++++++ stm/workerLoop.mli | 9 +++++++++ 5 files changed, 27 insertions(+), 15 deletions(-) create mode 100644 stm/workerLoop.ml create mode 100644 stm/workerLoop.mli (limited to 'stm') diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml index 23538a467e..0d2f9cb747 100644 --- a/stm/proofworkertop.ml +++ b/stm/proofworkertop.ml @@ -8,11 +8,7 @@ module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) -let () = Coqtop.toploop_init := (fun args -> - Flags.make_silent true; - W.init_stdout (); - CoqworkmgrApi.init !Flags.async_proofs_worker_priority; - args) +let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout let () = Coqtop.toploop_run := W.main_loop diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml index fff6d55434..9d30473739 100644 --- a/stm/queryworkertop.ml +++ b/stm/queryworkertop.ml @@ -8,11 +8,7 @@ module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) -let () = Coqtop.toploop_init := (fun args -> - Flags.make_silent true; - W.init_stdout (); - CoqworkmgrApi.init !Flags.async_proofs_worker_priority; - args) +let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout let () = Coqtop.toploop_run := W.main_loop diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml index d5333d1077..256532c6b6 100644 --- a/stm/tacworkertop.ml +++ b/stm/tacworkertop.ml @@ -8,11 +8,7 @@ module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) -let () = Coqtop.toploop_init := (fun args -> - Flags.make_silent true; - W.init_stdout (); - CoqworkmgrApi.init !Flags.async_proofs_worker_priority; - args) +let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout let () = Coqtop.toploop_run := W.main_loop diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml new file mode 100644 index 0000000000..56fcf8537f --- /dev/null +++ b/stm/workerLoop.ml @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit) -> string list -> string list -- cgit v1.2.3 From 829a8feb3d02da057d39b5029b422e8a45dd1608 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 25 Jan 2017 14:39:29 +0100 Subject: [xml] Restore protocol compatibility with 8.6. By default, we serialize messages to the "rich printing representation" as it was done in 8.6, this ways clients don't have to adapt unless they specifically request the new format using option `--xml_format=Ppcmds` --- stm/stm.mllib | 1 + stm/workerLoop.ml | 6 +++++- 2 files changed, 6 insertions(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/stm.mllib b/stm/stm.mllib index 4b254e8113..72b5380162 100644 --- a/stm/stm.mllib +++ b/stm/stm.mllib @@ -5,6 +5,7 @@ TQueue WorkerPool Vernac_classifier CoqworkmgrApi +WorkerLoop AsyncTaskQueue Stm ProofBlockDelimiter diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml index 56fcf8537f..50b42512cb 100644 --- a/stm/workerLoop.ml +++ b/stm/workerLoop.ml @@ -6,9 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -let rec parse args = args +let rec parse = function + | "--xml_format=Ppcmds" :: rest -> parse rest + | x :: rest -> x :: parse rest + | [] -> [] let loop init args = + let args = parse args in Flags.make_silent true; init (); CoqworkmgrApi.init !Flags.async_proofs_worker_priority; -- cgit v1.2.3