From 29644bf0814945cbf2b4388b8f8bd19f109503a0 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 12 Dec 2017 12:00:25 -0500 Subject: Make [abstract] nodes show up in the Ltac profile This closes #5082 and closes #5778, but makes #6404 apply to `abstract` as well as `transparent_abstract`. This is unfortunate, but I think it is worth it to get `abstract` in the profile (and therefore not misassign the time spent sending the subproof to the kernel). Another alternative would have been to add a dedicated entry to `ltac_call_kind` for `TacAbstract`, but I think it's better to just deal with #6404 all at once. The "better" solution here would have been to move `abstract` out of the Ltac syntax tree and define it via `TACTIC EXTEND` like `transparent_abstract`. However, the STM relies on its ability to recognize `abstract` and `solve [ abstract ... ]` syntactically so that it can handle `par: abstract`. Note that had to add locations to `TacAbstract` nodes, as I could not figure out how to call `push_trace` otherwise. --- test-suite/output-modulo-time/ltacprof_abstract.out | 14 ++++++++++++++ test-suite/output-modulo-time/ltacprof_abstract.v | 8 ++++++++ 2 files changed, 22 insertions(+) create mode 100644 test-suite/output-modulo-time/ltacprof_abstract.out create mode 100644 test-suite/output-modulo-time/ltacprof_abstract.v (limited to 'test-suite/output-modulo-time') 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 000000000..c60c5abdd --- /dev/null +++ b/test-suite/output-modulo-time/ltacprof_abstract.out @@ -0,0 +1,14 @@ +total time: 0.964s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─sleep' -------------------------------- 100.0% 100.0% 1 0.964s +─abstract (sleep; constructor) --------- 0.0% 100.0% 1 0.964s +─constructor --------------------------- 0.0% 0.0% 1 0.000s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─abstract (sleep; constructor) --------- 0.0% 100.0% 1 0.964s + ├─sleep' ------------------------------ 100.0% 100.0% 1 0.964s + └─constructor ------------------------- 0.0% 0.0% 1 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 000000000..10a76309e --- /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. -- cgit v1.2.3