search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
336 stars 68 forks source link

Ltac printing - where is it displayed? #733

Closed threonorm closed 2 months ago

threonorm commented 7 months ago

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 commented 7 months ago

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

shilangyu commented 6 months ago

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

rtetley commented 2 months ago

While working on #842 I noticed what is happening here. idtac sends a Info level feedback which we currently ignore entirely. Turning it on would display all info messages such as foo is defined, etc... Should we print this in the goal panel along other messages (with an option to turn it off) ?

For debug messages I think I will build a custom view in the Panel bar (see https://code.visualstudio.com/api/ux-guidelines/panel).

@shilangyu However debug auto. seems to work for me ?

TheoWinterhalter commented 2 months ago

Showing foo is defined is not so bad when plugins create additional definitions silently like Equations.

rtetley commented 2 months ago

Okay the idea will be to display them in the goal view, but avoid triggering diagnostics, that way we avoid squiggly lines. (See #842)

rtetley commented 2 months ago

Should we add a setting to disable Info level messages ? Or is removing them from diagnostics enough ?