Stream: Coq users

Topic: Future-compatibility & deprecated-hint-without-locality?

view this post on Zulip Jason Gross (Mar 03 2021 at 13:34):

I'm getting a bunch of deprecated-hint-without-locality warnings on fiat-crypto. It's easy to fix many of them just by adding Global. However, Global Hint Rewrite is an error in Coq 8.9 (which we support as it's the version on the latest Debian stable; when Bullseye becomes stable, I expect we'll be open to dropping support for 8.9 and 8.10 and bump the minimum version to 8.11, which is what's packaged on the latest Ubuntu LTS, focal). Is there a good way to be future compatible here while still supporting Coq 8.9?

view this post on Zulip Théo Zimmermann (Mar 03 2021 at 13:54):

There is no simple solution to this, no. But note that it may take a while before the default locality is actually changed, so it's fine to delay these new annotations a bit and silence the warning in the meantime.

view this post on Zulip Paolo Giarrusso (Mar 03 2021 at 14:17):

One of the hint commands still rejects Global in 8.13 and IIRC that's Hint Rewrite.

view this post on Zulip Théo Zimmermann (Mar 03 2021 at 14:41):


Last updated: May 18 2024 at 08:40 UTC