Merge branch "LtacProf for trunk" (PR #165).

18 files changed, 608 insertions, 28 deletions

diff --git a/.gitignore b/.gitignore
index 1cbf56e3c..0193c9dfa 100644
--- a/.gitignore
+++ b/.gitignore
@@ -127,6 +127,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/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 12dea9a30..ffcb37134 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -78,7 +78,7 @@ For instance
 {\tt try repeat \tac$_1$ ||
   \tac$_2$;\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$];\tac$_4$.}
 \end{quote}
-is understood as 
+is understood as
 \begin{quote}
 {\tt (try (repeat (\tac$_1$ || \tac$_2$)));} \\
 {\tt ((\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$]);\tac$_4$).}
@@ -174,7 +174,7 @@ is understood as
 \\
 {\messagetoken}\!\!\!\!\!\! & ::= & {\qstring} ~|~ {\ident} ~|~ {\integer} \\
 \\
-\tacarg & ::= & 
+\tacarg & ::= &
         {\qualid}\\
 & $|$ & {\tt ()} \\
 & $|$ & {\tt ltac :} {\atom}\\
@@ -344,7 +344,7 @@ for $=1,...,n$. It fails if the number of focused goals is not exactly $n$.
     expects multiple goals, such as {\tt swap}, would act as if a single
     goal is focused.
 
-  \item {\tacexpr} {\tt ; [ } {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]} 
+  \item {\tacexpr} {\tt ; [ } {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
 
     This variant of local tactic application is paired with a
     sequence.  In this variant, $n$ must be the number of goals
@@ -782,7 +782,7 @@ setting option {\tt Printing All}, see Section~\ref{SetPrintingAll}).
 \begin{coq_example}
 Ltac f x :=
   match x with
-    context f [S ?X] => 
+    context f [S ?X] =>
     idtac X;                    (* To display the evaluation order *)
     assert (p := eq_refl 1 : X=1);    (* To filter the case X=1 *)
     let x:= context f[O] in assert (x=O) (* To observe the context *)
@@ -1026,7 +1026,7 @@ Reset Initial.
 \index{Tacticals!abstract@{\tt abstract}}}
 
 From the outside ``\texttt{abstract \tacexpr}'' is the same as
-{\tt solve \tacexpr}. Internally it saves an auxiliary lemma called 
+{\tt solve \tacexpr}. Internally it saves an auxiliary lemma called
 {\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the
 current goal and \textit{n} is chosen so that this is a fresh name.
 Such auxiliary lemma is inlined in the final proof term
@@ -1196,6 +1196,86 @@ s: & continue current evaluation without stopping\\
 r $n$: & advance $n$ steps further\\
 r {\qstring}: & advance up to the next call to ``{\tt idtac} {\qstring}''\\
 \end{tabular}
+
+\subsection[Profiling {\ltac} tactics]{Profiling {\ltac} tactics\optindex{Ltac Profiling}\comindex{Show Ltac Profile}\comindex{Reset Ltac Profile}}
+
+It is possible to measure the time spent in invocations of primitive tactics as well as tactics defined in {\ltac} and their inner invocations. The primary use is the development of complex tactics, which can sometimes be so slow as to impede interactive usage. The reasons for the performence degradation can be intricate, like a slowly performing {\ltac} match or a sub-tactic whose performance only degrades in certain situations. The profiler generates a call tree and indicates the time spent in a tactic depending its calling context. Thus it allows to locate the part of a tactic definition that contains the performance bug.
+
+\begin{quote}
+{\tt Set Ltac Profiling}.
+\end{quote}
+Enables the profiler
+
+\begin{quote}
+{\tt Unset Ltac Profiling}.
+\end{quote}
+Disables the profiler
+
+\begin{quote}
+{\tt Show Ltac Profile}.
+\end{quote}
+Prints the profile
+
+\begin{quote}
+{\tt Show Ltac Profile} {\qstring}.
+\end{quote}
+Prints a profile for all tactics that start with {\qstring}. Append a period (.) to the string if you only want exactly that name.
+
+\begin{quote}
+{\tt Reset Profile}.
+\end{quote}
+Resets the profile, that is, deletes all accumulated information
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{coq_example*}
+Require Import Coq.omega.Omega.
+
+Ltac mytauto := tauto.
+Ltac tac := intros; repeat split; omega || mytauto.
+
+Notation max x y := (x + (y - x)) (only parsing).
+\end{coq_example*}
+\begin{coq_example*}
+Goal forall x y z A B C D E F G H I J K L M N O P Q R S T U V W X Y Z,
+    max x (max y z) = max (max x y) z /\ max x (max y z) = max (max x y) z
+    /\ (A /\ B /\ C /\ D /\ E /\ F /\ G /\ H /\ I /\ J /\ K /\ L /\ M /\ N /\ O /\ P /\ Q /\ R /\ S /\ T /\ U /\ V /\ W /\ X /\ Y /\ Z
+        -> Z /\ Y /\ X /\ W /\ V /\ U /\ T /\ S /\ R /\ Q /\ P /\ O /\ N /\ M /\ L /\ K /\ J /\ I /\ H /\ G /\ F /\ E /\ D /\ C /\ B /\ A).
+Proof.
+\end{coq_example*}
+\begin{coq_example}
+  Set Ltac Profiling.
+  tac.
+\end{coq_example}
+{\let\textit\texttt% use tt mode for the output of ltacprof
+\begin{coq_example}
+  Show Ltac Profile.
+\end{coq_example}
+\begin{coq_example}
+  Show Ltac Profile "omega".
+\end{coq_example}
+}
+\begin{coq_example*}
+Abort.
+Unset Ltac Profiling.
+\end{coq_example*}
+
+\tacindex{start ltac profiling}\tacindex{stop ltac profiling}
+The following two tactics behave like {\tt idtac} but enable and disable the profiling. They allow you to exclude parts of a proof script from profiling.
+
+\begin{quote}
+{\tt start ltac profiling}.
+\end{quote}
+
+\begin{quote}
+{\tt stop ltac profiling}.
+\end{quote}
+
+You can also pass the {\tt -profile-ltac} command line option to {\tt coqc}, which performs a {\tt Set Ltac Profiling} at the beginning of each document, and a {\tt Show Ltac 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.
+
 \endinput
 
 \subsection{Permutation on closed lists}
@@ -1229,7 +1309,7 @@ Another more complex example is the problem of permutation on closed
 lists. The aim is to show that a closed list is a permutation of
 another one.  First, we define the permutation predicate as shown on
 Figure~\ref{permutpred}.
- 
+
 \begin{figure}[p]
 \begin{center}
 \fbox{\begin{minipage}{0.95\textwidth}
@@ -1555,7 +1635,7 @@ Figure~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}.
 \begin{center}
 \fbox{\begin{minipage}{0.95\textwidth}
 \begin{coq_example*}
-Lemma isos_ex1 : 
+Lemma isos_ex1 :
   forall A B:Set, A * unit * B = B * (unit * A).
 Proof.
 intros; IsoProve.
@@ -1575,7 +1655,7 @@ Qed.
 \label{isoslem}
 \end{figure}
 
-%%% Local Variables: 
+%%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
-%%% End: 
+%%% End:
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/lib/unicode.ml b/lib/unicode.ml
index 7aa8d9d51..dc852d981 100644
--- a/lib/unicode.ml
+++ b/lib/unicode.ml
@@ -261,3 +261,73 @@ let ascii_of_ident s =
         (Buffer.add_char out s.[!i]; incr i)
     done;
     Buffer.contents out
+
+(* Compute length of an UTF-8 encoded string
+   Rem 1 : utf8_length <= String.length (equal if pure ascii)
+   Rem 2 : if used for an iso8859_1 encoded string, the result is
+   wrong in very rare cases. Such a wrong case corresponds to any
+   sequence of a character in range 192..253 immediately followed by a
+   character in range 128..191 (typical case in french is "déçu" which
+   is counted 3 instead of 4); then no real harm to use always
+   utf8_length even if using an iso8859_1 encoding *)
+
+(** FIXME: duplicate code with Pp *)
+
+let utf8_length s =
+  let len = String.length s
+  and cnt = ref 0
+  and nc = ref 0
+  and p = ref 0 in
+  while !p < len do
+    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 && !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 ;
+  !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)
diff --git a/lib/unicode.mli b/lib/unicode.mli
index aaf455dec..1f8bd44ee 100644
--- a/lib/unicode.mli
+++ b/lib/unicode.mli
@@ -40,3 +40,9 @@ val ascii_of_ident : string -> string
 
 (** Validate an UTF-8 string *)
 val is_utf8 : string -> bool
+
+(** Return the length of a valid UTF-8 string. *)
+val utf8_length : string -> int
+
+(** Variant of {!String.sub} for UTF-8 strings. *)
+val utf8_sub : string -> int -> int -> string
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..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
@@ -10,6 +11,7 @@ Extraargs
 G_obligations
 Coretactics
 Extratactics
+Profile_ltac_tactics
 G_auto
 G_class
 Rewrite
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
new file mode 100644
index 000000000..7a8ef32c3
--- /dev/null
+++ b/ltac/profile_ltac.ml
@@ -0,0 +1,323 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+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
+
+(** 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 empty_treenode n = { entry = empty_entry (); children = Hashtbl.create n }
+
+(** 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. *)
+(** TODO: rewrite me in purely functional style *)
+let deepcopy_entry { total; local; ncalls; max_total } =
+  { total; local; ncalls; max_total }
+
+let rec deepcopy_treenode { entry; children } =
+  let children' = Hashtbl.create (Hashtbl.length children) in
+  let iter key subtree = Hashtbl.add children' key (deepcopy_treenode subtree) in
+  let () = Hashtbl.iter iter children in
+  { entry = deepcopy_entry entry; children = children' }
+
+let stack =
+  let freeze _ = List.map deepcopy_treenode in
+  Summary.ref ~freeze [empty_treenode 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 = empty_treenode 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 msgnl_with fmt strm = msg_with fmt (strm ++ fnl ())
+let msgnl          strm = msgnl_with !Pp_control.std_ft strm
+
+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 = match !stack with
+| [] | [_] ->
+  (* oops, our stack is invalid *)
+  encounter_multi_success_backtracking ()
+| node :: (parent :: _ as stack') ->
+  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;
+  let node' = { total = diff; local = diff; ncalls = 1; max_total = diff } in
+  add_entry node.entry add_total node'
+
+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 =
+  str " tactic                                    self  total   calls       max" ++
+  fnl () ++
+  str "────────────────────────────────────────┴──────┴──────┴───────┴─────────┘"
+
+let rec print_node all_total indent prefix (s, n) =
+  let e = n.entry in
+  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 fold s n l = if n.entry.total /. all_total < 0.02 then l else (s, n) :: l in
+  let ls = Hashtbl.fold fold 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
+    let iter is_last =
+      let sep0 = if first_level then "" else if is_last then "  " else " │" in
+      let sep1 = if first_level then "─" else if is_last then " └─" else " ├─" in
+      print_node all_total (indent ^ sep0) (indent ^ sep1)
+    in
+    prlist_with_sep fnl (fun pr -> pr) (list_iter_is_last iter 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 =
+    let iter s node =
+      let node' = get_node s global in
+      add_entry node'.entry true node.entry;
+      cumulate node.children
+    in
+    Hashtbl.iter iter table
+  in
+  cumulate tree;
+  warn_encountered_multi_success_backtracking ();
+  let msg =
+    h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
+    fnl () ++
+    header ++
+    print_table all_total "" true global ++
+    fnl () ++
+    header ++
+    print_table all_total "" true tree
+  in
+  Feedback.msg_notice msg
+  (* 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 =
+    let iter 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
+    in
+    Hashtbl.iter iter 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 ();
+  let msg =
+    h 0 (str"total time:           " ++ padl 11 (format_sec (all_total))) ++
+    h 0 (str"time spent in tactic: " ++ padl 11 (format_sec (tactic_total))) ++
+    fnl () ++
+    header ++
+    print_table tactic_total "" true table_tactic
+  in
+  Feedback.msg_notice msg
+
+let reset_profile () =
+  stack := [empty_treenode 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..7bbdca942
--- /dev/null
+++ b/ltac/profile_ltac.mli
@@ -0,0 +1,25 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Ltac profiling primitives *)
+
+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
new file mode 100644
index 000000000..c092a0cb6
--- /dev/null
+++ b/ltac/profile_ltac_tactics.ml4
@@ -0,0 +1,39 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i camlp4deps: "grammar/grammar.cma" i*)
+
+(** Ltac profiling entrypoints *)
+
+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_ltac_profiling
+| [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ]
+END
+
+TACTIC EXTEND stop_profiling
+| [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ]
+END
+
+VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF
+  [ "Reset" "Ltac" "Profile" ] -> [ reset_profile() ]
+END
+
+VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY
+  [ "Show" "Ltac" "Profile" ] -> [ print_results() ]
+END
+
+VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY
+  [ "Show" "Ltac" "Profile" string(s) ] -> [ print_results_tactic s ]
+END
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 5ee9b0fc4..ab61c8abb 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
+      let extra = TacStore.set ist.extra f_avoid_ids ids 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/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v
new file mode 100644
index 000000000..d5552695c
--- /dev/null
+++ b/test-suite/success/ltacprof.v
@@ -0,0 +1,8 @@
+(** Some LtacProf tests *)
+
+Set Ltac Profiling.
+Ltac multi := (idtac + idtac).
+Goal True.
+  try (multi; fail). (* Used to result in: Anomaly: Uncaught exception Failure("hd"). Please report. *)
+Admitted.
+Show Ltac Profile.
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 32c22f9e6..45e843e60 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -50,8 +50,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..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"
+    | ("-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 869f6bb93..aab20650a 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
+    |"-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
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index f855c096e..5359a288a 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  -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\"\