Ok first issue with overlays: https://github.com/coq-community/autosubst/pull/27
I think a year is more than enough time no?
you should probably use global in overlays
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?)
I thought fiat legacy was just for our CI, how does it support anything?
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.
we shouldn't be changing behaviour in overlays
at least not this kind of hard to debug change
if possible
@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?
we can skip the warning as error stage
or we can tell them to update or get kicked out of CI
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.
cc @Ralf Jung
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.
I'm confused why there's no backwards compatible behavior? If I leave the hints unannotated and set up my Require
s 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?
You can try to do that, but I don't see you can pull this off in practice.
Well technically there is a way to avoid the warning (which fails as an error) and that is to disable the warning.
So I guess if people like in Jason's suggestion don't care for Global or Export then we can recommend disabling the warning
are we changing the default and removing the warning soon after the branch or are we waiting longer?
Even though we have been very careful not to replace global with export, I have yet to see a development for which this matters.
it breaks the stdlib immediately...
But at least that is easy to patch.
For example, I did a search and replace on #[global] to #[export] in the HoTT lib recently, and nothing much changed.
I wonder if we are being too careful, that is all.
it's super hard to track hints, so I feel for the people who have gazillions of global hints around
we don't lose anything by being cautious
should non-library developers even use hints?
what's a non-library dev?
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
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.
Well, I would want people using the HoTT library for instance to create their own instances which are a form of hint
So it really depends on the circumstances of the hint database/setup etc.
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.
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
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++.
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
how do you handle the transitive part?
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
@Karl Palmskog that sounds as useful as "you can use mathcomp but you can't use Canonical
”.
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.
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: Oct 13 2024 at 01:02 UTC