Pierre-Marie Pédrot (May 09 2022 at 20:09): Pierre-Marie Pédrot (May 09 2022 at 20:09):it breaks the stdlib immediately...
Ali Caglayan (May 09 2022 at 20:15):But at least that is easy to patch.
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.
Ali Caglayan (May 09 2022 at 20:16):I wonder if we are being too careful, that is all.
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
Pierre-Marie Pédrot (May 09 2022 at 20:17):we don't lose anything by being cautious
Karl Palmskog (May 09 2022 at 20:19):should non-library developers even use hints?
Pierre-Marie Pédrot (May 09 2022 at 20:19):what's a non-library dev?
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
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.
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
Ali Caglayan (May 09 2022 at 20:29):So it really depends on the circumstances of the hint database/setup etc.
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.
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
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++.
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
Gaëtan Gilbert (May 09 2022 at 20:59):how do you handle the transitive part?
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
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”.
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.
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