LtacProf now handles multi-success backtracking

Fixes #12196

2 files changed, 55 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".