Gaëtan Gilbert (Jun 01 2023 at 10:32): 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 ?
Ralf Jung (Jun 01 2023 at 12:53):@Tej Chajed would be the main contact
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.
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
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.
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.)
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: Nov 29 2023 at 22:01 UTC