Gaëtan Gilbert (Dec 08 2022 at 18:09): 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)
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"
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: Apr 20 2024 at 08:02 UTC