LtacProf now handles multi-success backtracking

Fixes #12196

3 files changed, 72 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_12196.v b/test-suite/bugs/closed/bug_12196.v
new file mode 100644
index 0000000000..c0851b3204
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12196.v
@@ -0,0 +1,46 @@
+(** TODO: Figure out how to test "sanity" for the ltac profiler output *)
+Fixpoint fact (n : nat) := match n with 0 => 1 | S n' => n * fact n' end.
+Fixpoint walk (n : nat) := match n with 0 => tt | S n => walk n end.
+Ltac slow := idtac + (do 2 (let x := eval lazy in (walk (fact 9)) in idtac)).
+Ltac slow2 := idtac + (do 2 (let x := eval lazy in (walk (fact 9)) in idtac)).
+Ltac multi := idtac + slow + slow2.
+Set Ltac Profiling.
+Goal True.
+  Time try (multi; fail).
+  (* Warning: Ltac Profiler cannot yet handle backtracking into multi-success
+ tactics; profiling results may be wildly inaccurate.
+ [profile-backtracking,ltac] *)
+  Show Ltac Profile.
+  (* Used to be:
+total time:      0.000s
+
+ tactic                                   local  total   calls       max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─multi ---------------------------------  47.1%  47.1%       1    0.000s
+─slow ----------------------------------  35.3%  35.3%       1    0.000s
+─slow2 ---------------------------------  17.6%  17.6%       1    0.000s
+
+ tactic                                   local  total   calls       max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─multi ---------------------------------  47.1%  47.1%       1    0.000s
+─slow ----------------------------------  35.3%  35.3%       1    0.000s
+─slow2 ---------------------------------  17.6%  17.6%       1    0.000s
+
+   *)
+  (* Now:
+total time:      2.074s
+
+ tactic                                   local  total   calls       max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─multi ---------------------------------   0.0% 100.0%       6    1.119s
+─slow ----------------------------------  54.0%  54.0%       3    1.119s
+─slow2 ---------------------------------  46.0%  46.0%       3    0.955s
+
+ tactic                                   local  total   calls       max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─multi ---------------------------------   0.0% 100.0%       6    1.119s
+ ├─slow --------------------------------  54.0%  54.0%       3    1.119s
+ └─slow2 -------------------------------  46.0%  46.0%       3    0.955s
+
+*)
+Abort.
diff --git a/test-suite/bugs/closed/bug_6378.v b/test-suite/bugs/closed/bug_6378.v
index 68ae7961dd..453924d587 100644
--- a/test-suite/bugs/closed/bug_6378.v
+++ b/test-suite/bugs/closed/bug_6378.v
@@ -7,11 +7,20 @@ Ltac profile_constr tac :=
 
 Ltac slow _ := eval vm_compute in (Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl).
 
+Ltac manipulate_ltac_prof :=
+  start ltac profiling;
+  reset ltac profile;
+  try ((idtac + reset ltac profile + idtac); fail);
+  try ((idtac + start ltac profiling + idtac); fail);
+  try ((idtac + stop ltac profiling + idtac); fail).
+
 Goal True.
   start ltac profiling.
   reset ltac profile.
+  manipulate_ltac_prof.
   reset ltac profile.
   stop ltac profiling.
+  Set Warnings Append "+profile-invalid-stack-no-self".
   time profile_constr slow.
   show ltac profile cutoff 0.
   show ltac profile "slow".
diff --git a/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v
index d5552695c4..f40f40c2bb 100644
--- a/test-suite/success/ltacprof.v
+++ b/test-suite/success/ltacprof.v
@@ -6,3 +6,20 @@ Goal True.
   try (multi; fail). (* Used to result in: Anomaly: Uncaught exception Failure("hd"). Please report. *)
 Admitted.
 Show Ltac Profile.
+
+(* backtracking across profiler manipulation *)
+Unset Ltac Profiling.
+Reset Ltac Profile.
+
+Fixpoint slow (n : nat) : unit
+  := match n with
+     | 0 => tt
+     | S n => fst (slow n, slow n)
+     end.
+
+Ltac slow := idtac; let v := eval cbv in (slow 16) in idtac.
+Ltac multi2 :=
+  try (((idtac; slow) + (start ltac profiling; slow) + (idtac; slow) + (slow; stop ltac profiling; slow) + slow + (start ltac profiling; (idtac + slow); ((stop ltac profiling + idtac); fail))); slow; fail); slow; show ltac profile.
+Goal True.
+  multi2.
+Admitted.