Implement a way to set `-quiet`

[cpitclaudel]

Hi @ejgallego,

I noticed that coq-lsp prints more messages than serapi did. For example:

Inductive I := .

{"textDocument":{"uri":"file:///home/cpc/git/epfl/alectryon/test/minimal.v","version":0},"position":{"line":0,"character":0,"offset":-1},"range":{"start":{"line":0,"character":0,"offset":0},"end":{"line":0,"character":16,"offset":16}},"program":[],"messages":[{"range":null,"level":4,"text":"I is defined"},{"range":null,"level":4,"text":"I_rect is defined"},{"range":null,"level":4,"text":"I_ind is defined"},{"range":null,"level":4,"text":"I_rec is defined"},{"range":null,"level":4,"text":"I_sind is defined"}]}

SerAPI gives feedback for things like Check, but doesn't print these … is defined messages. Is there an explanation for the difference / a way to turn them off? Or is there a way to detect them that's better than just string matching?

Thanks a lot!

[ejgallego]

Hi @cpitclaudel , I will look into this more closely soon (holidays), but note the level field in the message.

Rocq has two kinds of messages, Info and Notice, at level 4 and 3 respectively. Messages at level 4 are omitted when Rocq is in -quiet mode.

coq-lsp leaves the Flags.quiet setting with its default value, SerAPI relied on the STM which could set quiet := true

Does filtering messages with level = 4 recover the SerAPI behavior?

I'm not sure -quiet should be the default for coq-lsp.

[ejgallego]

To be more concrete, these messages are emitted in Rocq's upstream by this code:

  Flags.if_verbose Feedback.msg_info (minductive_message names);

Thus, the situation in Rocq is a bit diverse:

• there are two levels, Info and Notice
• moreover, some code will guard the generation of such messages using the Flags.quiet setting, or in some cases, some other factors.

[there are some issues upstream discussing how to improve control over this]

I think we don't expose a way to set Flags.quiet to true other than using the Set Silent command, but we could add a --quiet flag command line, or an option to LSP's init config.

[cpitclaudel]

Does filtering messages with level = 4 recover the SerAPI behavior?

Yep, this is perfect. Thanks a lot!

[ejgallego]

Yep, this is perfect. Thanks a lot!

Glad it helps!

In any case I'll add a way to set quiet := true, as not every call to Rocq's msg_info is guarded with the flag.