diff options
Diffstat (limited to 'test-suite/output-modulo-time')
| -rw-r--r-- | test-suite/output-modulo-time/ltacprof.out | 15 | ||||
| -rw-r--r-- | test-suite/output-modulo-time/ltacprof.v | 8 | ||||
| -rw-r--r-- | test-suite/output-modulo-time/ltacprof_abstract.out | 17 | ||||
| -rw-r--r-- | test-suite/output-modulo-time/ltacprof_abstract.v | 8 | ||||
| -rw-r--r-- | test-suite/output-modulo-time/ltacprof_cutoff.out | 37 |
5 files changed, 85 insertions, 0 deletions
diff --git a/test-suite/output-modulo-time/ltacprof.out b/test-suite/output-modulo-time/ltacprof.out new file mode 100644 index 0000000000..5553e1b38d --- /dev/null +++ b/test-suite/output-modulo-time/ltacprof.out @@ -0,0 +1,15 @@ +total time: 1.032s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─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 +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─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.v b/test-suite/output-modulo-time/ltacprof.v new file mode 100644 index 0000000000..1e9e919797 --- /dev/null +++ b/test-suite/output-modulo-time/ltacprof.v @@ -0,0 +1,8 @@ +(* -*- coq-prog-args: ("-profile-ltac-cutoff" "0.0") -*- *) +Ltac sleep' := do 100 (do 100 (do 100 idtac)). +Ltac sleep := sleep'. + +Theorem x : True. +Proof. + idtac. idtac. sleep. constructor. +Defined. diff --git a/test-suite/output-modulo-time/ltacprof_abstract.out b/test-suite/output-modulo-time/ltacprof_abstract.out new file mode 100644 index 0000000000..fef4fa248d --- /dev/null +++ b/test-suite/output-modulo-time/ltacprof_abstract.out @@ -0,0 +1,17 @@ +total time: 0.922s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─abstract (sleep; constructor) --------- 0.0% 100.0% 1 0.922s +─sleep' -------------------------------- 100.0% 100.0% 1 0.922s +─constructor --------------------------- 0.0% 0.0% 1 0.000s +─sleep --------------------------------- 0.0% 0.0% 0 0.000s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─abstract (sleep; constructor) --------- 0.0% 100.0% 1 0.922s + ├─sleep' ------------------------------ 100.0% 100.0% 1 0.922s + ├─constructor ------------------------- 0.0% 0.0% 1 0.000s + └─sleep ------------------------------- 0.0% 0.0% 0 0.000s + └sleep' ------------------------------ 0.0% 0.0% 0 0.000s + diff --git a/test-suite/output-modulo-time/ltacprof_abstract.v b/test-suite/output-modulo-time/ltacprof_abstract.v new file mode 100644 index 0000000000..10a76309e3 --- /dev/null +++ b/test-suite/output-modulo-time/ltacprof_abstract.v @@ -0,0 +1,8 @@ +(* -*- coq-prog-args: ("-profile-ltac-cutoff" "0.0") -*- *) +Ltac sleep' := do 100 (do 100 (do 100 idtac)). +Ltac sleep := sleep'. + +Theorem x : True. +Proof. + idtac. idtac. abstract (sleep; constructor). +Defined. 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 0000000000..d91a38bb54 --- /dev/null +++ b/test-suite/output-modulo-time/ltacprof_cutoff.out @@ -0,0 +1,37 @@ +total time: 1.632s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─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.632s +└foo1 ---------------------------------- 0.0% 64.2% 1 1.048s + +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 +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ + |