Merge PR #6380: Add tactics to reset and display the Ltac profile

4 files changed, 52 insertions, 3 deletions

diff --git a/CHANGES b/CHANGES
index e03ab683c4..24f3580787 100644
--- a/CHANGES
+++ b/CHANGES
@@ -34,6 +34,7 @@ Tactics
 - The tactic "romega" is also aware now of the bodies of context variables.
 - Tactic "decide equality" now able to manage constructors which
   contain proofs.
+- Added tactics reset ltac profile, show ltac profile (and variants)
 
 Vernacular Commands
 
@@ -288,7 +289,7 @@ Changes from 8.6 to 8.6.1
 - Fix bug 5550: "typeclasses eauto with" does not work with section variables.
 - Bug 5546, qualify datatype constructors when needed in Show Match
 - Bug #5535, test for Show with -emacs
-- Fix bug #5486, don't reverse ids in tuples 
+- Fix bug #5486, don't reverse ids in tuples
 - Fixing #5522 (anomaly with free vars of pat)
 - Fix bug #5526, don't check for nonlinearity in notation if printing only
 - Fix bug #5255
@@ -310,7 +311,7 @@ Changes from 8.6 to 8.6.1
 - show unused intro pattern warning
 - [future] Be eager when "chaining" already resolved future values.
 - Opaque side effects
-- Fix #5132: coq_makefile generates incorrect install goal 
+- Fix #5132: coq_makefile generates incorrect install goal
 - Run non-tactic comands without resilient_command
 - Univs: fix bug #5365, generation of u+k <= v constraints
 - make `emit' tail recursive
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 8d82460a72..00430c07f6 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1358,6 +1358,21 @@ The following two tactics behave like {\tt idtac} but enable and disable the pro
 {\tt stop ltac profiling}.
 \end{quote}
 
+\tacindex{reset ltac profile}\tacindex{show ltac profile}
+The following tactics behave like the corresponding vernacular commands and allow displaying and resetting the profile from tactic scripts for benchmarking purposes.
+
+\begin{quote}
+{\tt reset ltac profile}.
+\end{quote}
+
+\begin{quote}
+{\tt show ltac profile}.
+\end{quote}
+
+\begin{quote}
+{\tt show ltac profile} {\qstring}.
+\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.
diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4
index f095660638..58e3a3a57e 100644
--- a/plugins/ltac/profile_ltac_tactics.ml4
+++ b/plugins/ltac/profile_ltac_tactics.ml4
@@ -18,6 +18,15 @@ 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))
+
 TACTIC EXTEND start_ltac_profiling
 | [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ]
 END
@@ -26,8 +35,18 @@ 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
+
 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/test-suite/bugs/closed/6378.v b/test-suite/bugs/closed/6378.v
index d0ef090d08..68ae7961dd 100644
--- a/test-suite/bugs/closed/6378.v
+++ b/test-suite/bugs/closed/6378.v
@@ -1,4 +1,18 @@
+Require Import Coq.ZArith.ZArith.
+Ltac profile_constr tac :=
+  let dummy := match goal with _ => reset ltac profile; start ltac profiling end in
+  let ret := match goal with _ => tac () end in
+  let dummy := match goal with _ => stop ltac profiling; show ltac profile end in
+  pose 1.
+
+Ltac slow _ := eval vm_compute in (Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl).
+
 Goal True.
   start ltac profiling.
+  reset ltac profile.
+  reset ltac profile.
   stop ltac profiling.
+  time profile_constr slow.
+  show ltac profile cutoff 0.
+  show ltac profile "slow".
 Abort.