Stream: Coq devs & plugin devs

Topic: [disc] Make hint locality warning an error


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: Feb 06 2023 at 19:03 UTC