From 5348a615a484e379896deac8a6944af1f92b2d4c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Sep 2016 17:58:06 +0200 Subject: test-suite: fix sed on OS X, does not handle + --- test-suite/Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'test-suite/Makefile') diff --git a/test-suite/Makefile b/test-suite/Makefile index 1dfbb29ff..a40ea80ae 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -304,16 +304,16 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ | grep -v "^" \ - | sed -e 's/\s*[0-9]*\.[0-9]\+\s*//g' \ + | sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \ -e 's/\s*0\.\s*//g' \ -e 's/\s*[-+]nan\s*//g' \ -e 's/\s*[-+]inf\s*//g' \ > $$tmpoutput; \ - sed -e 's/\s*[0-9]*\.[0-9]\+\s*//g' \ + sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \ -e 's/\s*0\.\s*//g' \ -e 's/\s*[-+]nan\s*//g' \ -e 's/\s*[-+]inf\s*//g' \ - $*.out > $$tmpexpected; \ + $*.out > $$tmpexpected; \ diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ -- cgit v1.2.3 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(-) (limited to 'test-suite/Makefile') 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'. -- cgit v1.2.3 From c4c7aa6d7b14a6d76c287b97d487abe055406577 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 29 Sep 2016 18:28:24 -0400 Subject: LtacProf cutoff is for total percent, not time --- ltac/profile_ltac.ml | 4 +-- test-suite/Makefile | 4 +-- test-suite/output-modulo-time/ltacprof_cutoff.out | 33 +++++++++++++++++++++++ test-suite/output-modulo-time/ltacprof_cutoff.v | 12 +++++++++ 4 files changed, 49 insertions(+), 4 deletions(-) create mode 100644 test-suite/output-modulo-time/ltacprof_cutoff.out create mode 100644 test-suite/output-modulo-time/ltacprof_cutoff.v (limited to 'test-suite/Makefile') diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index a91ff98fb..2514ededb 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -128,7 +128,7 @@ let to_ltacprof_results xml = | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML") let feedback_results results = - Feedback.(feedback + Feedback.(feedback (Custom (Loc.dummy_loc, "ltacprof_results", of_ltacprof_results results))) (* ************** pretty printing ************************************* *) @@ -218,7 +218,7 @@ let to_string ~filter ?(cutoff=0.0) node = !global in warn_encountered_multi_success_backtracking (); - let filter s n = filter s && n >= cutoff in + let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in let msg = h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++ fnl () ++ diff --git a/test-suite/Makefile b/test-suite/Makefile index a40ea80ae..e3800ee22 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -304,12 +304,12 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ | grep -v "^" \ - | sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \ + | sed -e 's/\s*[-+0-9]*\.[0-9][0-9]*\s*//g' \ -e 's/\s*0\.\s*//g' \ -e 's/\s*[-+]nan\s*//g' \ -e 's/\s*[-+]inf\s*//g' \ > $$tmpoutput; \ - sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \ + sed -e 's/\s*[-+0-9]*\.[0-9][0-9]*\s*//g' \ -e 's/\s*0\.\s*//g' \ -e 's/\s*[-+]nan\s*//g' \ -e 's/\s*[-+]inf\s*//g' \ diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.out b/test-suite/output-modulo-time/ltacprof_cutoff.out new file mode 100644 index 000000000..13cd87b8c --- /dev/null +++ b/test-suite/output-modulo-time/ltacprof_cutoff.out @@ -0,0 +1,33 @@ +total time: 1.584s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─sleep --------------------------------- 100.0% 100.0% 3 0.572s +─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s +─foo1 ---------------------------------- 0.0% 63.9% 1 1.012s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s +└foo1 ---------------------------------- 0.0% 63.9% 1 1.012s + +total time: 1.584s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─sleep --------------------------------- 100.0% 100.0% 3 0.572s +─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s +─foo1 ---------------------------------- 0.0% 63.9% 1 1.012s +─foo0 ---------------------------------- 0.0% 31.3% 1 0.496s +─constructor --------------------------- 0.0% 0.0% 1 0.000s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s + ├─foo1 -------------------------------- 0.0% 63.9% 1 1.012s + │ ├─sleep ----------------------------- 32.6% 32.6% 1 0.516s + │ └─foo0 ------------------------------ 0.0% 31.3% 1 0.496s + │ └sleep ----------------------------- 31.3% 31.3% 1 0.496s + └─sleep ------------------------------- 36.1% 36.1% 1 0.572s +─constructor --------------------------- 0.0% 0.0% 1 0.000s + diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v new file mode 100644 index 000000000..50131470e --- /dev/null +++ b/test-suite/output-modulo-time/ltacprof_cutoff.v @@ -0,0 +1,12 @@ +(* -*- coq-prog-args: ("-emacs" "-profile-ltac") -*- *) +Require Coq.ZArith.BinInt. +Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac). + +Ltac foo0 := idtac; sleep. +Ltac foo1 := sleep; foo0. +Ltac foo2 := sleep; foo1. +Goal True. + foo2. + Show Ltac Profile CutOff 47. + constructor. +Qed. -- cgit v1.2.3 From 775b8f28562d1d5063da2b28a06e59610b76f06f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 30 Sep 2016 10:14:10 +0200 Subject: Ignore file names in warning emitted by test-suite/output/* (#5111) --- test-suite/Makefile | 2 +- test-suite/output/Arguments_renaming.out | 18 +++++++++--------- 2 files changed, 10 insertions(+), 10 deletions(-) (limited to 'test-suite/Makefile') diff --git a/test-suite/Makefile b/test-suite/Makefile index a40ea80ae..6ecc7bcaa 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -280,7 +280,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ - | grep -v "^" \ + | sed 's/File "[^"]*"/File "stdin"/' \ > $$tmpoutput; \ diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 815305581..1633ad976 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,20 +1,20 @@ -File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 1, characters 0-36: +File "stdin", line 1, characters 0-36: Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. -[arguments-assert,vernacular] +[arguments-ignore-rename-nonimpl,vernacular] The command has indeed failed with message: Error: To rename arguments the "rename" flag must be specified. Argument A renamed to B. -File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25: +File "stdin", line 2, characters 0-25: Warning: Ignoring rename of A into T. Only implicit arguments can be renamed. -[arguments-assert,vernacular] -File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25: +[arguments-ignore-rename-nonimpl,vernacular] +File "stdin", line 2, characters 0-25: Warning: This command is just asserting the number and names of arguments of identity. If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes' [arguments-assert,vernacular] -File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 4, characters 0-40: +File "stdin", line 4, characters 0-40: Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. -[arguments-assert,vernacular] +[arguments-ignore-rename-nonimpl,vernacular] @eq_refl : forall (B : Type) (y : B), y = y eq_refl @@ -121,9 +121,9 @@ The command has indeed failed with message: Error: Argument z cannot be declared implicit. The command has indeed failed with message: Error: Extra argument y. -File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 53, characters 0-26: +File "stdin", line 53, characters 0-26: Warning: Ignoring rename of x into s. Only implicit arguments can be renamed. -[arguments-assert,vernacular] +[arguments-ignore-rename-nonimpl,vernacular] The command has indeed failed with message: Error: To rename arguments the "rename" flag must be specified. Argument A renamed to R. -- cgit v1.2.3 From 69d43e7615f080c2e4e57a87e84b51be857ab678 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 30 Sep 2016 11:08:47 +0200 Subject: Restore code ignoring lines in output (camlp5 warnings) --- test-suite/Makefile | 1 + 1 file changed, 1 insertion(+) (limited to 'test-suite/Makefile') diff --git a/test-suite/Makefile b/test-suite/Makefile index 6ecc7bcaa..acf1dae05 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -280,6 +280,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ + | grep -v "^" \ | sed 's/File "[^"]*"/File "stdin"/' \ > $$tmpoutput; \ diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \ -- cgit v1.2.3 From 98da77db53b4a41062c47f8f55418eb1fbb7e5bb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 30 Sep 2016 16:19:45 +0200 Subject: test-suite/output-modulo-time made more robust Order of items made stable --- test-suite/Makefile | 5 ++++- test-suite/output-modulo-time/ltacprof_cutoff.out | 4 +--- 2 files changed, 5 insertions(+), 4 deletions(-) (limited to 'test-suite/Makefile') diff --git a/test-suite/Makefile b/test-suite/Makefile index efa0236c3..b32071e80 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -309,12 +309,15 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out -e 's/\s*0\.\s*//g' \ -e 's/\s*[-+]nan\s*//g' \ -e 's/\s*[-+]inf\s*//g' \ + -e 's/^[^a-zA-Z]*//' \ + | sort \ > $$tmpoutput; \ sed -e 's/\s*[-+0-9]*\.[0-9][0-9]*\s*//g' \ -e 's/\s*0\.\s*//g' \ -e 's/\s*[-+]nan\s*//g' \ -e 's/\s*[-+]inf\s*//g' \ - $*.out > $$tmpexpected; \ + -e 's/^[^a-zA-Z]*//' \ + $*.out | sort > $$tmpexpected; \ diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.out b/test-suite/output-modulo-time/ltacprof_cutoff.out index 13cd87b8c..0cd5777cc 100644 --- a/test-suite/output-modulo-time/ltacprof_cutoff.out +++ b/test-suite/output-modulo-time/ltacprof_cutoff.out @@ -2,8 +2,8 @@ total time: 1.584s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─sleep --------------------------------- 100.0% 100.0% 3 0.572s ─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s +─sleep --------------------------------- 100.0% 100.0% 3 0.572s ─foo1 ---------------------------------- 0.0% 63.9% 1 1.012s tactic local total calls max @@ -19,7 +19,6 @@ total time: 1.584s ─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s ─foo1 ---------------------------------- 0.0% 63.9% 1 1.012s ─foo0 ---------------------------------- 0.0% 31.3% 1 0.496s -─constructor --------------------------- 0.0% 0.0% 1 0.000s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ @@ -29,5 +28,4 @@ total time: 1.584s │ └─foo0 ------------------------------ 0.0% 31.3% 1 0.496s │ └sleep ----------------------------- 31.3% 31.3% 1 0.496s └─sleep ------------------------------- 36.1% 36.1% 1 0.572s -─constructor --------------------------- 0.0% 0.0% 1 0.000s -- cgit v1.2.3