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 ++++++++
 test-suite/output/bug5778.out                       |  4 ++++
 test-suite/output/bug5778.v                         |  7 +++++++
 4 files changed, 33 insertions(+)
 create mode 100644 test-suite/output-modulo-time/ltacprof_abstract.out
 create mode 100644 test-suite/output-modulo-time/ltacprof_abstract.v
 create mode 100644 test-suite/output/bug5778.out
 create mode 100644 test-suite/output/bug5778.v

(limited to 'test-suite')

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..c60c5abddf
--- /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 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/bug5778.out b/test-suite/output/bug5778.out
new file mode 100644
index 0000000000..91ceb1b583
--- /dev/null
+++ b/test-suite/output/bug5778.out
@@ -0,0 +1,4 @@
+The command has indeed failed with message:
+In nested Ltac calls to "c", "abs" and "abstract b ltac:(())", last call
+failed.
+The term "I" has type "True" which should be Set, Prop or Type.
diff --git a/test-suite/output/bug5778.v b/test-suite/output/bug5778.v
new file mode 100644
index 0000000000..0dcd76aeff
--- /dev/null
+++ b/test-suite/output/bug5778.v
@@ -0,0 +1,7 @@
+Ltac a _ := pose (I : I).
+Ltac b _ := a ().
+Ltac abs _ := abstract b ().
+Ltac c _ := abs ().
+Goal True.
+  Fail c ().
+Abort.
-- 
cgit v1.2.3