About printing of traces of failures while calling ltac code.

An Ltac trace printing mechanism was introduced in 8.4 which was
inadvertedly modified by a series of commits such as 8e10368c3,
91f44f1da7a, ...

It was also sometimes buggy, iirc, when entering ML tactics which
themselves were calling ltac code.

It got really bad in 8.5 as in:

Tactic Notation "f" constr(x) := apply x. Ltac g x := f x.
Goal False.
idtac; f I. (* bad location reporting *)
g I.        (* was referring to tactic name "Top.Top#<>#1" *)

which this commit fixes.

I don't have a clear idea of what would be the best ltac tracing
mechanism, but to avoid it to be broken without being noticed, I
started to add some tests.

Eventually, it might be worth that an Ltac expert brainstrom on it!

5 files changed, 69 insertions, 9 deletions

diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml
index d661f9677..e657eb9bc 100644
--- a/ltac/tactic_debug.ml
+++ b/ltac/tactic_debug.ml
@@ -330,10 +330,9 @@ let db_breakpoint debug s =
 
 let is_defined_ltac trace =
   let rec aux = function
-  | (_, Tacexpr.LtacNameCall f) :: tail ->
-      not (Tacenv.is_ltac_for_ml_tactic f)
-  | (_, Tacexpr.LtacAtomCall _) :: tail ->
-      false
+  | (_, Tacexpr.LtacNameCall f) :: _ -> not (Tacenv.is_ltac_for_ml_tactic f)
+  | (_, Tacexpr.LtacNotationCall f) :: _ -> true
+  | (_, Tacexpr.LtacAtomCall _) :: _ -> false
   | _ :: tail -> aux tail
   | [] -> false in
   aux (List.rev trace)
@@ -341,7 +340,7 @@ let is_defined_ltac trace =
 let explain_ltac_call_trace last trace loc =
   let calls = last :: List.rev_map snd trace in
   let pr_call ck = match ck with
-  | Tacexpr.LtacNotationCall kn -> quote (KerName.print kn)
+    | Tacexpr.LtacNotationCall kn -> quote (Pptactic.pr_alias_key kn)
   | Tacexpr.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
   | Tacexpr.LtacMLCall t ->
       quote (Pptactic.pr_glob_tactic (Global.env()) t)
@@ -363,6 +362,7 @@ let explain_ltac_call_trace last trace loc =
   in
   match calls with
   | [] -> mt ()
+  | [a] -> hov 0 (str "Ltac call to " ++ pr_call a ++ str " failed.")
   | _ ->
     let kind_of_last_call = match List.last calls with
     | Tacexpr.LtacConstrInterp _ -> ", last term evaluation failed."
@@ -373,10 +373,13 @@ let explain_ltac_call_trace last trace loc =
 
 let skip_extensions trace =
   let rec aux = function
-  | (_,Tacexpr.LtacNameCall f as tac) :: _ 
-      when Tacenv.is_ltac_for_ml_tactic f -> [tac]
-  | (_,(Tacexpr.LtacNotationCall _ | Tacexpr.LtacMLCall _) as tac)
-      :: _ -> [tac]
+  | (_,Tacexpr.LtacNameCall f as tac) :: _
+       when Tacenv.is_ltac_for_ml_tactic f -> [tac]
+  | (_,Tacexpr.LtacNotationCall _ as tac) :: (_,Tacexpr.LtacMLCall _) :: _ ->
+     (* Case of an ML defined tactic with entry of the form <<"foo" args>> *)
+     (* see tacextend.mlp *)
+     [tac]
+  | (_,Tacexpr.LtacMLCall _ as tac) :: _ -> [tac]
   | t :: tail -> t :: aux tail
   | [] -> [] in
   List.rev (aux (List.rev trace))
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 114410fed..3d1e3e054 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -366,6 +366,24 @@ module Make
       in
       str "<" ++ name ++ str ">" ++ args
 
+
+  let pr_alias_key key =
+    try
+      let prods = (KNmap.find key !prnotation_tab).pptac_prods in
+      (* First printing strategy: only the head symbol *)
+      match prods with
+      | TacTerm s :: prods -> str s
+      | _ ->
+      (* Second printing strategy; if ever Tactic Notation is eventually *)
+      (* accepting notations not starting with an identifier *)
+      let rec pr = function
+      | [] -> []
+      | TacTerm s :: prods -> s :: pr prods
+      | TacNonTerm (_,_,id) :: prods -> ".." :: pr prods in
+      str (String.concat " " (pr prods))
+    with Not_found ->
+      KerName.print key
+    
   let pr_alias_gen pr_gen lev key l =
     try
       let pp = KNmap.find key !prnotation_tab in
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index 4ef2ea918..f02785a55 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -45,6 +45,8 @@ module type Pp = sig
   val pr_extend :
     (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
 
+  val pr_alias_key : Names.KerName.t -> std_ppcmds
+
   val pr_alias : (Val.t -> std_ppcmds) ->
     int -> Names.KerName.t -> Val.t list -> std_ppcmds
 
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index 20e274e25..21a8cf9ed 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -3,3 +3,22 @@ Error: Ltac variable y depends on pattern variable name z which is not bound in
 Ltac f x y z :=
   symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize
    dependent z
+The command has indeed failed with message:
+In nested Ltac calls to "g1" and "refine", last call failed.
+The term "I" has type "True" while it is expected to have type "False".
+The command has indeed failed with message:
+In nested Ltac calls to "f1" and "refine", last call failed.
+The term "I" has type "True" while it is expected to have type "False".
+The command has indeed failed with message:
+In nested Ltac calls to "g2", "g1" and "refine", last call failed.
+The term "I" has type "True" while it is expected to have type "False".
+The command has indeed failed with message:
+In nested Ltac calls to "f2", "f1" and "refine", last call failed.
+The term "I" has type "True" while it is expected to have type "False".
+The command has indeed failed with message:
+Ltac call to "h" failed.
+Error: Ltac variable x is bound to I which cannot be coerced to
+a declared or quantified hypothesis.
+The command has indeed failed with message:
+In nested Ltac calls to "h" and "injection", last call failed.
+Error: No primitive equality found.
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 373b870b9..dfa60eeda 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -25,3 +25,21 @@ Ltac f x y z :=
   generalize dependent z.
 
 Print Ltac f.
+
+(* Error messages *)
+
+Ltac g1 x := refine x.
+Tactic Notation "g2" constr(x) := g1 x.
+Tactic Notation "f1" constr(x) := refine x.
+Ltac f2 x := f1 x.
+Goal False.
+Fail g1 I.
+Fail f1 I.
+Fail g2 I.
+Fail f2 I.
+
+Ltac h x := injection x.
+Goal True -> False.
+Fail h I.
+intro H.
+Fail h H.