Ltac printing - where is it displayed?

[threonorm]

Hi,

First, thank you for all the hard work on the extension!

I recently updated to modern VsCoq (vscoq-language-server 2.1.0, coq 8.18, VsCoq 2.1), and I had trouble to figure out where the Ltac debugging messages are showing, typically in the following snippet:

  Goal True.
     idtac "Printing something".

In previous versions, there used to be a buffer for those Ltac debugging outputs, but I can't seem to find it anymore. Is it a deprecated feature, or maybe there is a more modern way to achieve a similar effect, or I just missed the place where the output would be displayed?

[rtetley]

Hi, Thanks for reporting ! There seems to be a regression... I'll investigate !

[shilangyu]

Probably stems from the same underlying issue: debugging tactics such as debug auto. also does not print information anywhere.