Stream: Coq devs & plugin devs

Topic: Feedback vs CWarnings


view this post on Zulip Lasse (Apr 07 2021 at 16:45):

Is there any guidance somewhere on when a warning should be routed through CWarnings (allowing users to turn it into an error or ignore it), or immediately send it to Feedback? Looking through the codebase, both seem to be widely used and I cannot easily find a pattern. Is it the goal that all warnings eventually route through CWarnings?

view this post on Zulip Gaëtan Gilbert (Apr 07 2021 at 16:46):

all cwarnings

view this post on Zulip Lasse (Apr 07 2021 at 16:47):

So I´m encouraged to open PR´s to remove instances of Feedback.msg_warn?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2021 at 16:47):

Yup, it would be great if you could do so.

view this post on Zulip Lasse (Apr 07 2021 at 16:48):

Okay thanks. (I´ll probably not do so systematically, just the ones that annoy me ;-) )


Last updated: Oct 21 2021 at 20:02 UTC