diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-09-29 14:32:50 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-09-29 14:36:33 -0400 |
| commit | 46daf37ed46397b03a30fa2d89b62ffcc2c8d166 (patch) | |
| tree | aae47a61675ba940388ecc35e206c138f6cbaf17 | |
| parent | edb55a94fc5c0473e57f5a61c0c723194c2ff414 (diff) | |
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.
| -rw-r--r-- | lib/flags.ml | 2 | ||||
| -rw-r--r-- | test-suite/Makefile | 2 | ||||
| -rw-r--r-- | 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 af55e9e2b..65873e521 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 a40ea80ae..d2899034b 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 d79451f0f..6611db70e 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'. |