Stream: Coq users

Topic: Auto-fix for future-coercion-class-field?


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ralf Jung (Aug 11 2022 at 16:10):

ah no that would not work, the line number is also wrong

view this post on Zulip 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).

view this post on Zulip Ralf Jung (Aug 11 2022 at 16:10):

it points at the Class rather than the :>

view this post on Zulip Ralf Jung (Aug 11 2022 at 16:10):

and then there are multiple :> in a class it only complains about the first

view this post on Zulip 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

view this post on Zulip Pierre Roux (Aug 11 2022 at 16:11):

Sure, that's when you (rightfully) complained, fixed in 8.16.0

view this post on Zulip Ralf Jung (Aug 11 2022 at 16:11):

oh okay I didnt realize that was after the rc

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Ralf Jung (Aug 11 2022 at 16:12):

thanks for reminding me that the warning is gone!

view this post on Zulip Pierre Roux (Aug 11 2022 at 16:15):

Indeed, the person who initially complained was @Paolo Giarrusso not you, sorry about that.


Last updated: Jan 29 2023 at 01:02 UTC