From 46daf37ed46397b03a30fa2d89b62ffcc2c8d166 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 29 Sep 2016 14:32:50 -0400
Subject: Set the default LtacProf cutoff to 2%

This was the original value from Tobias' code.  When a user passes
-profile-ltac on the command line, or inserts [Show Ltac Profile] in the
document, the most useful default behavior is to not overload them with
useless information.  When GUI clients want to display fancier profiling
information, there is no cost to the user to requiring them to specify
what cutoff they want.  If the GUI client does not have any special
LtacProf handling, the most useful presentation is again the one that
cuts off the display at 2% total time.
---
 lib/flags.ml                             | 2 +-
 test-suite/Makefile                      | 2 +-
 test-suite/output-modulo-time/ltacprof.v | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/lib/flags.ml b/lib/flags.ml
index af55e9e2bb..65873e5214 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -231,7 +231,7 @@ let print_mod_uid = ref false
 
 let tactic_context_compat = ref false
 let profile_ltac = ref false
-let profile_ltac_cutoff = ref 0.0
+let profile_ltac_cutoff = ref 2.0
 
 let dump_bytecode = ref false
 let set_dump_bytecode = (:=) dump_bytecode
diff --git a/test-suite/Makefile b/test-suite/Makefile
index a40ea80ae4..d2899034b8 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -51,7 +51,7 @@ SINGLE_QUOTE="
 get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_args,$(1)), ($(call get_coq_prog_args,$(1)))))
 # get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop
 has_compile_flag = $(filter "-compile",$(call get_coq_prog_args,$(1)))
-has_profile_ltac_or_compile_flag = $(filter "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1)))
+has_profile_ltac_or_compile_flag = $(filter "-profile-ltac-cutoff" "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1)))
 get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqc),$(command))
 
 
diff --git a/test-suite/output-modulo-time/ltacprof.v b/test-suite/output-modulo-time/ltacprof.v
index d79451f0f7..6611db70e2 100644
--- a/test-suite/output-modulo-time/ltacprof.v
+++ b/test-suite/output-modulo-time/ltacprof.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-profile-ltac") -*- *)
+(* -*- coq-prog-args: ("-emacs" "-profile-ltac-cutoff" "0.0") -*- *)
 Ltac sleep' := do 100 (do 100 (do 100 idtac)).
 Ltac sleep := sleep'.
 
-- 
cgit v1.2.3