Make Ltac Profiling an setting

5 files changed, 39 insertions, 35 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 608793d04f..ffcb371346 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1197,27 +1197,27 @@ 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\comindex{Start Profiling}\comindex{Stop Profiling}\comindex{Show Profile}\comindex{Reset Profile}}
+\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 Start Profiling}.
+{\tt Set Ltac Profiling}.
 \end{quote}
 Enables the profiler
 
 \begin{quote}
-{\tt Stop Profiling}.
+{\tt Unset Ltac Profiling}.
 \end{quote}
 Disables the profiler
 
 \begin{quote}
-{\tt Show Profile}.
+{\tt Show Ltac Profile}.
 \end{quote}
 Prints the profile
 
 \begin{quote}
-{\tt Show Profile} {\qstring}.
+{\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.
 
@@ -1245,34 +1245,34 @@ 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,
 Proof.
 \end{coq_example*}
 \begin{coq_example}
-  Start Profiling.
+  Set Ltac Profiling.
   tac.
 \end{coq_example}
 {\let\textit\texttt% use tt mode for the output of ltacprof
 \begin{coq_example}
-  Show Profile.
+  Show Ltac Profile.
 \end{coq_example}
 \begin{coq_example}
-  Show Profile "omega".
+  Show Ltac Profile "omega".
 \end{coq_example}
 }
 \begin{coq_example*}
 Abort.
-Stop Profiling.
+Unset Ltac Profiling.
 \end{coq_example*}
 
-\tacindex{start profiling}\tacindex{stop profiling}
+\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 profiling}.
+{\tt start ltac profiling}.
 \end{quote}
 
 \begin{quote}
-{\tt stop profiling}.
+{\tt stop ltac profiling}.
 \end{quote}
 
-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.
+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/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4
index ce00c29202..b83ab8c520 100644
--- a/ltac/profile_ltac_tactics.ml4
+++ b/ltac/profile_ltac_tactics.ml4
@@ -9,32 +9,32 @@ let tclSET_PROFILING b =
    Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
    set_profiling b))
 
-TACTIC EXTEND start_profiling
-  | [ "start" "profiling" ] -> [ tclSET_PROFILING true  ]
+TACTIC EXTEND start_ltac_profiling
+  | [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true  ]
 END
 
 TACTIC EXTEND stop_profiling
-  | [ "stop" "profiling" ] ->  [ tclSET_PROFILING false ]
+  | [ "stop" "ltac" "profiling" ] ->  [ tclSET_PROFILING false ]
 END;;
 
-
-VERNAC COMMAND EXTEND StartProfiling CLASSIFIED AS SIDEFF
- [ "Start" "Profiling" ] -> [ 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() ]
+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
 
-VERNAC COMMAND EXTEND ShowProfile CLASSIFIED AS QUERY
- [ "Show" "Profile" ] -> [ print_results() ]
+VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY
+ [ "Show" "Ltac" "Profile" ] -> [ print_results() ]
 END
 
 
-VERNAC COMMAND EXTEND ShowProfileTactic CLASSIFIED AS QUERY
- [ "Show" "Profile" string(s) ] -> [ print_results_tactic s ]
+VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY
+ [ "Show" "Ltac" "Profile" string(s) ] -> [ print_results_tactic s ]
 END
diff --git a/ltacprof/profile_ltac.ml b/ltacprof/profile_ltac.ml
index 6ae07689dd..97d74ad80f 100644
--- a/ltacprof/profile_ltac.ml
+++ b/ltacprof/profile_ltac.ml
@@ -3,9 +3,11 @@ 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. *)
-let is_profiling = Summary.ref false ~name:"is-profiling-ltac"
+(** [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
diff --git a/ltacprof/profile_ltac.mli b/ltacprof/profile_ltac.mli
index dd750517e3..65c067e860 100644
--- a/ltacprof/profile_ltac.mli
+++ b/ltacprof/profile_ltac.mli
@@ -2,6 +2,8 @@ val do_profile : string -> ('a * Tacexpr.ltac_call_kind) list -> 'b Proofview.ta
 
 val set_profiling : bool -> unit
 
+val get_profiling : unit -> bool
+
 val set_display_profile_at_close : bool -> unit
 
 val entered_call : unit -> unit
diff --git a/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v
index 6b73443d6a..ae11358eda 100644
--- a/test-suite/success/ltacprof.v
+++ b/test-suite/success/ltacprof.v
@@ -1,8 +1,8 @@
 (** Some LtacProf tests *)
 
-Start Profiling.
+Set Ltac Profiling.
 Ltac multi := (idtac + idtac).
 Goal True.
   try (multi; fail). (* Anomaly: Uncaught exception Failure("hd"). Please report. *)
 Admitted.
-Show Profile.
+Show Ltac Profile.