Ralf Jung (Aug 11 2022 at 16:04): Ralf Jung (Aug 11 2022 at 16:04):Is there any tool available for fixing future-coercion-class-field? We have a lot of those warnings -- 37 in Iris alone, probably hundreds over the repos we maintain -- so fixing them all manually is not really feasible.
Ralf Jung (Aug 11 2022 at 16:05):IIRC the PR mentioned the possibility of another syntax that means "instance but not coercion"; if such a syntax existed then probably the line numbers printed by the warning would be enough to automate this reasonably well.
Ralf Jung (Aug 11 2022 at 16:10):ah no that would not work, the line number is also wrong
Pierre Roux (Aug 11 2022 at 16:10):Well, following your request, the warning is gone in 8.16. In 8.17 you'll just have to replace :> with :: (or probably rather silence the warning for a few version before doing that if you want to keep some backward compatibility).
Ralf Jung (Aug 11 2022 at 16:10):it points at the Class rather than the :>
Ralf Jung (Aug 11 2022 at 16:10):and then there are multiple :> in a class it only complains about the first
Ralf Jung (Aug 11 2022 at 16:10):Pierre Roux said:
Well, following your request, the warning is gone in 8.16. In 8.17 you'll just have to replace
:>with::(or probably rather silence the warning for a few version before doing that if you want to keep some backward compatibility).
is it? I am seeing it in the rc1
Pierre Roux (Aug 11 2022 at 16:11):Sure, that's when you (rightfully) complained, fixed in 8.16.0
Ralf Jung (Aug 11 2022 at 16:11):oh okay I didnt realize that was after the rc
Ralf Jung (Aug 11 2022 at 16:11):(I complained based on the PR where I got pinged, not based on seeing the warning in the wild)
Ralf Jung (Aug 11 2022 at 16:12):okay I guess I'll have to wait for https://github.com/coq/opam-coq-archive/pull/2253 then before I can ensure on CI that we are warning-free with 8.16
Ralf Jung (Aug 11 2022 at 16:12):thanks for reminding me that the warning is gone!
Pierre Roux (Aug 11 2022 at 16:15):Indeed, the person who initially complained was @Paolo Giarrusso not you, sorry about that.
Last updated: Oct 13 2024 at 01:02 UTC