# Ltac: Where did my idtac debug output go?

When debugging Ltac tactics in Coq, one can use idtac to print debug messages. However, when a tactic invocation fails, ProofGeneral will not display any of the debug output in the *response* buffer, so in order to read our debug output, we have to read the *coq* buffer or precede the failing command with Fail.

Let's illustrate this with an example: Suppose we're in a goal like

U : Type

a, b, c, z : U

P, Q, R : U -> Prop

H : forall y : U, y = a \/ y = b \/ y = c

H0 : forall y : U, P y -> Q y

─────────────────────────────────────────────────────────

R z
where we have a hypothesis like H whose disjunction tells us what values
variables of type U can take, and suppose we want to write a tactic which
collects a list of all possible values for variables of type U,
i.e. it should return the list [a; b; c].
We could write it as follows:

U : Type

a, b, c, z : U

P, Q, R : U -> Prop

H : forall y : U, y = a \/ y = b \/ y = c

H0 : forall y : U, P y -> Q y

─────────────────────────────────────────────────────────

R z

Ltac disjunction_to_list d :=

lazymatch d with

| (_ = ?v \/ ?rest) =>

let s := disjunction_to_list rest in

constr:(v :: s)

| (_ = ?v) => constr:(v :: nil)

| _ => fail "did not expect" d

end.

And if we test it with

let d := type of (H z) in let r := disjunction_to_list d in idtac r.
we get back [a; b; c], as expected. On the other hand, if we use it on a
hypothesis which is not a disjunction,

let d := type of (H0 z) in let r := disjunction_to_list d in idtac r.
we get back our custom error message, as expected:

Error: Ltac call to "disjunction_to_list" failed.

Tactic failure: did not expect (P z -> Q z).
Now, let's not hard code H, but find it with a match goal:

match goal with

| H: forall (x: U), ?d |- _ =>

let r := disjunction_to_list d in idtac r

end.
But this results in an unhelpful error message:

Error: No matching clauses for match.
So let's add some debug output with idtac to check which hypotheses are being tested:

match goal with

| H: forall (x: U), ?d |- _ =>

idtac "Trying" H;

let r := disjunction_to_list d in idtac r

end.
But unfortunately, we don't get any debug output, the only thing displayed in
ProofGeneral's response window is

Error: No matching clauses for match.
Now here's the trick: ProofGeneral also has a buffer named *coq*, and if we
open it, we find the raw output of the coqtop process, which contains all the
debug output:

<infomsg>Trying H0</infomsg>

<infomsg>Trying H</infomsg>

<infomsg>Trying R</infomsg>

<infomsg>Trying Q</infomsg>

<infomsg>Trying P</infomsg>
An alternative way to get all output is, surprisingly, to use the Fail command:

Fail match goal with

| H: forall (x: U), ?d |- _ =>

idtac "Trying" H;

let r := disjunction_to_list d in idtac r

end.
It prints all we want into the response buffer:

Trying H0

Trying H

Trying R

Trying Q

Trying P

The command has indeed failed with message:

No matching clauses for match.
So we now know how to debug our tactic, but we still need to find why the above failed.
It turns out that the d we were passing to disjunction_to_list contains an
unbound variable x, so matching on it is not allowed and fails.
We can fix it as follows:

match goal with

| A: forall (x: U), ?d |- _ =>

idtac "Trying" d;

let A' := type of (A z) in

let r := disjunction_to_list A' in idtac r

end.
Whose output is as expected:

Trying (P x -> Q x)

Trying (x = a \/ x = b \/ x = c)

[a; b; c]
So, long story short:
In order to find lost debug output, it might help to look at the *coq* buffer or to
precede a failing command with Fail.
You can find the Coq source of this blog post here.

let d := type of (H z) in let r := disjunction_to_list d in idtac r.

let d := type of (H0 z) in let r := disjunction_to_list d in idtac r.

Error: Ltac call to "disjunction_to_list" failed.

Tactic failure: did not expect (P z -> Q z).

match goal with

| H: forall (x: U), ?d |- _ =>

let r := disjunction_to_list d in idtac r

end.

Error: No matching clauses for match.

match goal with

| H: forall (x: U), ?d |- _ =>

idtac "Trying" H;

let r := disjunction_to_list d in idtac r

end.

Error: No matching clauses for match.

<infomsg>Trying H0</infomsg>

<infomsg>Trying H</infomsg>

<infomsg>Trying R</infomsg>

<infomsg>Trying Q</infomsg>

<infomsg>Trying P</infomsg>

Fail match goal with

| H: forall (x: U), ?d |- _ =>

idtac "Trying" H;

let r := disjunction_to_list d in idtac r

end.

Trying H0

Trying H

Trying R

Trying Q

Trying P

The command has indeed failed with message:

No matching clauses for match.

match goal with

| A: forall (x: U), ?d |- _ =>

idtac "Trying" d;

let A' := type of (A z) in

let r := disjunction_to_list A' in idtac r

end.

Trying (P x -> Q x)

Trying (x = a \/ x = b \/ x = c)

[a; b; c]