diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 11:59:59 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 11:59:59 +0200 |
| commit | 367e1f913f8d0b921dc4902b83d889dac3576580 (patch) | |
| tree | 5b8ee1687a24d6cb011fbc9ce383ef8d9affec6f | |
| parent | 10545881bb05aedafc512e211a4df9e7433750e7 (diff) | |
| parent | 46daf37ed46397b03a30fa2d89b62ffcc2c8d166 (diff) | |
Merge remote-tracking branch 'github/pr/302' into v8.6
Was PR#302: Set the default LtacProf cutoff to 2%
| -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 acf1dae05..9d7444d7a 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'. |