Stream: Coq devs & plugin devs

Topic: perennial warnings as error


view this post on Zulip Gaëtan Gilbert (Jun 01 2023 at 10:32):

It seems the version of perennial we run in CI sets some warnings to be errors https://github.com/mit-pdos/perennial/blob/master/_CoqProject#L3-L8
I don't think we want that, especially since perennial overlays are a pain due to their use of submodules
Any opposition to turning it off in https://github.com/coq/coq/pull/17669 ?
or maybe upstream could turn it off

cc not sure who our perennial contacts are, maybe @Ralf Jung ?

view this post on Zulip Ralf Jung (Jun 01 2023 at 12:53):

@Tej Chajed would be the main contact

view this post on Zulip Ralf Jung (Jun 01 2023 at 12:53):

I think we want those things to be errors on our CI, but probably not on yours. not sure what the best way is to achieve that.

view this post on Zulip Gaëtan Gilbert (Jun 01 2023 at 12:56):

do you not test with coq master in your CI though? It seems likely to lead to breakage

view this post on Zulip Tej Chajed (Jun 01 2023 at 14:15):

We do test with both Coq master and Coq 8.17. It's rare that only Coq master fails but if we see that 8.17 succeeds then we know it's a recent change and it's generally easy to deal with.

view this post on Zulip Tej Chajed (Jun 01 2023 at 14:15):

I do like having warnings as errors, but we could turn off deprecated-tactic-notation. It was probably leftover from some earlier cleanup. (Unfortunately that's a very broad warning and I don't think we can make it more specific.)

view this post on Zulip Théo Zimmermann (Jun 02 2023 at 12:58):

With current Coq master, I think it can be made more specific (using the versions in which the warnings were introduced).


Last updated: Jun 23 2024 at 01:02 UTC