Stream: Coq devs & plugin devs

Topic: about warnings


view this post on Zulip Gaëtan Gilbert (Dec 08 2022 at 18:09):

https://github.com/coq/coq/pull/16902#discussion_r1043649768
@Jim Fehrle
Set Warnings does not reset warnings, one would need to do Set Warnings "-all,default" to reset.
Set Warnings is actually converted to Set Warnings Append by the implementation, same for Set Debug
(btw Set ... Append "thing" seems undocumented)

view this post on Zulip Jim Fehrle (Dec 08 2022 at 18:35):

Then I don't understand your comment in the PR "The point is that unmentioned warnings are reset, so for instance".

The description of the Warnings flags seems a bit thin. It should mention Set Warnings "-all,default". It doesn't list or explain the available categories. Readers shouldn't have to experiment or read code to get a full understanding of this flag. Who is the expert on it? Is it still deemed experimental?

I created https://github.com/coq/coq/issues/16963 to cover documenting "Append"

view this post on Zulip Théo Zimmermann (Dec 09 2022 at 09:16):

Warnings are not experimental, but I agree there is insufficient documentation. See https://github.com/coq/coq/issues/13557 and the issues and PR linked from there.


Last updated: Feb 05 2023 at 21:03 UTC