Stream: Coq devs & plugin devs

Topic: Warning on implicit hint database declaration


view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 15:39):

In particular, it seems that Program Instance generates new hint databases on the fly (!)

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Matthieu Sozeau (Mar 22 2021 at 15:41):

What does the database contain?

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 15:42):

It happens in CRelationClasses, with Program Instance impl_Reflexive : Reflexive impl.

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 15:42):

yes.

view this post on Zulip Matthieu Sozeau (Mar 22 2021 at 15:42):

Ok, I'm happy to help :)

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 15:42):

(and as usual, it's a rabbit hole)

view this post on Zulip Matthieu Sozeau (Mar 22 2021 at 15:43):

Can you look in the db ?

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 15:44):

the database is conspicuously named impl_Reflexive

view this post on Zulip Matthieu Sozeau (Mar 22 2021 at 15:44):

Hmm I see. Hint unfolds are declared for the obligations of (every?) program definition?

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 15:45):

what's the point if they are secluded in a database that lies around?

view this post on Zulip 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)

view this post on Zulip Matthieu Sozeau (Mar 22 2021 at 15:45):

Well, it lets you use them if you want, using auto with foo

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 15:46):

Without scoping? This is a recipe for disaster.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 15:48):

So, you confirm it's an intended behaviour?

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 15:48):

Expect trouble downstream.

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Mar 22 2021 at 15:50):

Yes, it's intended that we create the database.

view this post on Zulip Matthieu Sozeau (Mar 22 2021 at 15:50):

However, it's probably very seldom used

view this post on Zulip Matthieu Sozeau (Mar 22 2021 at 15:51):

You could imagine an attribute for Program to declare these hints in a particular database.

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 15:52):

'mkay

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 16:14):

Superglobal is back, and it is pas content

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 16:21):

There are hints spread around declaring implicitly different hint databases.

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 16:21):

In files that are not even related by require.

view this post on Zulip Matthieu Sozeau (Mar 22 2021 at 16:23):

Sure, as long as we don't have scoping this is broken

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 16:23):

No no, it's supposed to be the very same database.

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Mar 22 2021 at 16:23):

Oh, ok, how come you get different results?

view this post on Zulip Matthieu Sozeau (Mar 22 2021 at 16:24):

You mean that e.g. precedence of hints is not commutative?

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Mar 22 2021 at 16:25):

But one should definitely not be allowed to declare the same database twice!

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 16:25):

Yes, but that is the problem.

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 16:25):

I am not talking about program now.

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 16:26):

Several Arith files declare the db arith several times.

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 16:26):

(implicitly)

view this post on Zulip 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

view this post on Zulip Guillaume Melquiond (Mar 22 2021 at 16:26):

In the file declaring nat?

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 16:27):

This is a design choice, which will matter when databases are scoped.

view this post on Zulip Guillaume Melquiond (Mar 22 2021 at 16:27):

Sure, I am just disputing the fact that there is no sup.

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 16:28):

Well it's not a sup, it's an upper bound.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 16:31):

But it's not unique, so you have to think.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 16:43):

Inquiry: where does the sets database live?

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 16:43):

it's used by unrelated parts of the stdlib.

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 16:44):

amongst others, theories/Sets/ obviously, but also theories/Relations/

view this post on Zulip Guillaume Melquiond (Mar 22 2021 at 16:49):

Perhaps theories/Init/Datatypes.v? (Or any other from Init.)

view this post on Zulip 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.

view this post on Zulip 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: Oct 21 2021 at 21:03 UTC