Pierre-Marie Pédrot (Mar 22 2021 at 15:39): Pierre-Marie Pédrot (Mar 22 2021 at 15:39):I am currently trying to write a patch so that Coq warns for implicit declaration of hint databases, and the least I can say is that it's quite tricky.
Pierre-Marie Pédrot (Mar 22 2021 at 15:39):In particular, it seems that Program Instance generates new hint databases on the fly (!)
Pierre-Marie Pédrot (Mar 22 2021 at 15:40):Is this a design choice, or is there something very fishy going on? cc @Matthieu Sozeau
Matthieu Sozeau (Mar 22 2021 at 15:41):Program Instance? For sure Equations does it, it generates a few of databases for the equalities of the definition (rewrite) and its well-founded obligations (hints).
Matthieu Sozeau (Mar 22 2021 at 15:41):What does the database contain?
Pierre-Marie Pédrot (Mar 22 2021 at 15:42):It happens in CRelationClasses, with Program Instance impl_Reflexive : Reflexive impl.
Matthieu Sozeau (Mar 22 2021 at 15:42):I'm curious, is this a prerequesite for turning hint databases into properly scoped objects at some point?
Pierre-Marie Pédrot (Mar 22 2021 at 15:42):yes.
Matthieu Sozeau (Mar 22 2021 at 15:42):Ok, I'm happy to help :)
Pierre-Marie Pédrot (Mar 22 2021 at 15:42):(and as usual, it's a rabbit hole)
Matthieu Sozeau (Mar 22 2021 at 15:43):Can you look in the db ?
Guillaume Melquiond (Mar 22 2021 at 15:43):Generating hint databases on the fly seems like a good idea, as long as they are transient ones (i.e., unnamed). Is the generated one supposed to survive Program Instance?
Pierre-Marie Pédrot (Mar 22 2021 at 15:43):for the command above I get:
Non-discriminated database
Unfoldable variable definitions: none
Unfoldable constant definitions: none
Cut: emp
For any goal ->
For impl_Reflexive_obligation_1 -> unfold impl_Reflexive_obligation_1(level 4, id 0)
the database is conspicuously named impl_Reflexive
Matthieu Sozeau (Mar 22 2021 at 15:44):Hmm I see. Hint unfolds are declared for the obligations of (every?) program definition?
Pierre-Marie Pédrot (Mar 22 2021 at 15:45):what's the point if they are secluded in a database that lies around?
Pierre-Marie Pédrot (Mar 22 2021 at 15:45):(this patch also uncovers quite a lot of very suspicious activity around hint dbs in the stdlib btw)
Matthieu Sozeau (Mar 22 2021 at 15:45):Well, it lets you use them if you want, using auto with foo
Pierre-Marie Pédrot (Mar 22 2021 at 15:46):Without scoping? This is a recipe for disaster.
Pierre-Marie Pédrot (Mar 22 2021 at 15:46):If people happen to define a program instance with some generic name, it will appear randomly in unrelated places.
Matthieu Sozeau (Mar 22 2021 at 15:48):Well yes. Ideally you would like to be able to scope this hint database as foo.unfolds or foo.obligations
Pierre-Marie Pédrot (Mar 22 2021 at 15:48):So, you confirm it's an intended behaviour?
Pierre-Marie Pédrot (Mar 22 2021 at 15:48):Expect trouble downstream.
Pierre-Marie Pédrot (Mar 22 2021 at 15:49):The transition phase is going to be painful, with people wondering where their database clash are coming from.
Matthieu Sozeau (Mar 22 2021 at 15:50):Yes, it's intended that we create the database.
Matthieu Sozeau (Mar 22 2021 at 15:50):However, it's probably very seldom used
Matthieu Sozeau (Mar 22 2021 at 15:51):You could imagine an attribute for Program to declare these hints in a particular database.
Pierre-Marie Pédrot (Mar 22 2021 at 15:52):'mkay
Pierre-Marie Pédrot (Mar 22 2021 at 16:13):I suspect this is completely broken. If you try to define two databases with the same name in two different files and then require them both, you'll get a different thing depending on the order of require.
Pierre-Marie Pédrot (Mar 22 2021 at 16:14):Superglobal is back, and it is pas content
Guillaume Melquiond (Mar 22 2021 at 16:17):Isn't that an orthogonal problem? That is, the content of hint databases should depend on the order of Import rather than the order of Require?
Pierre-Marie Pédrot (Mar 22 2021 at 16:18):No, it's linked to the fact that there is no proper semantic for duplicate database creation.
Pierre-Marie Pédrot (Mar 22 2021 at 16:18):So if you haphazardly create databases automatically through commands you're bound to get weird behaviours.
Pierre-Marie Pédrot (Mar 22 2021 at 16:20):I am porting the stdlib to the warning right now and it's a festival.
Pierre-Marie Pédrot (Mar 22 2021 at 16:21):There are hints spread around declaring implicitly different hint databases.
Pierre-Marie Pédrot (Mar 22 2021 at 16:21):In files that are not even related by require.
Matthieu Sozeau (Mar 22 2021 at 16:23):Sure, as long as we don't have scoping this is broken
Pierre-Marie Pédrot (Mar 22 2021 at 16:23):No no, it's supposed to be the very same database.
Pierre-Marie Pédrot (Mar 22 2021 at 16:23):but there is no single place to put it, since there is no sup of the require chain.
Matthieu Sozeau (Mar 22 2021 at 16:23):Oh, ok, how come you get different results?
Matthieu Sozeau (Mar 22 2021 at 16:24):You mean that e.g. precedence of hints is not commutative?
Pierre-Marie Pédrot (Mar 22 2021 at 16:24):Declaring a database erases the old one, if there is already one with the same name.
Matthieu Sozeau (Mar 22 2021 at 16:25):But one should definitely not be allowed to declare the same database twice!
Pierre-Marie Pédrot (Mar 22 2021 at 16:25):Yes, but that is the problem.
Guillaume Melquiond (Mar 22 2021 at 16:25):Pierre-Marie Pédrot said:
but there is no single place to put it, since there is no sup of the require chain.
Since Program requires a specific file from the standard library, this seems like a sup. Or am I missing something?
Pierre-Marie Pédrot (Mar 22 2021 at 16:25):I am not talking about program now.
Pierre-Marie Pédrot (Mar 22 2021 at 16:26):Several Arith files declare the db arith several times.
Pierre-Marie Pédrot (Mar 22 2021 at 16:26):(implicitly)
Pierre-Marie Pédrot (Mar 22 2021 at 16:26):but there is no root file required by everybody in which the db creation could be put
Guillaume Melquiond (Mar 22 2021 at 16:26):In the file declaring nat?
Pierre-Marie Pédrot (Mar 22 2021 at 16:27):This is a design choice, which will matter when databases are scoped.
Guillaume Melquiond (Mar 22 2021 at 16:27):Sure, I am just disputing the fact that there is no sup.
Pierre-Marie Pédrot (Mar 22 2021 at 16:28):Well it's not a sup, it's an upper bound.
Guillaume Melquiond (Mar 22 2021 at 16:30):That is good enough. Databases do not have to be declared in the least upper bound of the files using them. Any upper bound is fine.
Pierre-Marie Pédrot (Mar 22 2021 at 16:31):But it's not unique, so you have to think.
Pierre-Marie Pédrot (Mar 22 2021 at 16:38):There are quite a few databases that really look like deprecated stuff, judging from the point in time they were introduced and where they are used.
Matthieu Sozeau (Mar 22 2021 at 16:42):That's quite probable that we have deprecated databases. And for sure this work will imply choosing where to declared the db, but that's a good thing I believe
Pierre-Marie Pédrot (Mar 22 2021 at 16:43):Inquiry: where does the sets database live?
Pierre-Marie Pédrot (Mar 22 2021 at 16:43):it's used by unrelated parts of the stdlib.
Pierre-Marie Pédrot (Mar 22 2021 at 16:44):amongst others, theories/Sets/ obviously, but also theories/Relations/
Guillaume Melquiond (Mar 22 2021 at 16:49):Perhaps theories/Init/Datatypes.v? (Or any other from Init.)
Pierre-Marie Pédrot (Mar 22 2021 at 19:08):I am slightly concerned that polluting the prelude with stuff that is barely used at all is going to be problematic for our users.
Théo Zimmermann (Mar 23 2021 at 13:36):Maybe in the case of sets it means that it should be split into separate databases.
Last updated: May 31 2023 at 17:01 UTC