Ltac2 messages are not displayed in *response* buffer if there's timing output

[samuelgruetter]

Not sure if this is a PG issue or an Ltac2 issue, but here's something that works fine in Ltac1 but not in Ltac2:

Ltac wait1 n :=
  idtac "hi";
  lazymatch n with
  | O => idtac
  | S ?m => wait1 m; wait1 m
  end.

Goal False.
Proof.
  wait1 1.

prints

hi
hi
hi

in the *response* buffer.

Ltac wait2 n :=
  idtac "hi";
  time (idtac; lazymatch n with
  | O => idtac
  | S ?m => wait2 m; wait2 m
  end).

wait2 1.

prints

hi
hi
Tactic call ran for 0. secs (0.u,0.s) (success)
hi
Tactic call ran for 0. secs (0.u,0.s) (success)
Tactic call ran for 0. secs (0.u,0.s) (success)

in the *response* buffer, and

<infomsg>hi</infomsg>
<infomsg>hi</infomsg>
<infomsg>Tactic call ran for 0. secs (0.u,0.s) (success)</infomsg>
<infomsg>hi</infomsg>
<infomsg>Tactic call ran for 0. secs (0.u,0.s) (success)</infomsg>
<infomsg>Tactic call ran for 0. secs (0.u,0.s) (success)</infomsg>

in the *coq* buffer.

Abort.

Require Import Ltac2.Ltac2.

Ltac2 rec wait1(n: int) :=
  let _ := Message.print (Message.of_string "hi") in
  if Int.equal n 0 then () else (wait1 (Int.sub n 1); wait1 (Int.sub n 1)).

Goal False.
Proof.
  wait1 1.

displays

hi
hi
hi

in the *response* buffer.

Now, the surprise: If I add timing:

Ltac2 rec wait2(n: int) :=
  let _ := Message.print (Message.of_string "hi") in
  Control.time None (fun _ => if Int.equal n 0 then () else (wait2 (Int.sub n 1); wait2 (Int.sub n 1))).

  wait2 1.

suddenly the "hi" outputs are gone, and the *response* buffer only contains

Tactic call ran for 0. secs (0.u,0.s) (success)
Tactic call ran for 0. secs (0.u,0.s) (success)
Tactic call ran for 0. secs (0.u,0.s) (success)

and in order to see all output, I need to know that there's a *coq* buffer too, where I can see

hi
hi
<infomsg>Tactic call ran for 0. secs (0.u,0.s) (success)</infomsg>
hi
<infomsg>Tactic call ran for 0. secs (0.u,0.s) (success)</infomsg>
<infomsg>Tactic call ran for 0. secs (0.u,0.s) (success)</infomsg>

Desired behavior: All Ltac2 messages should appear in the *response* buffer.

Coq version: 8.13.0 PG version: 7844e312b2a192c4245d0d05c12908efc5730e3b

[hendriktews]

In your last *coq* excerpt, the hi's are not inside infomsg tags, explaining the difference IMO. PG contains some heuristics, probably stemming from Isabelle, that discard apparently useless output before output it recognizes as useful.

[Matafou]

Yes, this seems to be a missing in ltac2 messages. I will fill a bug report in Coq.

That said the given script gives an error in coq v8.11 and v8.12. I which version does it work?

[Matafou]

OK it works in v8.13. Workaround:

Ltac2 rec wait2(n: int) :=
  let _ := ltac1:(idtac "hi") in
  Control.time None (fun _ => if Int.equal n 0 then () else (wait2 (Int.sub n 1); wait2 (Int.sub n 1))).

That said maybe there is another ltac2 command to emit infomsg instead of simple strings?