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.
In particular, it seems that Program Instance generates new hint databases on the fly (!)
Is this a design choice, or is there something very fishy going on? cc @Matthieu Sozeau
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).
What does the database contain?
It happens in CRelationClasses, with Program Instance impl_Reflexive : Reflexive impl.
I'm curious, is this a prerequesite for turning hint databases into properly scoped objects at some point?
yes.
Ok, I'm happy to help :)
(and as usual, it's a rabbit hole)
Can you look in the db ?
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
?
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
Hmm I see. Hint unfolds are declared for the obligations of (every?) program definition?
what's the point if they are secluded in a database that lies around?
(this patch also uncovers quite a lot of very suspicious activity around hint dbs in the stdlib btw)
Well, it lets you use them if you want, using auto with foo
Without scoping? This is a recipe for disaster.
If people happen to define a program instance with some generic name, it will appear randomly in unrelated places.
Well yes. Ideally you would like to be able to scope this hint database as foo.unfolds
or foo.obligations
So, you confirm it's an intended behaviour?
Expect trouble downstream.
The transition phase is going to be painful, with people wondering where their database clash are coming from.
Yes, it's intended that we create the database.
However, it's probably very seldom used
You could imagine an attribute for Program to declare these hints in a particular database.
'mkay
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.
Superglobal is back, and it is pas content
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
?
No, it's linked to the fact that there is no proper semantic for duplicate database creation.
So if you haphazardly create databases automatically through commands you're bound to get weird behaviours.
I am porting the stdlib to the warning right now and it's a festival.
There are hints spread around declaring implicitly different hint databases.
In files that are not even related by require.
Sure, as long as we don't have scoping this is broken
No no, it's supposed to be the very same database.
but there is no single place to put it, since there is no sup of the require chain.
Oh, ok, how come you get different results?
You mean that e.g. precedence of hints is not commutative?
Declaring a database erases the old one, if there is already one with the same name.
But one should definitely not be allowed to declare the same database twice!
Yes, but that is the problem.
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?
I am not talking about program now.
Several Arith files declare the db arith several times.
(implicitly)
but there is no root file required by everybody in which the db creation could be put
In the file declaring nat
?
This is a design choice, which will matter when databases are scoped.
Sure, I am just disputing the fact that there is no sup.
Well it's not a sup, it's an upper bound.
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.
But it's not unique, so you have to think.
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.
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
Inquiry: where does the sets
database live?
it's used by unrelated parts of the stdlib.
amongst others, theories/Sets/
obviously, but also theories/Relations/
Perhaps theories/Init/Datatypes.v
? (Or any other from Init
.)
I am slightly concerned that polluting the prelude with stuff that is barely used at all is going to be problematic for our users.
Maybe in the case of sets
it means that it should be split into separate databases.
Last updated: Dec 07 2023 at 18:01 UTC