Open samuelgruetter opened 3 years ago
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.
Yes, this seems to be a
That said the given script gives an error in coq v8.11 and v8.12. I which version does it work?
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?
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:
prints
in the
*response*
buffer.prints
in the
*response*
buffer, andin the
*coq*
buffer.displays
in the
*response*
buffer.Now, the surprise: If I add timing:
suddenly the "hi" outputs are gone, and the
*response*
buffer only containsand in order to see all output, I need to know that there's a
*coq*
buffer too, where I can seeDesired behavior: All Ltac2 messages should appear in the
*response*
buffer.Coq version: 8.13.0 PG version: 7844e312b2a192c4245d0d05c12908efc5730e3b