Stream: Coq devs & plugin devs

Topic: full CI on innocuous PRs


view this post on Zulip Jason Gross (Nov 24 2022 at 03:47):

Do PRs that only change deprecation warnings like https://github.com/coq/coq/pull/16892#issuecomment-1325919914, or PRs that only change documentation, need full CI?

view this post on Zulip Maxime Dénès (Nov 24 2022 at 08:29):

For deprecation warnings, we could imagine some downstream developments treating them as errors (although unlikely).

view this post on Zulip Gaëtan Gilbert (Nov 24 2022 at 08:46):

didn't aac tactics treat deprecation as error? or was that only the plugin part?

view this post on Zulip Karl Palmskog (Nov 24 2022 at 08:52):

@Gaëtan Gilbert the Coq part of AAC tactics (which uses the plugin) will indeed treat deprecation as error.

view this post on Zulip Karl Palmskog (Nov 24 2022 at 08:53):

if this is a problem I can change it, but otherwise I'd like to keep it as a canary for deprecations

view this post on Zulip Théo Zimmermann (Nov 24 2022 at 09:26):

Only documentation PRs: fine to merge with just light CI.


Last updated: Feb 06 2023 at 19:03 UTC