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 ?
@Tej Chajed would be the main contact
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.
do you not test with coq master in your CI though? It seems likely to lead to breakage
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.
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.)
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