Allow hints with no specified database inside sections.

[charguer]

This issue records that something needs to be done to properly handle the depreciation in 8.10
of hints added to the core database: #8987
Discussed with @Zimmi48 and @maximedenes

The illegitimate use pattern that the PR aims to get rid of is:

Hint Resolve mylemma. (* outside of any section, trying to extend the global database *)

Lemma bla... (* possibly in a different file, with a call to auto implicitly using mylemma. *)

However, one very legitimate use pattern is:

Section Foo. 
Hint Resolve mylemma.
Lemma bla...
End Foo.

I think it should continue to be accepted, in its current form, with the semantics that the hint spans over the section.

Yet to be addressed in the case of:

Section Foo. 
Lemma bla.
Proof.
   Hint Resolve mylemma. (* hint inside a proof *)
Qed.
End Foo.

Should this be allowed? Should the hint span over the current proof only (intuitive) or the entire section (not intuitive, but I think it's the current behavior).

Furthermore, as a facility for users who were previously relying on the core database, and for other users in general, one very nice feature would be to enable extending the "current" hint database with an existing database.

Hint Resolve bar1 bar2  : mydatabase. (* replace previous use of core *)

Section Foo. 
Hint mydatabase. (* here all mydatabase lemmas can be used by auto *)
Lemma bla...
End Foo.

Such a script could be a properly fixed version of the illegitimate pattern described at first in this thread.

Last, as a killer feature, one would be able to assign a name to the union of several bases. This would enable modularity in proof scripts. Such a desirable property.

Declare HintDb mybase1 := union mydatabase1 mydatabase2.

Ability to remove one or several hints would also be the next feature wish (that would require hint externs to be assigned explicit names, to allow referring to them).

Please note that:

• the "eauto with" syntax is good to have, but in general is super heavy and does not scale up well, in comparison to using per-section hints,
• rebinding "auto" to something else is super not modular (two libraries could rebind it differently).

Remark: if the syntax Hint Resolve foo. not inside a section is removed, it could then be reinterpreted as Local Hint Resolve foo, which has the meaning "use foo as a hint within the scope of the current file".

Summary of current proposal (see #10559 (comment))

• For every section, and for every module, an associated hint data base is created (think of it as the local extension to core).
• Hints with unspecified database are added to the database associated with the nearest enclosing section/module.
• The eauto tactic loads by default the hints from the databases associated with current section and current module (just like an eauto with would do).
• Command or option to set default hint database and disable the implicit-core-hint-db warning. #14752
• The command Create HindDb mybase := (union base1 base2 base3). can be used to create union of databases. If the implementation is tricky, we could start with the following interpretation: eauto with mybase is shorthand for eauto with base1 base2. This has a simple, well-defined semantics, probably quite close from the one that we want. We can warn users that this is an experimental feature, in particular the priority of how hints apply may be updated in a future release.

[Zimmi48]

Notations local to a section can be used to rebind auto / eauto though.
I'm putting the 8.10.0 milestone because part of this should at least be addressed by then. At the very least, the use case should not just be left unanswered even if no great solution is provided.
Related: #7650.

[Armael]

Notations local to a section can be used to rebind auto / eauto though.

That's only a very partial solution, which only works if I'm calling auto by hand, I think. It doesn't work in the more realistic case where I rely on some other tactic/notation which calls auto under the hood.

Actually, I tried defining a notation for auto, but it doesn't seem to be picked up:

Tactic Notation "auto" := (idtac "hello").
Goal True. auto. (* solves the goal *)

[Zimmi48]

I am a bit dubious regarding the silent postponing of this issue to 8.10.1. Since it seems that we are not going to be able to provide a satisfying answer to this question by 8.10.0, what about reporting the deprecation until we can find one? @maximedenes What do you think? Was it important to you that the removal of this feature happens in 8.11? Is there anything that is going to be blocked if it doesn't?

[charguer]

I would encourage indeed postponing the depreciation.
Is there any rush to issue depreciation warning for hints, given all the trouble it is going to generate?

[maximedenes]

given all the trouble it is going to generate

What trouble do you mean? To have to add : core to the warning declaration? It does not sound like the end of the world to me.

On the other hand, using an implicit global database seems like an obvious bad practice to me. I agree that it seems a bit less bad on local hints, although still not great since the tactic which uses these local hints will also depend on what is in core globally.

So I'd like to question the fact that this use is "legitimate", as is claimed here. If everything is local, why not use a local database (maybe copying an existing global one, but explicitly) ?

If the real problem is that the syntax is inconvenient / too verbose, let's work on improving that, rather than relying on shaky semantics.

[maximedenes]

Last, as a killer feature, one would be able to assign a name to the union of several bases.

FTR I tried to work on this, but we need to define what the union of bases is. For example, if two incompatible transparency flags are defined for the same constant, what should the result be?

[maximedenes]

What I can do to improve the current situation is to provide a Use HintDb foo command that will make hints be added to foo when they don't carry a database name.

Should it have effect on hint commands only? Or on automation tactics too? Should it be allowed anywhere, or only in a section?

[charguer]

Remark: the union of bases is already implicitly defined by the interpretation of "eauto with foo bar", which effectively considers the union of bases foo and bar (and core). I don't know if this specification of union is the desirable one, but it already exists, it seems to me.

[charguer]

Now if you'd like to go for something simpler than syntax/semantics for union of bases, here is my proposal.

Hint Resolve foo : base.  => ok
Hint Resolve foo.  => warning deprecated
Local Hint Resolve foo.   => new command; each section/module/file implicitly defines a hint database, which is implicitly used by eauto.
Local Hint Import base. => command to add the hint database "base" to what eauto uses in the current section/module/file. This saves the need to repeat, e.g. "eauto with arith" throughout one's file.

As a result, the current pattern that I explain above to be useful can be obtained simply by adding "Local" modifiers to the hints that I define.

In any case, any addition of a new mechanism deserves discussion and feedback, and it would be counterproductive to settle on some design for new features (whether Use HintDb foo or something else) in just a few days.

[charguer]

although still not great since the tactic which uses these local hints will also depend on what is in core globally.

To handle this, I would suggest "core" not be imported by default (eventually, this base should get deprecated). The command Local Hint Import core. can be used to obtain backward compatibility.

[maximedenes]

the union of bases is already implicitly defined by the interpretation of "eauto with foo bar",

That's the eauto union of bases, if you will. Then you have the typeclasses eauto union, etc (I think there are several different interpretations). Also, I wouldn't call that a union because it does not commute IIRC (but maybe that's a minor point).

eventually, this base should get deprecated

I agree, this was another motivation of the deprecation: all bases should be defined on the user side, not baked in the system. Also, they should be designated by qualids, not short global names.

To handle this, I would suggest "core" not be imported by default

Seems interesting, but what does imported mean here? That the "core" database would not be visible, or that it would not be picked up by automation tactics?

[charguer]

To handle this, I would suggest "core" not be imported by default
Seems interesting, but what does imported mean here? That the "core" database would not be visible, or that it would not be picked up by automation tactics?

The "core" database would exist, but would be deprecated and eventually eliminated.
By "not imported by default", I mean that "eauto" would not consider its hints. Unless Local Hint Import core is mentioned.

In other words, in the script

Local Hint Import base1 base2.
Hint Resolve lemma1.
Section X.
Local Hint Import base3.
Hint  Resolve lemma2.
eauto with base4 base5.

the last tactic is to be interpreted as

eauto with base5 base4 base3 base2 base1 using lemma1 lemma2.

Meaning that hint data bases are stacked, in the sense that more recent hints are considered before older hints, when their priority level is the same.
(I'm not sure this is the current behavior of eauto with base1 base2 using foo1 foo2, and I don't know if this was ever properly specified.)

[Zimmi48]

Please let's not talk about union of bases here. It already has its own issue and it is definitely not an 8.10 question. And for having thought about this with Armael, it is indeed far from trivial.

[charguer]

it is indeed far from trivial.

Agreed. Hence the suggestion to define everything in terms of "eauto with" multiple bases.
Hopefully this is simpler also from an implementation point of view.

[Zimmi48]

Hence the suggestion to define everything in terms of "eauto with" multiple bases. Hopefully this is simpler also from an implementation point of view.

I'd rather not implement a half-baked feature without carefully considering the long-term consequences of this design. The fact that it is difficult to define the union of databases does not mean that we should not do it.

---

Regarding my proposal to delay the deprecation to 8.11, this was just intended to leave the time to implement and properly test one of the idea that were proposed in this thread, like the Local Hint command.

[maximedenes]

There is something I don't understand, though. The proposals are talking about changing the semantics of the Hint command when not provided with a database. It seems better from the user point of view to do it in two steps (ask to make the current meaning of the syntax explicit using : core, then introduce the new meaning), rather than changing what exists without warning (then potentially debugging large Ltac programs whose behavior changed, etc).

[maximedenes]

Regarding my proposal to delay the deprecation to 8.11, this was just intended to leave the time to implement and properly test one of the idea that were proposed in this thread, like the Local Hint command.

So, if we implement something like the Local Hint command, when would the warning be emitted?

[charguer]

My suggestion would be to implement Local Hint as a beta feature in 8.10.x (for some x) so that it can be tested at scale. Then in 8.11, this new feature would be advertised, at the same time of making Hint Resolve foo. raise a depreciation warning, indicating that the "core" database is deprecated.

[maximedenes]

What I don't understand is what you do for people who already use Local Hint foo. today. They will never get a warning, will they? But the meaning of the command will change.

[Zimmi48]

The proposals are talking about changing the semantics of the Hint command when not provided with a database.

In the future yes, but not at once, no. (At least I would also recommend against this.)

It seems better from the user point of view to do it in two steps (ask to make the current meaning of the syntax explicit using : core, then introduce the new meaning)

The new feature could also be guarded behind an option, so that users can activate it manually and avoid adding all the : core annotations. Especially given that we want to remove core anyway.

My suggestion would be to implement Local Hint as a beta feature in 8.10.x (for some x) so that it can be tested at scale.

I disagree on the need on publishing a half-baked feature in 8.10. We are pretty capable of testing the feature during the 8.11 cycle.

[charguer]

The proposals are talking about changing the semantics of the Hint command when not provided with a database.

No, the point is to change the maning of Hint at once. We would only very slightly change the interpretation of Local Hint, as explained below.

What I don't understand is what you do for people who already use Local Hint foo. today. They will never get a warning, will they? But the meaning of the command will change.

Afaik, the current behavior of Local Hint foo is to add a hint locally to the core database, which is always considered by eauto within the local scope. If we reinterpret this command as adding a hint to a local database that is taken into account by eauto within the local scope, I think it is essentially equivalent, right?

The only caveat I see is the potential reordering of the hints considered by eauto. But I don't recall reading anything about the guarantees of eauto w.r.t. the order in which it considers the hints. How many proof script would be affected by that, when it comes to "local hints"?

Regarding the translation, it seems to me reasonably feasible to replace Section X. Hint Resolve foo. with Section X. Local Hint Resolve foo. Even if that takes some effort, it is something I can essentially manage to do with a script.

[ppedrot]

Should this be considered a blocker for 8.11?

[maximedenes]

I seem to recall that after discussing the real content of #8987 with @charguer during a WG, we agreed it was not a blocker.

[maximedenes]

In particular, it was in fact better to have a cycle with the deprecation before changing the meaning of hints with no specified database.

[ppedrot]

OK postponing then.

[Zimmi48]

@maximedenes What is the status of this? Should it still be considered for 8.12?

[Zimmi48]

Removing the 8.12 milestone. Let's address this before removing support for no specified database, but not urgent.

[charguer]

Let's address this before removing support for no specified database, but not urgent.

I think it's a good time to ping back on this issue. @Zimmi48 @ppedrot

Let me summarize my current proposal:

1. For every section, and for every module, an associated hint data base is created (think of it as the local extension to core).
2. Hints with unspecified database are added to the database associated with the nearest enclosing section/module.
3. The eauto tactic loads by default the hints from the databases associated with current section and current module (just like an eauto with would do).
4. The command Open HintDb mybase. loads mybase over the current section/module, meaning that eauto implicitly means eauto with mybase.
5. The command Create HindDb mybase := (union base1 base2 base3). can be used to create union of databases. If the implementation is tricky, we could start with the following interpretation: eauto with mybase is shorthand for eauto with base1 base2. This has a simple, well-defined semantics, probably quite close from the one that we want. We can warn users that this is an experimental feature, in particular the priority of how hints apply may be updated in a future release.

[Zimmi48]

I'm supportive of this proposal.
There might be some compatibility issue when implementing this change because using multiple bases (in a given order) is not equivalent to using a single bases with all its hints.
There is also the transparency hint question (which is taken from the first listed hint database IIRC).