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. --- .gitignore | 1 + Makefile.build | 2 +- Makefile.common | 5 +- lib/pp.ml | 32 +++++ lib/pp.mli | 3 + library/declaremods.ml | 6 + library/declaremods.mli | 3 + ltac/ltac.mllib | 1 + ltac/profile_ltac_tactics.ml4 | 40 ++++++ ltac/tacinterp.ml | 41 +++--- ltacprof/ltacprof.mllib | 1 + ltacprof/profile_ltac.ml | 286 ++++++++++++++++++++++++++++++++++++++++++ ltacprof/profile_ltac.mli | 15 +++ test-suite/success/ltacprof.v | 8 ++ tools/coq_makefile.ml | 5 +- tools/coqc.ml | 2 +- toplevel/coqtop.ml | 1 + toplevel/usage.ml | 1 + 18 files changed, 432 insertions(+), 21 deletions(-) create mode 100644 ltac/profile_ltac_tactics.ml4 create mode 100644 ltacprof/ltacprof.mllib create mode 100644 ltacprof/profile_ltac.ml create mode 100644 ltacprof/profile_ltac.mli create mode 100644 test-suite/success/ltacprof.v diff --git a/.gitignore b/.gitignore index 116f88dd7..bc1a05684 100644 --- a/.gitignore +++ b/.gitignore @@ -128,6 +128,7 @@ parsing/cLexer.ml ltac/coretactics.ml ltac/extratactics.ml ltac/extraargs.ml +ltac/profile_ltac_tactics.ml ide/coqide_main.ml # other auto-generated files diff --git a/Makefile.build b/Makefile.build index 44eb42f9a..c6fef10b6 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 +.PHONY: engine highparsing stm toplevel ltac ltacprof lib: lib/clib.cma lib/lib.cma kernel: kernel/kernel.cma diff --git a/Makefile.common b/Makefile.common index f592cd6ec..37db66be3 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 \ + proofs tactics pretyping interp stm ltacprof\ toplevel parsing printing intf engine ltac PLUGINS:=\ @@ -167,7 +167,8 @@ 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 toplevel/toplevel.cma parsing/highparsing.cma ltac/ltac.cma + stm/stm.cma ltacprof/ltacprof.cma toplevel/toplevel.cma \ + parsing/highparsing.cma ltac/ltac.cma TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma diff --git a/lib/pp.ml b/lib/pp.ml index 99c774e8d..5d7c71635 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -168,6 +168,38 @@ let utf8_length s = done ; !cnt +(* Variant of String.sub for UTF8 character positions *) +let utf8_sub s start_u len_u = + let len_b = String.length s + and end_u = start_u + len_u + and cnt = ref 0 + and nc = ref 0 + and p = ref 0 in + let start_b = ref len_b in + while !p < len_b && !cnt < end_u do + if !cnt <= start_u then start_b := !p ; + begin + match s.[!p] with + | '\000'..'\127' -> nc := 0 (* ascii char *) + | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *) + | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *) + | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *) + | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *) + | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *) + | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *) + | '\254'..'\255' -> nc := 0 (* invalid byte *) + end ; + incr p ; + while !p < len_b && !nc > 0 do + match s.[!p] with + | '\128'..'\191' (* next continuation byte *) -> incr p ; decr nc + | _ (* not a continuation byte *) -> nc := 0 + done ; + incr cnt + done ; + let end_b = !p in + String.sub s !start_b (end_b - !start_b) + (* formatting commands *) let str s = Glue.atom(Ppcmd_print (Str_def s)) let stras (i, s) = Glue.atom(Ppcmd_print (Str_len (s, i))) diff --git a/lib/pp.mli b/lib/pp.mli index a18744c37..56b82e448 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -100,6 +100,9 @@ val close_tag : unit -> std_ppcmds val string_of_ppcmds : std_ppcmds -> string +val utf8_length : string -> int +val utf8_sub : string -> int -> int -> string + (** {6 Printing combinators} *) val pr_comma : unit -> std_ppcmds diff --git a/library/declaremods.ml b/library/declaremods.ml index f3f734aa0..dcd63c769 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -897,7 +897,13 @@ let start_library dir = Lib.start_compilation dir mp; Lib.add_frozen_state () +let end_library_hook = ref ignore +let append_end_library_hook f = + let old_f = !end_library_hook in + end_library_hook := fun () -> old_f(); f () + let end_library ?except dir = + !end_library_hook(); let oname = Lib.end_compilation_checks dir in let mp,cenv,ast = Global.export ?except dir in let prefix, lib_stack = Lib.end_compilation oname in diff --git a/library/declaremods.mli b/library/declaremods.mli index 2b440c087..3917fe8d6 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -90,6 +90,9 @@ val end_library : ?except:Future.UUIDSet.t -> library_name -> Safe_typing.compiled_library * library_objects * Safe_typing.native_library +(** append a function to be executed at end_library *) +val append_end_library_hook : (unit -> unit) -> unit + (** [really_import_module mp] opens the module [mp] (in a Caml sense). It modifies Nametab and performs the [open_object] function for every object of the module. Raises [Not_found] when [mp] is unknown diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib index e0c6f3ac0..d8854e6e7 100644 --- a/ltac/ltac.mllib +++ b/ltac/ltac.mllib @@ -10,6 +10,7 @@ Extraargs G_obligations Coretactics Extratactics +Profile_ltac_tactics G_auto G_class Rewrite diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 new file mode 100644 index 000000000..0c4e0b075 --- /dev/null +++ b/ltac/profile_ltac_tactics.ml4 @@ -0,0 +1,40 @@ +(*i camlp4deps: "grammar/grammar.cma" i*) + +open Profile_ltac +open Stdarg + +DECLARE PLUGIN "profile_ltac_plugin" + +let tclSET_PROFILING b = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + set_profiling b)) + +TACTIC EXTEND start_profiling + | [ "start" "profiling" ] -> [ tclSET_PROFILING true ] +END + +TACTIC EXTEND stop_profiling + | [ "stop" "profiling" ] -> [ tclSET_PROFILING false ] +END;; + + +VERNAC COMMAND EXTEND StartProfiling CLASSIFIED AS SIDEFF + [ "Start" "Profiling" ] -> [ reset_profile(); set_profiling true ] +END + +VERNAC COMMAND EXTEND StopProfiling CLASSIFIED AS SIDEFF + [ "Stop" "Profiling" ] -> [ set_profiling false ] + END + +VERNAC COMMAND EXTEND ResetProfiling CLASSIFIED AS SIDEFF + [ "Reset" "Profile" ] -> [ reset_profile() ] +END + +VERNAC COMMAND EXTEND ShowProfile CLASSIFIED AS QUERY + [ "Show" "Profile" ] -> [ print_results() ] +END + + +VERNAC COMMAND EXTEND ShowProfileTactic CLASSIFIED AS QUERY + [ "Show" "Profile" string(s) ] -> [ print_results_tactic s ] +END diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 2c1f59634..4f7c02968 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -286,9 +286,10 @@ let constr_of_id env id = (** Generic arguments : table of interpretation functions *) +(* Some of the code further down depends on the fact that push_trace does not modify sigma (the evar map) *) let push_trace call ist = match TacStore.get ist.extra f_trace with -| None -> [call] -| Some trace -> call :: trace +| None -> Proofview.tclUNIT [call] +| Some trace -> Proofview.tclLIFT (Proofview.NonLogical.make Profile_ltac.entered_call) <*> Proofview.tclUNIT (call :: trace) let propagate_trace ist loc id v = let v = Value.normalize v in @@ -297,10 +298,11 @@ let propagate_trace ist loc id v = match tacv with | VFun (appl,_,lfun,it,b) -> let t = if List.is_empty it then b else TacFun (it,b) in - let ans = VFun (appl,push_trace(loc,LtacVarCall (id,t)) ist,lfun,it,b) in - of_tacvalue ans - | _ -> v - else v + push_trace(loc,LtacVarCall (id,t)) ist >>= fun trace -> + let ans = VFun (appl,trace,lfun,it,b) in + Proofview.tclUNIT (of_tacvalue ans) + | _ -> Proofview.tclUNIT v + else Proofview.tclUNIT v let append_trace trace v = let v = Value.normalize v in @@ -622,8 +624,13 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in intern_gen kind_for_intern ~allow_patvar ~ltacvars env c in - let trace = - push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in + (* Jason Gross: To avoid unnecessary modifications to tacinterp, as + suggested by Arnaud Spiwack, we run push_trace immediately. We do + this with the kludge of an empty proofview, and rely on the + invariant that running the tactic returned by push_trace does + not modify sigma. *) + let (_, dummy_proofview) = Proofview.init sigma [] in + let (trace,_,_,_) = Proofview.apply env (push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist) dummy_proofview in let (evd,c) = catch_error trace (understand_ltac flags env sigma vars kind) c in @@ -1169,7 +1176,9 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacAtom (loc,t) -> let call = LtacAtomCall t in - catch_error_tac (push_trace(loc,call) ist) (interp_atomic ist t) + push_trace(loc,call) ist >>= fun trace -> + Profile_ltac.do_profile "eval_tactic:2" trace + (catch_error_tac trace (interp_atomic ist t)) | TacFun _ | TacLetIn _ -> assert false | TacMatchGoal _ | TacMatch _ -> assert false | TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) []) @@ -1251,7 +1260,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let tac l = let addvar x v accu = Id.Map.add x v accu in let lfun = List.fold_right2 addvar ids l ist.lfun in - let trace = push_trace (loc,LtacNotationCall s) ist in + Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace -> let ist = { lfun = lfun; extra = TacStore.set ist.extra f_trace trace; } in @@ -1276,7 +1285,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Ftactic.run tac (fun () -> Proofview.tclUNIT ()) | TacML (loc,opn,l) -> - let trace = push_trace (loc,LtacMLCall tac) ist in + push_trace (loc,LtacMLCall tac) ist >>= fun trace -> let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in let tac = Tacenv.interp_ml_tactic opn in let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in @@ -1302,15 +1311,17 @@ and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t = try Id.Map.find id ist.lfun with Not_found -> in_gen (topwit wit_var) id in - Ftactic.bind (force_vrec ist v) begin fun v -> - let v = propagate_trace ist loc id v in + let open Ftactic in + force_vrec ist v >>= begin fun v -> + Ftactic.lift (propagate_trace ist loc id v) >>= fun v -> if mustbetac then Ftactic.return (coerce_to_tactic loc id v) else Ftactic.return v end | ArgArg (loc,r) -> let ids = extract_ids [] ist.lfun in let loc_info = ((if Loc.is_ghost loc' then loc else loc'),LtacNameCall r) in let extra = TacStore.set ist.extra f_avoid_ids ids in - let extra = TacStore.set extra f_trace (push_trace loc_info ist) in + push_trace loc_info ist >>= fun trace -> + 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) @@ -1408,7 +1419,7 @@ and tactic_of_value ist vle = lfun = lfun; extra = TacStore.set ist.extra f_trace []; } in let tac = name_if_glob appl (eval_tactic ist t) in - catch_error_tac trace tac + Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac) | (VFun _|VRec _) -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") else if has_type vle (topwit wit_tactic) then let tac = out_gen (topwit wit_tactic) vle in diff --git a/ltacprof/ltacprof.mllib b/ltacprof/ltacprof.mllib new file mode 100644 index 000000000..383e5d285 --- /dev/null +++ b/ltacprof/ltacprof.mllib @@ -0,0 +1 @@ +Profile_ltac diff --git a/ltacprof/profile_ltac.ml b/ltacprof/profile_ltac.ml new file mode 100644 index 000000000..889ae77b8 --- /dev/null +++ b/ltacprof/profile_ltac.ml @@ -0,0 +1,286 @@ +open Pp +open Printer +open Util + + +let is_profiling = ref false +let set_profiling b = is_profiling := b + +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} +let stack = ref [{entry=empty_entry(); children=Hashtbl.create 20}] + +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 option_start_time_add_total c = + (match option_start_time_add_total with + | Some (start_time, add_total) -> begin + 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() + end + | None -> () + ) + +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)) >>= fun option_start_time_add_total -> + tclFINALLY + tac + (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + (match call_trace with + | (_, c) :: _ -> + exit_tactic option_start_time_add_total c + | [] -> ())))) + + + +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 new file mode 100644 index 000000000..dd750517e --- /dev/null +++ b/ltacprof/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 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/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v new file mode 100644 index 000000000..6b73443d6 --- /dev/null +++ b/test-suite/success/ltacprof.v @@ -0,0 +1,8 @@ +(** Some LtacProf tests *) + +Start Profiling. +Ltac multi := (idtac + idtac). +Goal True. + try (multi; fail). (* Anomaly: Uncaught exception Failure("hd"). Please report. *) +Admitted. +Show Profile. diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 7b76514e4..91bb88753 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -49,8 +49,9 @@ let section s = let lib_dirs = ["kernel"; "lib"; "library"; "parsing"; "pretyping"; "interp"; "printing"; "intf"; - "proofs"; "tactics"; "tools"; "toplevel"; - "stm"; "grammar"; "config"; "ltac"; "engine"] + "proofs"; "tactics"; "tools"; "ltacprof"; + "toplevel"; "stm"; "grammar"; "config"; + "ltac"; "engine"] let usage () = diff --git a/tools/coqc.ml b/tools/coqc.ml index f957200ab..7210efc4f 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" + | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profileltac" |"-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 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