diff options
Diffstat (limited to 'test-suite/output-modulo-time')
| -rw-r--r-- | test-suite/output-modulo-time/ltacprof.out | 13 | ||||
| -rw-r--r-- | test-suite/output-modulo-time/ltacprof_cutoff.out | 40 | ||||
| -rw-r--r-- | test-suite/output-modulo-time/ltacprof_cutoff.v | 34 |
3 files changed, 56 insertions, 31 deletions
diff --git a/test-suite/output-modulo-time/ltacprof.out b/test-suite/output-modulo-time/ltacprof.out index cc04c2c9b..5553e1b38 100644 --- a/test-suite/output-modulo-time/ltacprof.out +++ b/test-suite/output-modulo-time/ltacprof.out @@ -1,12 +1,15 @@ -total time: 1.528s +total time: 1.032s - tactic local total calls max + tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─sleep' -------------------------------- 100.0% 100.0% 1 1.528s +─sleep' -------------------------------- 100.0% 100.0% 1 1.032s +─sleep --------------------------------- 0.0% 0.0% 0 0.000s ─constructor --------------------------- 0.0% 0.0% 1 0.000s - tactic local total calls max + tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─sleep' -------------------------------- 100.0% 100.0% 1 1.528s +─sleep' -------------------------------- 100.0% 100.0% 1 1.032s +─sleep --------------------------------- 0.0% 0.0% 0 0.000s +└sleep' -------------------------------- 0.0% 0.0% 0 0.000s ─constructor --------------------------- 0.0% 0.0% 1 0.000s diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.out b/test-suite/output-modulo-time/ltacprof_cutoff.out index 0cd5777cc..d91a38bb5 100644 --- a/test-suite/output-modulo-time/ltacprof_cutoff.out +++ b/test-suite/output-modulo-time/ltacprof_cutoff.out @@ -1,31 +1,37 @@ -total time: 1.584s +total time: 1.632s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s -─sleep --------------------------------- 100.0% 100.0% 3 0.572s -─foo1 ---------------------------------- 0.0% 63.9% 1 1.012s +─sleep --------------------------------- 100.0% 100.0% 3 0.584s +─foo2 ---------------------------------- 0.0% 100.0% 1 1.632s +─foo1 ---------------------------------- 0.0% 64.2% 1 1.048s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s -└foo1 ---------------------------------- 0.0% 63.9% 1 1.012s +─foo2 ---------------------------------- 0.0% 100.0% 1 1.632s +└foo1 ---------------------------------- 0.0% 64.2% 1 1.048s -total time: 1.584s +total time: 0.520s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─foo2 ---------------------------------- 0.0% 100.0% 1 0.520s +─sleep --------------------------------- 99.2% 99.2% 52 0.016s +─foo1 ---------------------------------- 0.0% 97.7% 1 0.508s +─foo0 ---------------------------------- 0.8% 96.2% 1 0.500s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─foo2 ---------------------------------- 0.0% 100.0% 1 0.520s +└foo1 ---------------------------------- 0.0% 97.7% 1 0.508s +└foo0 ---------------------------------- 0.8% 96.2% 1 0.500s +└sleep --------------------------------- 95.4% 95.4% 50 0.016s + +total time: 0.000s 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 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 diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v index 3dad6271a..ae5d51bae 100644 --- a/test-suite/output-modulo-time/ltacprof_cutoff.v +++ b/test-suite/output-modulo-time/ltacprof_cutoff.v @@ -1,12 +1,28 @@ (* -*- coq-prog-args: ("-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). +Module WithIdTac. + 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. + Ltac foo0 := idtac; sleep. + Ltac foo1 := sleep; foo0. + Ltac foo2 := sleep; foo1. + Goal True. + foo2. + Show Ltac Profile CutOff 47. + constructor. + Qed. +End WithIdTac. + +Module TestEval. + Ltac sleep := let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac. + + Ltac foo0 := idtac; do 50 (idtac; sleep). + Ltac foo1 := sleep; foo0. + Ltac foo2 := sleep; foo1. + Goal True. + Reset Ltac Profile. + foo2. + Show Ltac Profile CutOff 47. + constructor. + Qed. +End TestEval. |