Merge PR #6406: Make [abstract] nodes show up in the Ltac profile

5 files changed, 40 insertions, 3 deletions

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 179952f28..ccded4417 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1158,10 +1158,14 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
          Proofview.V82.tactic begin
            tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
          end
-  | TacAbstract (tac,ido) ->
+  | TacAbstract (t,ido) ->
+      let call = LtacMLCall tac in
+      push_trace(None,call) ist >>= fun trace ->
+      Profile_ltac.do_profile "eval_tactic:TacAbstract" trace
+        (catch_error_tac trace begin
       Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT
-        (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist tac)
-      end
+        (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist t)
+      end end)
   | TacThen (t1,t) ->
       Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t)
   | TacDispatch tl ->
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.
diff --git a/test-suite/output/bug5778.out b/test-suite/output/bug5778.out
new file mode 100644
index 000000000..91ceb1b58
--- /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 000000000..0dcd76aef
--- /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.