diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/profile_ltac.ml | 29 | ||||
| -rw-r--r-- | plugins/ltac/profile_ltac.mli | 37 | ||||
| -rw-r--r-- | plugins/ltac/profile_ltac_tactics.ml4 | 36 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 11 | ||||
| -rw-r--r-- | plugins/ltac/taccoerce.ml | 18 | ||||
| -rw-r--r-- | plugins/ltac/taccoerce.mli | 3 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 29 |
7 files changed, 113 insertions, 50 deletions
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 5225420dc4..1615465281 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -289,7 +289,7 @@ let rec find_in_stack what acc = function | { name } as x :: rest when String.equal name what -> Some(acc, x, rest) | { name } as x :: rest -> find_in_stack what (x :: acc) rest -let exit_tactic start_time c = +let exit_tactic ~count_call start_time c = let diff = time () -. start_time in match Local.(!stack) with | [] | [_] -> @@ -304,7 +304,7 @@ let exit_tactic start_time c = let node = { node with total = node.total +. diff; local = node.local +. diff; - ncalls = node.ncalls + 1; + ncalls = node.ncalls + (if count_call then 1 else 0); max_total = max node.max_total diff; } in (* updating the stack *) @@ -341,7 +341,7 @@ let tclFINALLY tac (finally : unit Proofview.tactic) = (fun v -> finally <*> Proofview.tclUNIT v) (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn) -let do_profile s call_trace tac = +let do_profile s call_trace ?(count_call=true) tac = let open Proofview.Notations in Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> if !is_profiling then @@ -359,7 +359,7 @@ let do_profile s call_trace tac = tac (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> (match call_trace with - | (_, c) :: _ -> exit_tactic start_time c + | (_, c) :: _ -> exit_tactic ~count_call start_time c | [] -> ())))) | None -> tac @@ -397,6 +397,27 @@ let reset_profile () = reset_profile_tmp (); data := SM.empty +(* ****************************** Named timers ****************************** *) + +let timer_data = ref M.empty + +let timer_name = function + | Some v -> v + | None -> "" + +let restart_timer name = + timer_data := M.add (timer_name name) (System.get_time ()) !timer_data + +let get_timer name = + try M.find (timer_name name) !timer_data + with Not_found -> System.get_time () + +let finish_timing ~prefix name = + let tend = System.get_time () in + let tstart = get_timer name in + Feedback.msg_info(str prefix ++ pr_opt str name ++ str " ran for " ++ + System.fmt_time_difference tstart tend) + (* ******************** *) let print_results_filter ~cutoff ~filter = diff --git a/plugins/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli index 52827cb36b..adedf7ee91 100644 --- a/plugins/ltac/profile_ltac.mli +++ b/plugins/ltac/profile_ltac.mli @@ -9,9 +9,39 @@ (** Ltac profiling primitives *) +(* Note(JasonGross): Ltac semantics are a bit insane. There isn't + really a good notion of how many times a tactic has been "called", + because tactics can be partially evaluated, and it's unclear + whether the number of "calls" should be the number of times the + body is fetched and unfolded, or the number of times the code is + executed to a value, etc. The logic in [Tacinterp.eval_tactic] + gives a decent approximation, which I believe roughly corresponds + to the number of times that the engine runs the tactic value which + results from evaluating the tactic expression bound to the name + we're considering. However, this is a poor approximation of the + time spent in the tactic; we want to consider time spent evaluating + a tactic expression to a tactic value to be time spent in the + expression, not just time spent in the caller of the expression. + So we need to wrap some nodes in additional profiling calls which + don't count towards to total call count. Whether or not a call + "counts" is indicated by the [count_call] boolean argument. + + Unfortunately, at present, we can get very strange call graphs when + a named tactic expression never runs as a tactic value: if we have + [Ltac t0 := t.] and [Ltac t1 := t0.], then [t1] is considered to + run 0(!) times. It evaluates to [t] during tactic expression + evaluation, and although the call trace records the fact that it + was called by [t0] which was called by [t1], the tactic running + phase never sees this. Thus we get one call tree (from expression + evaluation) that has [t1] calls [t0] calls [t], and another call + tree which says that the caller of [t1] calls [t] directly; the + expression evaluation time goes in the first tree, and the call + count and tactic running time goes in the second tree. Alas, I + suspect that fixing this requires a redesign of how the profiler + hooks into the tactic engine. *) val do_profile : string -> ('a * Tacexpr.ltac_call_kind) list -> - 'b Proofview.tactic -> 'b Proofview.tactic + ?count_call:bool -> 'b Proofview.tactic -> 'b Proofview.tactic val set_profiling : bool -> unit @@ -22,6 +52,10 @@ val print_results_tactic : string -> unit val reset_profile : unit -> unit +val restart_timer : string option -> unit + +val finish_timing : prefix:string -> string option -> unit + val do_print_results_at_close : unit -> unit (* The collected statistics for a tactic. The timing data is collected over all @@ -46,4 +80,3 @@ type treenode = { (* Returns the profiling results known by the current process *) val get_local_profiling_results : unit -> treenode val feedback_results : treenode -> unit - diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4 index f095660638..9864ffeb65 100644 --- a/plugins/ltac/profile_ltac_tactics.ml4 +++ b/plugins/ltac/profile_ltac_tactics.ml4 @@ -18,6 +18,21 @@ DECLARE PLUGIN "ltac_plugin" let tclSET_PROFILING b = Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> set_profiling b)) +let tclRESET_PROFILE = + Proofview.tclLIFT (Proofview.NonLogical.make reset_profile) + +let tclSHOW_PROFILE ~cutoff = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results ~cutoff)) + +let tclSHOW_PROFILE_TACTIC s = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results_tactic s)) + +let tclRESTART_TIMER s = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> restart_timer s)) + +let tclFINISH_TIMING ?(prefix="Timer") (s : string option) = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> finish_timing ~prefix s)) + TACTIC EXTEND start_ltac_profiling | [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ] END @@ -26,8 +41,27 @@ TACTIC EXTEND stop_ltac_profiling | [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ] END +TACTIC EXTEND reset_ltac_profile +| [ "reset" "ltac" "profile" ] -> [ tclRESET_PROFILE ] +END + +TACTIC EXTEND show_ltac_profile +| [ "show" "ltac" "profile" ] -> [ tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff ] +| [ "show" "ltac" "profile" "cutoff" int(n) ] -> [ tclSHOW_PROFILE ~cutoff:(float_of_int n) ] +| [ "show" "ltac" "profile" string(s) ] -> [ tclSHOW_PROFILE_TACTIC s ] +END + +TACTIC EXTEND restart_timer +| [ "restart_timer" string_opt(s) ] -> [ tclRESTART_TIMER s ] +END + +TACTIC EXTEND finish_timing +| [ "finish_timing" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix:"Timer" s ] +| [ "finish_timing" "(" string(prefix) ")" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix s ] +END + VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF - [ "Reset" "Ltac" "Profile" ] -> [ reset_profile() ] + [ "Reset" "Ltac" "Profile" ] -> [ reset_profile () ] END VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2e14243d8a..a698b05dd7 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1781,7 +1781,9 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = - new_instance (Flags.is_universe_polymorphism ()) + let program_mode = Flags.is_program_mode () in + let poly = Flags.is_universe_polymorphism () in + new_instance ~program_mode poly binders instance (Some (true, CAst.make @@ CRecord (fields))) ~global ~generalize:false ~refine:false Hints.empty_hint_info @@ -2012,9 +2014,10 @@ let add_morphism glob binders m s n = [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - ignore(new_instance ~global:glob poly binders instance - (Some (true, CAst.make @@ CRecord [])) - ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) + let program_mode = Flags.is_program_mode () in + ignore(new_instance ~program_mode ~global:glob poly binders instance + (Some (true, CAst.make @@ CRecord [])) + ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) (** Bind to "rewrite" too *) diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 9ae112d371..e5933de2a6 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -61,12 +61,9 @@ struct type t = Val.t -let normalize v = v - let of_constr c = in_gen (topwit wit_constr) c let to_constr v = - let v = normalize v in if has_type v (topwit wit_constr) then let c = out_gen (topwit wit_constr) v in Some c @@ -78,7 +75,6 @@ let to_constr v = let of_uconstr c = in_gen (topwit wit_uconstr) c let to_uconstr v = - let v = normalize v in if has_type v (topwit wit_uconstr) then Some (out_gen (topwit wit_uconstr) v) else None @@ -86,7 +82,6 @@ let to_uconstr v = let of_int i = in_gen (topwit wit_int) i let to_int v = - let v = normalize v in if has_type v (topwit wit_int) then Some (out_gen (topwit wit_int) v) else None @@ -108,14 +103,12 @@ let constr_of_id env id = (* Gives the constr corresponding to a Constr_context tactic_arg *) let coerce_to_constr_context v = - let v = Value.normalize v in if has_type v (topwit wit_constr_context) then out_gen (topwit wit_constr_context) v else raise (CannotCoerceTo "a term context") (* Interprets an identifier which must be fresh *) let coerce_var_to_ident fresh env sigma v = - let v = Value.normalize v in let fail () = raise (CannotCoerceTo "a fresh identifier") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -140,7 +133,6 @@ let g = sigma in let id_of_name = function | Name.Anonymous -> Id.of_string "x" | Name.Name x -> x in - let v = Value.normalize v in let fail () = raise (CannotCoerceTo "an identifier") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -179,7 +171,6 @@ let id_of_name = function let coerce_to_intro_pattern env sigma v = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then snd (out_gen (topwit wit_intro_pattern) v) else if has_type v (topwit wit_var) then @@ -198,7 +189,6 @@ let coerce_to_intro_pattern_naming env sigma v = | _ -> raise (CannotCoerceTo "a naming introduction pattern") let coerce_to_hint_base v = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with | _, IntroNaming (IntroIdentifier id) -> Id.to_string id @@ -206,13 +196,11 @@ let coerce_to_hint_base v = else raise (CannotCoerceTo "a hint base name") let coerce_to_int v = - let v = Value.normalize v in if has_type v (topwit wit_int) then out_gen (topwit wit_int) v else raise (CannotCoerceTo "an integer") let coerce_to_constr env v = - let v = Value.normalize v in let fail () = raise (CannotCoerceTo "a term") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -230,7 +218,6 @@ let coerce_to_constr env v = else fail () let coerce_to_uconstr env v = - let v = Value.normalize v in if has_type v (topwit wit_uconstr) then out_gen (topwit wit_uconstr) v else @@ -243,7 +230,6 @@ let coerce_to_closed_constr env v = let coerce_to_evaluable_ref env sigma v = let fail () = raise (CannotCoerceTo "an evaluable reference") in - let v = Value.normalize v in let ev = if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -284,7 +270,6 @@ let coerce_to_intro_pattern_list ?loc env sigma v = let coerce_to_hyp env sigma v = let fail () = raise (CannotCoerceTo "a variable") in - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with | _, IntroNaming (IntroIdentifier id) when is_variable env id -> id @@ -306,7 +291,6 @@ let coerce_to_hyp_list env sigma v = (* Interprets a qualified name *) let coerce_to_reference env sigma v = - let v = Value.normalize v in match Value.to_constr v with | Some c -> begin @@ -318,7 +302,6 @@ let coerce_to_reference env sigma v = (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) let coerce_to_quantified_hypothesis sigma v = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let v = out_gen (topwit wit_intro_pattern) v in match v with @@ -336,7 +319,6 @@ let coerce_to_quantified_hypothesis sigma v = (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) let coerce_to_decl_or_quant_hyp env sigma v = - let v = Value.normalize v in if has_type v (topwit wit_int) then AnonHyp (out_gen (topwit wit_int) v) else diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index d7b253a687..dce16b7333 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -31,9 +31,6 @@ module Value : sig type t = Val.t - val normalize : t -> t - (** Eliminated the leading dynamic type casts. *) - val of_constr : constr -> t val to_constr : t -> constr option val of_uconstr : Ltac_pretype.closed_glob_constr -> t diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index ded902a8fb..f2720954d0 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -136,7 +136,6 @@ let to_tacvalue v = out_gen (topwit wit_tacvalue) v (** More naming applications *) let name_vfun appl vle = - let vle = Value.normalize vle in if has_type vle (topwit wit_tacvalue) then match to_tacvalue vle with | VFun (appl0,trace,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,lfun,vars,t)) @@ -235,7 +234,6 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with (* Displays a value *) let pr_value env v = - let v = Value.normalize v in let pr_with_env pr = match env with | Some (env,sigma) -> pr env sigma @@ -285,7 +283,6 @@ let push_trace call ist = match TacStore.get ist.extra f_trace with | Some trace -> Proofview.tclUNIT (call :: trace) let propagate_trace ist loc id v = - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then let tacv = to_tacvalue v in match tacv with @@ -298,7 +295,6 @@ let propagate_trace ist loc id v = else Proofview.tclUNIT v let append_trace trace v = - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then match to_tacvalue v with | VFun (appl,trace',lfun,it,b) -> of_tacvalue (VFun (appl,trace'@trace,lfun,it,b)) @@ -307,11 +303,9 @@ let append_trace trace v = (* Dynamically check that an argument is a tactic *) let coerce_to_tactic loc id v = - let v = Value.normalize v in let fail () = user_err ?loc (str "Variable " ++ Id.print id ++ str " should be bound to a tactic.") in - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then let tacv = to_tacvalue v in match tacv with @@ -514,7 +508,6 @@ let rec intropattern_ids accu (loc,pat) = match pat with let extract_ids ids lfun accu = let fold id v accu = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let (_, ipat) = out_gen (topwit wit_intro_pattern) v in if Id.List.mem id ids then accu @@ -816,7 +809,6 @@ let interp_constr_may_eval ist env sigma c = (** TODO: should use dedicated printers *) let message_of_value v = - let v = Value.normalize v in let pr_with_env pr = Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in let open Genprint in @@ -986,7 +978,6 @@ let interp_destruction_arg ist gl arg = try (** FIXME: should be moved to taccoerce *) let v = Id.Map.find id ist.lfun in - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let v = out_gen (topwit wit_intro_pattern) v in match v with @@ -1158,10 +1149,14 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Proofview.V82.tactic begin tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) end - | TacAbstract (tac,ido) -> + | TacAbstract (t,ido) -> + let call = LtacMLCall tac in + push_trace(None,call) ist >>= fun trace -> + Profile_ltac.do_profile "eval_tactic:TacAbstract" trace + (catch_error_tac trace begin Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT - (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist tac) - end + (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist t) + end end) | TacThen (t1,t) -> Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t) | TacDispatch tl -> @@ -1244,7 +1239,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Ftactic.run args tac and force_vrec ist v : Val.t Ftactic.t = - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then let v = to_tacvalue v in match v with @@ -1272,7 +1266,8 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = let extra = TacStore.set extra f_trace trace in let ist = { lfun = Id.Map.empty; extra = extra; } in let appl = GlbAppl[r,[]] in - val_interp ~appl ist (Tacenv.interp_ltac r) + Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false + (val_interp ~appl ist (Tacenv.interp_ltac r)) and interp_tacarg ist arg : Val.t Ftactic.t = match arg with @@ -1319,7 +1314,6 @@ and interp_tacarg ist arg : Val.t Ftactic.t = and interp_app loc ist fv largs : Val.t Ftactic.t = let (>>=) = Ftactic.bind in let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in - let fv = Value.normalize fv in if has_type fv (topwit wit_tacvalue) then match to_tacvalue fv with (* if var=[] and body has been delayed by val_interp, then body @@ -1338,7 +1332,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = let ist = { lfun = newlfun; extra = TacStore.set ist.extra f_trace []; } in - catch_error_tac trace (val_interp ist body) >>= fun v -> + Profile_ltac.do_profile "interp_app" trace ~count_call:false + (catch_error_tac trace (val_interp ist body)) >>= fun v -> Ftactic.return (name_vfun (push_appl appl largs) v) end begin fun (e, info) -> @@ -1371,7 +1366,6 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = (* Gives the tactic corresponding to the tactic value *) and tactic_of_value ist vle = - let vle = Value.normalize vle in if has_type vle (topwit wit_tacvalue) then match to_tacvalue vle with | VFun (appl,trace,lfun,[],t) -> @@ -1598,7 +1592,6 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t = Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in - let result = Value.normalize result in try let cresult = coerce_to_closed_constr env result in Proofview.tclLIFT begin |