From 9ff2c9d8d042c9989b6a8138c308398c49ae116f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 23 Jun 2015 10:12:41 +0200 Subject: LtacProf for Coq trunk This add LtacProfiling. Much of the code was written by Tobias Tebbi (@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq v8.5 and Coq trunk. --- toplevel/coqtop.ml | 1 + toplevel/usage.ml | 1 + 2 files changed, 2 insertions(+) (limited to 'toplevel') diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 869f6bb93..c2a1bac73 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -549,6 +549,7 @@ let parse_args arglist = else native_compiler := true |"-notop" -> unset_toplevel_name () |"-output-context" -> output_context := true + |"-profileltac" -> Profile_ltac.set_profiling true; Profile_ltac.set_display_profile_at_close true |"-q" -> no_load_rc () |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false |"-quick" -> Flags.compilation_mode := BuildVio diff --git a/toplevel/usage.ml b/toplevel/usage.ml index f855c096e..fa57d9d21 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -77,6 +77,7 @@ let print_usage_channel co command = \n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\ \n stdout (if unset)\ \n -time display the time taken by each command\ +\n -profileltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ \n (use environment variable\ \n OCAML_GC_STATS=\"/tmp/gclog.txt\"\ -- cgit v1.2.3 From 739ead8b2d70f978e31f793234d7a633636742a1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 13 May 2016 17:57:06 -0400 Subject: -profileltac -> -profile-ltac, as per @herbelin https://github.com/coq/coq/pull/150#issuecomment-219141596 ```bash git grep --name-only profileltac | xargs sed s'/profileltac/profile-ltac/g' -i ``` --- doc/refman/RefMan-ltac.tex | 2 +- tools/coqc.ml | 2 +- toplevel/coqtop.ml | 2 +- toplevel/usage.ml | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) (limited to 'toplevel') diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 59015742e..24f4b2a77 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1272,7 +1272,7 @@ The following two tactics behave like {\tt idtac} but enable and disable the pro {\tt stop profiling}. \end{quote} -You can also pass the {\tt -profileltac} command line option to {\tt coqc}, which performs a {\tt Start Profiling} at the beginning of each document, and a {\tt Show Profile} at the end. +You can also pass the {\tt -profile-ltac} command line option to {\tt coqc}, which performs a {\tt Start Profiling} at the beginning of each document, and a {\tt Show Profile} at the end. Note that the profiler currently does not handle backtracking into multi-success tactics, and issues a warning to this effect in many cases when such backtracking occurs. diff --git a/tools/coqc.ml b/tools/coqc.ml index 7210efc4f..18b2a24fa 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -88,7 +88,7 @@ let parse_args () = (* Options for coqtop : a) options with 0 argument *) - | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profileltac" + | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac" |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob" |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit" diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c2a1bac73..de0f73ff4 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -549,7 +549,7 @@ let parse_args arglist = else native_compiler := true |"-notop" -> unset_toplevel_name () |"-output-context" -> output_context := true - |"-profileltac" -> Profile_ltac.set_profiling true; Profile_ltac.set_display_profile_at_close true + |"-profile-ltac" -> Profile_ltac.set_profiling true; Profile_ltac.set_display_profile_at_close true |"-q" -> no_load_rc () |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false |"-quick" -> Flags.compilation_mode := BuildVio diff --git a/toplevel/usage.ml b/toplevel/usage.ml index fa57d9d21..5359a288a 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -77,7 +77,7 @@ let print_usage_channel co command = \n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\ \n stdout (if unset)\ \n -time display the time taken by each command\ -\n -profileltac display the time taken by each (sub)tactic\ +\n -profile-ltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ \n (use environment variable\ \n OCAML_GC_STATS=\"/tmp/gclog.txt\"\ -- cgit v1.2.3 From e4d5bbeecb4c5a4eca82700ba3946d9fd174e215 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 14 Jun 2016 00:12:44 +0200 Subject: Moving back Ltac profiling to the Ltac folder. --- Makefile.build | 2 +- Makefile.common | 5 +- lib/flags.ml | 1 + lib/flags.mli | 2 + ltac/ltac.mllib | 1 + ltac/profile_ltac.ml | 304 ++++++++++++++++++++++++++++++++++++++++++ ltac/profile_ltac.mli | 15 +++ ltac/profile_ltac_tactics.ml4 | 9 -- ltacprof/ltacprof.mllib | 1 - ltacprof/profile_ltac.ml | 301 ----------------------------------------- ltacprof/profile_ltac.mli | 17 --- toplevel/coqtop.ml | 2 +- 12 files changed, 327 insertions(+), 333 deletions(-) create mode 100644 ltac/profile_ltac.ml create mode 100644 ltac/profile_ltac.mli delete mode 100644 ltacprof/ltacprof.mllib delete mode 100644 ltacprof/profile_ltac.ml delete mode 100644 ltacprof/profile_ltac.mli (limited to 'toplevel') diff --git a/Makefile.build b/Makefile.build index 4f3077e5d..fc92507e6 100644 --- a/Makefile.build +++ b/Makefile.build @@ -570,7 +570,7 @@ test-suite: world $(ALLSTDLIB).v ################################################################## .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping -.PHONY: engine highparsing stm toplevel ltac ltacprof +.PHONY: engine highparsing stm toplevel ltac lib: lib/clib.cma lib/lib.cma kernel: kernel/kernel.cma diff --git a/Makefile.common b/Makefile.common index e2f67226b..86a7ea847 100644 --- a/Makefile.common +++ b/Makefile.common @@ -62,7 +62,7 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE) CORESRCDIRS:=\ config lib kernel kernel/byterun library \ - proofs tactics pretyping interp stm ltacprof\ + proofs tactics pretyping interp stm \ toplevel parsing printing intf engine ltac PLUGINS:=\ @@ -167,8 +167,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma \ - stm/stm.cma ltacprof/ltacprof.cma toplevel/toplevel.cma \ - parsing/highparsing.cma ltac/ltac.cma + stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma ltac/ltac.cma TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma diff --git a/lib/flags.ml b/lib/flags.ml index c1ec9738c..4983e4082 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -220,6 +220,7 @@ let native_compiler = ref false let print_mod_uid = ref false let tactic_context_compat = ref false +let profile_ltac = ref false let dump_bytecode = ref false let set_dump_bytecode = (:=) dump_bytecode diff --git a/lib/flags.mli b/lib/flags.mli index 24780f0dc..e13655e4a 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -143,6 +143,8 @@ val tactic_context_compat : bool ref (** Set to [true] to trigger the compatibility bugged context matching (old context vs. appcontext) is set. *) +val profile_ltac : bool ref + (** Dump the bytecode after compilation (for debugging purposes) *) val dump_bytecode : bool ref val set_dump_bytecode : bool -> unit diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib index d8854e6e7..65ed114cf 100644 --- a/ltac/ltac.mllib +++ b/ltac/ltac.mllib @@ -3,6 +3,7 @@ Tacenv Tactic_debug Tacintern Tacentries +Profile_ltac Tacinterp Evar_tactics Tactic_option diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml new file mode 100644 index 000000000..4f982f1eb --- /dev/null +++ b/ltac/profile_ltac.ml @@ -0,0 +1,304 @@ +open Unicode +open Pp +open Printer +open Util + + +(** [is_profiling] and the profiling info ([stack]) should be synchronized with the document; the rest of the ref cells are either local to individual tactic invocations, or global flags, and need not be synchronized, since no document-level backtracking happens within tactics. We synchronize is_profiling via an option. *) +let is_profiling = Flags.profile_ltac + +let set_profiling b = is_profiling := b +let get_profiling () = !is_profiling + +let new_call = ref false +let entered_call() = new_call := true +let is_new_call() = let b = !new_call in new_call := false; b + +(** Local versions of the old Pp.msgnl *) +let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ()) +let msgnl strm = msgnl_with !Pp_control.std_ft strm + +(** LtacProf cannot yet handle backtracking into multi-success tactics. To properly support this, we'd have to somehow recreate our location in the call-stack, and stop/restart the intervening timers. This is tricky and possibly expensive, so instead we currently just emit a warning that profiling results will be off. *) +let encountered_multi_success_backtracking = ref false +let warn_encountered_multi_success_backtracking() = + if !encountered_multi_success_backtracking + then Feedback.msg_warning (str "Ltac Profiler cannot yet handle backtracking into multi-success tactics; profiling results may be wildly inaccurate.") +let encounter_multi_success_backtracking() = + if not !encountered_multi_success_backtracking + then begin + encountered_multi_success_backtracking := true; + warn_encountered_multi_success_backtracking() + end + + +type entry = {mutable total : float; mutable local : float; mutable ncalls : int; mutable max_total : float} +let empty_entry() = {total = 0.; local = 0.; ncalls = 0; max_total = 0.} +let add_entry e add_total {total; local; ncalls; max_total} = + if add_total then e.total <- e.total +. total; + e.local <- e.local +. local; + e.ncalls <- e.ncalls + ncalls; + if add_total then e.max_total <- max e.max_total max_total + +type treenode = {entry : entry; children : (string, treenode) Hashtbl.t} + +(** Tobias Tebbi wrote some tricky code involving mutation. Rather than rewriting it in a functional style, we simply freeze the state when we need to by issuing a deep copy of the profiling data. *) +let deepcopy_entry {total; local; ncalls; max_total} = + {total; local; ncalls; max_total} + +let rec deepcopy_treenode {entry; children} = + {entry = deepcopy_entry entry; + children = + (let children' = Hashtbl.create (Hashtbl.length children) in + Hashtbl.iter + (fun key subtree -> Hashtbl.add children' key (deepcopy_treenode subtree)) + children; + children')} + +let stack = Summary.ref ~freeze:(fun _ -> List.map deepcopy_treenode) [{entry=empty_entry(); children=Hashtbl.create 20}] ~name:"LtacProf-stack" + +let on_stack = Hashtbl.create 5 + +let get_node c table = + try Hashtbl.find table c + with Not_found -> + let new_node = {entry=empty_entry(); children=Hashtbl.create 5} in + Hashtbl.add table c new_node; + new_node + +let rec add_node node node' = + add_entry node.entry true node'.entry; + Hashtbl.iter + (fun s node' -> add_node (get_node s node.children) node') + node'.children + +let time() = + let times = Unix.times() in + times.Unix.tms_utime +. times.Unix.tms_stime + +let rec print_treenode indent (tn : treenode) = + msgnl(str(indent^"{ entry = {")); + Feedback.msg_notice(str(indent^"total = ")); + msgnl(str (indent^(string_of_float (tn.entry.total)))); + Feedback.msg_notice(str(indent^"local = ")); + msgnl(str (indent^(string_of_float tn.entry.local))); + Feedback.msg_notice(str(indent^"ncalls = ")); + msgnl(str (indent^(string_of_int tn.entry.ncalls))); + Feedback.msg_notice(str(indent^"max_total = ")); + msgnl(str (indent^(string_of_float tn.entry.max_total))); + msgnl(str(indent^"}")); + msgnl(str(indent^"children = {")); + Hashtbl.iter + (fun s node -> + msgnl(str(indent^" "^s^" |-> ")); + print_treenode (indent^" ") node + ) + tn.children; + msgnl(str(indent^"} }")) + +let rec print_stack (st : treenode list) = + (match st with + | [] -> msgnl(str "[]") + | x::xs -> print_treenode "" x; msgnl(str("::")); print_stack xs) + + +let string_of_call ck = + let s = + string_of_ppcmds + (match ck with + | Tacexpr.LtacNotationCall s -> Names.KerName.print s + | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst + | Tacexpr.LtacVarCall (id,t) -> Nameops.pr_id id + | Tacexpr.LtacAtomCall te -> + (Pptactic.pr_glob_tactic (Global.env()) + (Tacexpr.TacAtom (Loc.ghost,te))) + | Tacexpr.LtacConstrInterp (c,_) -> + pr_glob_constr_env (Global.env()) c + | Tacexpr.LtacMLCall te -> + (Pptactic.pr_glob_tactic (Global.env()) + te) + ) in + for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done; + let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in + CString.strip s + +let exit_tactic start_time add_total c = + try + let node :: stack' = !stack in + let parent = List.hd stack' in + stack := stack'; + if add_total then Hashtbl.remove on_stack (string_of_call c); + let diff = time() -. start_time in + parent.entry.local <- parent.entry.local -. diff; + add_entry node.entry add_total {total = diff; local = diff; ncalls = 1; max_total = diff}; + with Failure("hd") -> (* oops, our stack is invalid *) + encounter_multi_success_backtracking() + +let tclFINALLY tac (finally : unit Proofview.tactic) = + let open Proofview.Notations in + Proofview.tclIFCATCH + tac + (fun v -> finally <*> Proofview.tclUNIT v) + (fun (exn,info) -> finally <*> Proofview.tclZERO ~info exn) + +let do_profile s call_trace tac = + let open Proofview.Notations in + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + if !is_profiling && is_new_call() then + match call_trace with + | (_, c) :: _ -> + let s = string_of_call c in + let parent = List.hd !stack in + let node, add_total = try Hashtbl.find on_stack s, false + with Not_found -> + let node = get_node s parent.children in + Hashtbl.add on_stack s node; + node, true + in + if not add_total && node = List.hd !stack then None else ( + stack := node :: !stack; + let start_time = time() in + Some (start_time, add_total) + ) + | [] -> None + else None)) >>= function + | Some (start_time, add_total) -> + tclFINALLY + tac + (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + (match call_trace with + | (_, c) :: _ -> + exit_tactic start_time add_total c + | [] -> ())))) + | None -> tac + + + +let format_sec x = (Printf.sprintf "%.3fs" x) +let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x)) +let padl n s = ws (max 0 (n - utf8_length s)) ++ str s +let padr n s = str s ++ ws (max 0 (n - utf8_length s)) +let padr_with c n s = + let ulength = utf8_length s in + str (utf8_sub s 0 n) ++ str(String.make (max 0 (n - ulength)) c) + +let rec list_iter_is_last f = function + | [] -> () + | [x] -> f true x + | x :: xs -> f false x; list_iter_is_last f xs + +let header() = + msgnl(str" tactic self total calls max"); + msgnl(str"────────────────────────────────────────┴──────┴──────┴───────┴─────────┘") + +let rec print_node all_total indent prefix (s,n) = + let e = n.entry in + msgnl( + h 0( + padr_with '-' 40 (prefix ^ s ^ " ") + ++padl 7 (format_ratio (e.local /. all_total)) + ++padl 7 (format_ratio (e.total /. all_total)) + ++padl 8 (string_of_int e.ncalls) + ++padl 10 (format_sec(e.max_total)) + ) + ); + print_table all_total indent false n.children + +and print_table all_total indent first_level table = + let ls = Hashtbl.fold + (fun s n l -> if n.entry.total /. all_total < 0.02 then l else (s, n) :: l) + table [] in + match ls with + | [(s,n)] when (not first_level) -> + print_node all_total indent (indent^"└") (s,n) + | _ -> + let ls = List.sort (fun (_, n1) (_, n2) -> compare n2.entry.total n1.entry.total) ls in + list_iter_is_last + (fun is_last -> + print_node + all_total + (indent^if first_level then "" else if is_last then " " else " │") + (indent^if first_level then "─" else if is_last then " └─" else " ├─") + ) + ls + +let print_results() = + let tree = (List.hd !stack).children in + let all_total = -. (List.hd !stack).entry.local in + let global = Hashtbl.create 20 in + let rec cumulate table = + Hashtbl.iter + (fun s node -> + let node' = get_node s global in + add_entry node'.entry true node.entry; + cumulate node.children + ) + table + in + cumulate tree; + warn_encountered_multi_success_backtracking(); + msgnl(str""); + msgnl(h 0( + str"total time: "++padl 11 (format_sec(all_total)) + ) + ); + msgnl(str""); + header(); + print_table all_total "" true global; + msgnl(str""); + header(); + print_table all_total "" true tree + (* FOR DEBUGGING *) + (* ; + msgnl(str""); + print_stack(!stack) + *) + +let print_results_tactic tactic = + let tree = (List.hd !stack).children in + let table_tactic = Hashtbl.create 20 in + let rec cumulate table = + Hashtbl.iter + (fun s node -> + if String.sub (s^".") 0 (min (1+String.length s) (String.length tactic)) = tactic + then add_node (get_node s table_tactic) node + else cumulate node.children + ) + table + in + cumulate tree; + let all_total = -. (List.hd !stack).entry.local in + let tactic_total = + Hashtbl.fold + (fun _ node all_total -> node.entry.total +. all_total) + table_tactic 0. in + warn_encountered_multi_success_backtracking(); + msgnl(str""); + msgnl(h 0( + str"total time: "++padl 11 (format_sec(all_total)) + ) + ); + msgnl(h 0( + str"time spent in tactic: "++padl 11 (format_sec(tactic_total)) + ) + ); + msgnl(str""); + header(); + print_table tactic_total "" true table_tactic + +let reset_profile() = + stack := [{entry=empty_entry(); children=Hashtbl.create 20}]; + encountered_multi_success_backtracking := false + +let do_print_results_at_close () = if get_profiling () then print_results () + +let _ = Declaremods.append_end_library_hook do_print_results_at_close + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "Ltac Profiling"; + optkey = ["Ltac"; "Profiling"]; + optread = get_profiling; + optwrite = set_profiling } diff --git a/ltac/profile_ltac.mli b/ltac/profile_ltac.mli new file mode 100644 index 000000000..0029b8b55 --- /dev/null +++ b/ltac/profile_ltac.mli @@ -0,0 +1,15 @@ +val do_profile : string -> ('a * Tacexpr.ltac_call_kind) list -> 'b Proofview.tactic -> 'b Proofview.tactic + +val set_profiling : bool -> unit + +val get_profiling : unit -> bool + +val entered_call : unit -> unit + +val print_results : unit -> unit + +val print_results_tactic : string -> unit + +val reset_profile : unit -> unit + +val do_print_results_at_close : unit -> unit diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 index b83ab8c52..8889bd13c 100644 --- a/ltac/profile_ltac_tactics.ml4 +++ b/ltac/profile_ltac_tactics.ml4 @@ -17,15 +17,6 @@ TACTIC EXTEND stop_profiling | [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ] END;; -let _ = - Goptions.declare_bool_option - { optsync = true; - optdepr = false; - optname = "Ltac Profiling"; - optkey = ["Ltac"; "Profiling"]; - optread = get_profiling; - optwrite = set_profiling } - VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF [ "Reset" "Ltac" "Profile" ] -> [ reset_profile() ] END diff --git a/ltacprof/ltacprof.mllib b/ltacprof/ltacprof.mllib deleted file mode 100644 index 383e5d285..000000000 --- a/ltacprof/ltacprof.mllib +++ /dev/null @@ -1 +0,0 @@ -Profile_ltac diff --git a/ltacprof/profile_ltac.ml b/ltacprof/profile_ltac.ml deleted file mode 100644 index 41bde12b1..000000000 --- a/ltacprof/profile_ltac.ml +++ /dev/null @@ -1,301 +0,0 @@ -open Unicode -open Pp -open Printer -open Util - - -(** [is_profiling] and the profiling info ([stack]) should be synchronized with the document; the rest of the ref cells are either local to individual tactic invocations, or global flags, and need not be synchronized, since no document-level backtracking happens within tactics. We synchronize is_profiling via an option. *) -let is_profiling = ref false - -let set_profiling b = is_profiling := b -let get_profiling () = !is_profiling - -let should_display_profile_at_close = ref false -let set_display_profile_at_close b = should_display_profile_at_close := b - - -let new_call = ref false -let entered_call() = new_call := true -let is_new_call() = let b = !new_call in new_call := false; b - -(** Local versions of the old Pp.msgnl *) -let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ()) -let msgnl strm = msgnl_with !Pp_control.std_ft strm - -(** LtacProf cannot yet handle backtracking into multi-success tactics. To properly support this, we'd have to somehow recreate our location in the call-stack, and stop/restart the intervening timers. This is tricky and possibly expensive, so instead we currently just emit a warning that profiling results will be off. *) -let encountered_multi_success_backtracking = ref false -let warn_encountered_multi_success_backtracking() = - if !encountered_multi_success_backtracking - then Feedback.msg_warning (str "Ltac Profiler cannot yet handle backtracking into multi-success tactics; profiling results may be wildly inaccurate.") -let encounter_multi_success_backtracking() = - if not !encountered_multi_success_backtracking - then begin - encountered_multi_success_backtracking := true; - warn_encountered_multi_success_backtracking() - end - - -type entry = {mutable total : float; mutable local : float; mutable ncalls : int; mutable max_total : float} -let empty_entry() = {total = 0.; local = 0.; ncalls = 0; max_total = 0.} -let add_entry e add_total {total; local; ncalls; max_total} = - if add_total then e.total <- e.total +. total; - e.local <- e.local +. local; - e.ncalls <- e.ncalls + ncalls; - if add_total then e.max_total <- max e.max_total max_total - -type treenode = {entry : entry; children : (string, treenode) Hashtbl.t} - -(** Tobias Tebbi wrote some tricky code involving mutation. Rather than rewriting it in a functional style, we simply freeze the state when we need to by issuing a deep copy of the profiling data. *) -let deepcopy_entry {total; local; ncalls; max_total} = - {total; local; ncalls; max_total} - -let rec deepcopy_treenode {entry; children} = - {entry = deepcopy_entry entry; - children = - (let children' = Hashtbl.create (Hashtbl.length children) in - Hashtbl.iter - (fun key subtree -> Hashtbl.add children' key (deepcopy_treenode subtree)) - children; - children')} - -let stack = Summary.ref ~freeze:(fun _ -> List.map deepcopy_treenode) [{entry=empty_entry(); children=Hashtbl.create 20}] ~name:"LtacProf-stack" - -let on_stack = Hashtbl.create 5 - -let get_node c table = - try Hashtbl.find table c - with Not_found -> - let new_node = {entry=empty_entry(); children=Hashtbl.create 5} in - Hashtbl.add table c new_node; - new_node - -let rec add_node node node' = - add_entry node.entry true node'.entry; - Hashtbl.iter - (fun s node' -> add_node (get_node s node.children) node') - node'.children - -let time() = - let times = Unix.times() in - times.Unix.tms_utime +. times.Unix.tms_stime - -let rec print_treenode indent (tn : treenode) = - msgnl(str(indent^"{ entry = {")); - Feedback.msg_notice(str(indent^"total = ")); - msgnl(str (indent^(string_of_float (tn.entry.total)))); - Feedback.msg_notice(str(indent^"local = ")); - msgnl(str (indent^(string_of_float tn.entry.local))); - Feedback.msg_notice(str(indent^"ncalls = ")); - msgnl(str (indent^(string_of_int tn.entry.ncalls))); - Feedback.msg_notice(str(indent^"max_total = ")); - msgnl(str (indent^(string_of_float tn.entry.max_total))); - msgnl(str(indent^"}")); - msgnl(str(indent^"children = {")); - Hashtbl.iter - (fun s node -> - msgnl(str(indent^" "^s^" |-> ")); - print_treenode (indent^" ") node - ) - tn.children; - msgnl(str(indent^"} }")) - -let rec print_stack (st : treenode list) = - (match st with - | [] -> msgnl(str "[]") - | x::xs -> print_treenode "" x; msgnl(str("::")); print_stack xs) - - -let string_of_call ck = - let s = - string_of_ppcmds - (match ck with - | Tacexpr.LtacNotationCall s -> Names.KerName.print s - | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst - | Tacexpr.LtacVarCall (id,t) -> Nameops.pr_id id - | Tacexpr.LtacAtomCall te -> - (Pptactic.pr_glob_tactic (Global.env()) - (Tacexpr.TacAtom (Loc.ghost,te))) - | Tacexpr.LtacConstrInterp (c,_) -> - pr_glob_constr_env (Global.env()) c - | Tacexpr.LtacMLCall te -> - (Pptactic.pr_glob_tactic (Global.env()) - te) - ) in - for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done; - let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in - CString.strip s - -let exit_tactic start_time add_total c = - try - let node :: stack' = !stack in - let parent = List.hd stack' in - stack := stack'; - if add_total then Hashtbl.remove on_stack (string_of_call c); - let diff = time() -. start_time in - parent.entry.local <- parent.entry.local -. diff; - add_entry node.entry add_total {total = diff; local = diff; ncalls = 1; max_total = diff}; - with Failure("hd") -> (* oops, our stack is invalid *) - encounter_multi_success_backtracking() - -let tclFINALLY tac (finally : unit Proofview.tactic) = - let open Proofview.Notations in - Proofview.tclIFCATCH - tac - (fun v -> finally <*> Proofview.tclUNIT v) - (fun (exn,info) -> finally <*> Proofview.tclZERO ~info exn) - -let do_profile s call_trace tac = - let open Proofview.Notations in - Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> - if !is_profiling && is_new_call() then - match call_trace with - | (_, c) :: _ -> - let s = string_of_call c in - let parent = List.hd !stack in - let node, add_total = try Hashtbl.find on_stack s, false - with Not_found -> - let node = get_node s parent.children in - Hashtbl.add on_stack s node; - node, true - in - if not add_total && node = List.hd !stack then None else ( - stack := node :: !stack; - let start_time = time() in - Some (start_time, add_total) - ) - | [] -> None - else None)) >>= function - | Some (start_time, add_total) -> - tclFINALLY - tac - (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> - (match call_trace with - | (_, c) :: _ -> - exit_tactic start_time add_total c - | [] -> ())))) - | None -> tac - - - -let format_sec x = (Printf.sprintf "%.3fs" x) -let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x)) -let padl n s = ws (max 0 (n - utf8_length s)) ++ str s -let padr n s = str s ++ ws (max 0 (n - utf8_length s)) -let padr_with c n s = - let ulength = utf8_length s in - str (utf8_sub s 0 n) ++ str(String.make (max 0 (n - ulength)) c) - -let rec list_iter_is_last f = function - | [] -> () - | [x] -> f true x - | x :: xs -> f false x; list_iter_is_last f xs - -let header() = - msgnl(str" tactic self total calls max"); - msgnl(str"────────────────────────────────────────┴──────┴──────┴───────┴─────────┘") - -let rec print_node all_total indent prefix (s,n) = - let e = n.entry in - msgnl( - h 0( - padr_with '-' 40 (prefix ^ s ^ " ") - ++padl 7 (format_ratio (e.local /. all_total)) - ++padl 7 (format_ratio (e.total /. all_total)) - ++padl 8 (string_of_int e.ncalls) - ++padl 10 (format_sec(e.max_total)) - ) - ); - print_table all_total indent false n.children - -and print_table all_total indent first_level table = - let ls = Hashtbl.fold - (fun s n l -> if n.entry.total /. all_total < 0.02 then l else (s, n) :: l) - table [] in - match ls with - | [(s,n)] when (not first_level) -> - print_node all_total indent (indent^"└") (s,n) - | _ -> - let ls = List.sort (fun (_, n1) (_, n2) -> compare n2.entry.total n1.entry.total) ls in - list_iter_is_last - (fun is_last -> - print_node - all_total - (indent^if first_level then "" else if is_last then " " else " │") - (indent^if first_level then "─" else if is_last then " └─" else " ├─") - ) - ls - -let print_results() = - let tree = (List.hd !stack).children in - let all_total = -. (List.hd !stack).entry.local in - let global = Hashtbl.create 20 in - let rec cumulate table = - Hashtbl.iter - (fun s node -> - let node' = get_node s global in - add_entry node'.entry true node.entry; - cumulate node.children - ) - table - in - cumulate tree; - warn_encountered_multi_success_backtracking(); - msgnl(str""); - msgnl(h 0( - str"total time: "++padl 11 (format_sec(all_total)) - ) - ); - msgnl(str""); - header(); - print_table all_total "" true global; - msgnl(str""); - header(); - print_table all_total "" true tree - (* FOR DEBUGGING *) - (* ; - msgnl(str""); - print_stack(!stack) - *) - -let print_results_tactic tactic = - let tree = (List.hd !stack).children in - let table_tactic = Hashtbl.create 20 in - let rec cumulate table = - Hashtbl.iter - (fun s node -> - if String.sub (s^".") 0 (min (1+String.length s) (String.length tactic)) = tactic - then add_node (get_node s table_tactic) node - else cumulate node.children - ) - table - in - cumulate tree; - let all_total = -. (List.hd !stack).entry.local in - let tactic_total = - Hashtbl.fold - (fun _ node all_total -> node.entry.total +. all_total) - table_tactic 0. in - warn_encountered_multi_success_backtracking(); - msgnl(str""); - msgnl(h 0( - str"total time: "++padl 11 (format_sec(all_total)) - ) - ); - msgnl(h 0( - str"time spent in tactic: "++padl 11 (format_sec(tactic_total)) - ) - ); - msgnl(str""); - header(); - print_table tactic_total "" true table_tactic - -let reset_profile() = - stack := [{entry=empty_entry(); children=Hashtbl.create 20}]; - encountered_multi_success_backtracking := false - -let do_print_results_at_close () = - if !should_display_profile_at_close - then print_results () - else () - -let _ = Declaremods.append_end_library_hook do_print_results_at_close diff --git a/ltacprof/profile_ltac.mli b/ltacprof/profile_ltac.mli deleted file mode 100644 index 65c067e86..000000000 --- a/ltacprof/profile_ltac.mli +++ /dev/null @@ -1,17 +0,0 @@ -val do_profile : string -> ('a * Tacexpr.ltac_call_kind) list -> 'b Proofview.tactic -> 'b Proofview.tactic - -val set_profiling : bool -> unit - -val get_profiling : unit -> bool - -val set_display_profile_at_close : bool -> unit - -val entered_call : unit -> unit - -val print_results : unit -> unit - -val print_results_tactic : string -> unit - -val reset_profile : unit -> unit - -val do_print_results_at_close : unit -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index de0f73ff4..aab20650a 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -549,7 +549,7 @@ let parse_args arglist = else native_compiler := true |"-notop" -> unset_toplevel_name () |"-output-context" -> output_context := true - |"-profile-ltac" -> Profile_ltac.set_profiling true; Profile_ltac.set_display_profile_at_close true + |"-profile-ltac" -> Flags.profile_ltac := true |"-q" -> no_load_rc () |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false |"-quick" -> Flags.compilation_mode := BuildVio -- cgit v1.2.3