Stream: Coq devs & plugin devs

Topic: [disc] Make hint locality warning an error


view this post on Zulip Ali Caglayan (May 09 2022 at 16:31):

Ok first issue with overlays: https://github.com/coq-community/autosubst/pull/27

view this post on Zulip Ali Caglayan (May 09 2022 at 16:31):

I think a year is more than enough time no?

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 16:36):

you should probably use global in overlays

view this post on Zulip Jason Gross (May 09 2022 at 16:37):

There's also an issue with bbv and fiat-crypto-legacy, which still support 8.7. Is there a truly backwards compatible way to fix this issue? (e.g., suppressing the error message in the build, and adding Export FileName in whatever places are necessary to make the code work with the hints being either global or export?)

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 16:38):

I thought fiat legacy was just for our CI, how does it support anything?

view this post on Zulip Ali Caglayan (May 09 2022 at 16:47):

I've tried #[global] and Global for Hint Rewrite and they don't work on 8.13 and older so not sure what we can do here.

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 17:00):

we shouldn't be changing behaviour in overlays
at least not this kind of hard to debug change

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 17:00):

if possible

view this post on Zulip Ali Caglayan (May 09 2022 at 17:07):

@Gaëtan Gilbert I agree that I should have gone with #[global] the first time, but the real issue here is that more than 2 versions of compatible Coq is wanted, but I don't see how we can deliver that without delaying this cleanup?

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 17:10):

we can skip the warning as error stage
or we can tell them to update or get kicked out of CI

view this post on Zulip Paolo Giarrusso (May 09 2022 at 18:38):

Skipping this stage doesn't seem to help much — there’s no backwards compatible fix anyway, so you’d still kick out of CI the more digilent projects, or reduce the supported versions, or delay the change.

view this post on Zulip Paolo Giarrusso (May 09 2022 at 19:14):

cc @Ralf Jung

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 19:36):

I'm fine with this not being part of 8.16 but at some point we'll have to kick the bucket. Striving to support Coq 8.7 seems a bit far-fetched if you ask me.

view this post on Zulip Jason Gross (May 09 2022 at 19:53):

I'm confused why there's no backwards compatible behavior? If I leave the hints unannotated and set up my Requires such that it works fine regardless of whether the behavior is Global or Export, shouldn't that continue to work even with the change in default semantics?

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 19:54):

You can try to do that, but I don't see you can pull this off in practice.

view this post on Zulip Ali Caglayan (May 09 2022 at 19:59):

Well technically there is a way to avoid the warning (which fails as an error) and that is to disable the warning.

view this post on Zulip Ali Caglayan (May 09 2022 at 20:00):

So I guess if people like in Jason's suggestion don't care for Global or Export then we can recommend disabling the warning

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 20:00):

are we changing the default and removing the warning soon after the branch or are we waiting longer?

view this post on Zulip Ali Caglayan (May 09 2022 at 20:01):

Even though we have been very careful not to replace global with export, I have yet to see a development for which this matters.

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 20:09):

it breaks the stdlib immediately...

view this post on Zulip Ali Caglayan (May 09 2022 at 20:15):

But at least that is easy to patch.

view this post on Zulip Ali Caglayan (May 09 2022 at 20:15):

For example, I did a search and replace on #[global] to #[export] in the HoTT lib recently, and nothing much changed.

view this post on Zulip Ali Caglayan (May 09 2022 at 20:16):

I wonder if we are being too careful, that is all.

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 20:17):

it's super hard to track hints, so I feel for the people who have gazillions of global hints around

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 20:17):

we don't lose anything by being cautious

view this post on Zulip Karl Palmskog (May 09 2022 at 20:19):

should non-library developers even use hints?

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 20:19):

what's a non-library dev?

view this post on Zulip Karl Palmskog (May 09 2022 at 20:20):

the risk of hint management going awry seems to so high that ordinary users proving something probably should only use hints indirectly through tactics provided by their libraries

view this post on Zulip Karl Palmskog (May 09 2022 at 20:20):

for example, Stdpp devs are library developers. If you're writing some conference artifact, you're probably not making a library to be used by many others.

view this post on Zulip Ali Caglayan (May 09 2022 at 20:28):

Well, I would want people using the HoTT library for instance to create their own instances which are a form of hint

view this post on Zulip Ali Caglayan (May 09 2022 at 20:29):

So it really depends on the circumstances of the hint database/setup etc.

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 20:42):

Karl Palmskog said:

should non-library developers even use hints?

Isn't it the other way around? It's not a problem if some leaf development has messy hints.

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 20:43):

OTOH if we say library devs shouldn't define hints they will put in their doc "you should consider making X Y Z hints"
and the next step after that is putting XYZ as export Hint in some RecommendedHints module

view this post on Zulip Ralf Jung (May 09 2022 at 20:49):

Ali Caglayan said:

Gaëtan Gilbert I agree that I should have gone with #[global] the first time, but the real issue here is that more than 2 versions of compatible Coq is wanted, but I don't see how we can deliver that without delaying this cleanup?

FWIW in the case of autosubst I am fine with 2 versions of compatible Coq -- I dont want to block this change. but in general I think this might be a bit quick, e.g. if this affected std++.

view this post on Zulip Jason Gross (May 09 2022 at 20:57):

You can try to do that, but I don't see you can pull this off in practice.

I am fine implementing the tedious but straightforward solution of giving every file that declares hints a Module Export Hints that collects all the hints, and then sticking a littany of Export foo.Hints lines on the top of every file that breaks

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 20:59):

how do you handle the transitive part?

view this post on Zulip Paolo Giarrusso (May 09 2022 at 22:51):

Adding Export to files that break sounds... unexpected. Either add imports in each client that breaks, or add exports to some central file (not straightforward). Coq has too much mutable state for idempotent exports; even if Hints modules only have hints, in that strategy I'd expect they'll be duplicated

view this post on Zulip Paolo Giarrusso (May 09 2022 at 22:56):

@Karl Palmskog that sounds as useful as "you can use mathcomp but you can't use Canonical”.

view this post on Zulip Paolo Giarrusso (May 09 2022 at 23:02):

and even for automation, one strategy (going back at least to https://www.cambridge.org/core/product/identifier/S0956796813000051/type/journal_article) is to use ad-hoc polymorphism to extend proof automation — that paper encodes backtracking using canonical structures, but type classes also work.

view this post on Zulip Théo Zimmermann (May 10 2022 at 08:16):

Gaëtan Gilbert said:

are we changing the default and removing the warning soon after the branch or are we waiting longer?

IMHO we should not make the warning fatal if we do not plan to change the default soon after.


Last updated: Dec 07 2023 at 07:39 UTC