Can't practically improve my Hint locality in Coq 8.13.0

[andrew-appel]

Normally when a new version of Coq comes out, I adjust my big Coq development to avoid using deprecated features. Unfortunately, Coq 8.13.0 is not mature enough for me to do this regarding the new Hint locality deprecation warning, deprecated-hint-without-locality. Because I believe this problem will be annoying for many users, I write this message here as a bug report, instead of just adding a reply to the Zulip topic.

I want to adjust my development the "right" way, not the "quick and dirty" way. That is, I don't want to simply add Global to every Hint, I want them to have the recommended #[export] locality.

First problem: The deprecation message says, 'It is recommended to use "export" whenever possible' but gives no clue about how to use "export." I have been using Coq for many years, but never used an 'attribute' before, and it took 30 minutes of detective work in the refman before I figured out that one must write #[export] before the Hint. (Try the experiment yourself, pretending you didn't already know...). So, je vous prie, adjust the deprecation warning to say, "It is recommended to use #[export] Hint rather than just Hint, whenever possible."

Second problem: After studying all the relevant documentation, I concluded that I should write,
Global Set Loose Hint Behavior "Warn" and then eliminate all the warning messages about "Hint used but not imported". But I find that most of those messages are caused by Coq's built-in tactics such as reflexivity and lia. As a user I can't solve that problem myself.

Third problem: The #[export] mechanism doesn't work for Instance, as is known.

Therefore: In Coq 8.13.0 it is not possible for users to systematically and reliably adjust their developments to the new style of Hint locality, without the hassle of filtering out warning messages that come from Coq's own built-in tactics, and given the problem that Instances don't work properly. I feel that it is best to abandon the effort to adapt my development. That is, I will simply suppress the warning, via Global Set Warnings "-deprecated-hint-without-locality", until a new release of Coq comes out that fixes these two issues.

And therefore, the aggressive schedule by which Coq 8.15 will have different, incompatible behavior should be reconsidered until such time as an intermediate release of Coq does realistically permit users to adapt.

[JasonGross]

Second problem: After studying all the relevant documentation, I concluded that I should write,
Global Set Loose Hint Behavior "Warn" and then eliminate all the warning messages about "Hint used but not imported". But I find that most of those messages are caused by Coq's built-in tactics such as reflexivity and lia. As a user I can't solve that problem myself.

If this warning message does not mention which hint / database is used, then it should be updated to mention that. Ideally it should also mention which file the hint was declared in. In this case I suspect it is the typeclass_instances. The solution to these warnings, I believe, is to Import the module declaring the hint being used by reflexivity / lia, rather than to adjust the tactic itself.

[andrew-appel]

I disagree that "the solution is to Import the module declaring the hint used by reflexivity/lia". As a user of Coq, I treat those tactics as abstractions, and I shouldn't need to know what modules they rely on.

[JasonGross]

And therefore, the aggressive schedule by which Coq 8.15 will have different, incompatible behavior should be reconsidered until such time as an intermediate release of Coq does realistically permit users to adapt.

There is an easy backwards-compatible fix in this case, though: replace all Hint with Global Hint when not enclosed in a section. Although Global is frowned upon, it seems better to be explicit about it. AFAIK there is no concrete plan yet to deprecate Global, and thus users are free to adapt to Global Set Loose Hint Behavior "Warn" and replace Global with #[export] at their convenience. I would suggest that rather than issuing Global Set Warnings "-deprecated-hint-without-locality" you instead just stick Global in front of all your hints, and you can move to #[export] once Global Set Loose Hint Behavior "Warn" has better warnings and the coqdevs update the standard library to remove Global hints.

[andrew-appel]

I fully understand that I could make every hint Global. But, as I understand it, the point is that users are really encouraged to use #[export] rather than Global. I could remark that #[export] is quite ugly syntax, but that shouldn't matter, because in the glorious future one will simply write Hint Resolve and it will default to "export". But to get to that glorious future, users will need the tools to analyze the use of their hints; and my message just points out that the time is not yet ripe for users to do that.

[JasonGross]

I disagree that "the solution is to Import the module declaring the hint used by reflexivity/lia". As a user of Coq, I treat those tactics as abstractions, and I shouldn't need to now what modules they rely on.

I mostly agree with you about lia (but note that zify is extensible via typeclasses and hence the behavior depends on whether or not it's been extended in this way). On the other hand, reflexivity will solve a goal of any relation with a Reflexive instance. Consider:

Require Import Coq.Setoids.Setoid.
Global Set Loose Hint Behavior "Warn".
Axiom R : nat -> nat -> Prop.
Module foo.
  Global Instance R_Reflexive : Reflexive R.
  Admitted.
End foo.

Goal R 0 0.
  reflexivity.
  (* Warning: Hint used but not imported: exact foo.R_Reflexive from foo [non-imported-hint,automation] *)

What should the behavior be here?

[andrew-appel]

Perhaps you are right about user-defined reflexive instances, but I'm getting warning messages that complain that I should Import Z in order to use reflexivity. That seems a bit much.

[JasonGross]

Plausibly the fix to the warnings from lia is that the standard library should Export the modules declaring the hints in the module that defines lia, rather than merely Importing them. I suspect that a similar reorganization needs to be done to the standard library to fix the issues with warnings on reflexivity. I expect the coqdevs would find it useful to have a suite of small test-cases that currently emit warnings but should not, which should get added to the test-suite to ensure that they do not emit warnings.

[gares]

CC @ppedrot @coq/doc-maintainers

[JasonGross]

but I'm getting warning messages that complain that I should Import Z in order to use reflexivity

Do you have an example reproducing this warning?

[andrew-appel]

Require Import ZArith.
Global Set Loose Hint Behavior "Warn".
Goal forall a b, (a | b)%Z.
intros. try reflexivity.

Hint used but not imported: exact Z.divide_reflexive from Z

[gares]

And therefore, the aggressive schedule by which Coq 8.15 will have different, incompatible behavior should be reconsidered until such time as an intermediate release of Coq does realistically permit users to adapt.

I'm sorry if the announcements looked aggressive. I'd say 8.15 is an optimistic schedule; we are aware it won't be easy to match, and we've already decided that we will extend the deadline if problems arise. At the same time not all users are as diligent as you are (thanks for that!). So we played the deadline card, I hope you can understand.

[SkySkimmer]

Forget about Loose Hint Behaviour, just use the attributes.
Loose Hint Behaviour affects how libraries are imported, not how hints are declared, so it's hard to use.

[andrew-appel]

As I understand it, the purpose of "Loose Hint Behavior Warn" is to diagnose those places where one would run into difficulty when changing a Hint from (current default) Global to (future default) #[export]. If I am going to change hundreds of Hints throughout my system, I certainly do want such a diagnostic aid. The value of this aid would be improved if the Coq standard library obeyed the rules. Two examples are discussed above:

1. lia should follow best practices so that LooseHintBehWarn doesn't make it squawk; and
2. Users (and the reflexivity tactic) should not be required to Import Z; we generally prefer to make use of name disambiguation by writing Z.to_nat with an explicit module name. Therefore, Hints should be outside of but adjacent to Z, of the form,
   #[export] Hint Resolve Z.divide_reflexive

[ppedrot]

But, as I understand it, the point is that users are really encouraged to use #[export] rather than Global

This is definitely true for newly written code. But there is no easy switch from global to export hints, this will require a huge refactoring for any development of a reasonable size, and it will cascade down to code that depends on a library. This is why this change of semantics was introduced via a warning. It is not reasonable to believe that big libraries will switch overnight to export semantics, but in the meantime we really, really want people to stop introducing global hints.

[Zimmi48]

We've might have done a bad job at communicating the plan but the idea is that the faster existing projects add Global annotations to their code (thus keeping the current behavior unchanged), the faster we will be able to switch the default to the better-behaved export attribute and thus the less (future) code will rely on this terrible semantics that hints are loaded at Require time.

There's a possibility though that we will anyway delay the next steps of the process for one more release so that more commands support the export attribute first (see #13394).

We do not yet have a plan to switch existing code from global to export (but it is kind of independent of the above consideration). Note that the Loose Hint Behavior option is not considered as a good solution anymore and in particular the documentation around this option should be reworked (see #13370).

[Zimmi48]

In particular, I should add that the standard library was "fixed" for this change by adding Global annotations anywhere (thus keeping the old semantics for existing hints).

[ppedrot]

Note that the Loose Hint Behavior option is not considered as a good solution anymore

Yes and no. Before the introduction of the export attribute I agree it was indeed mostly useless. Now that the user can cherry-pick the scoping behaviour on a per-hint basis, it can be used as @andrew-appel did to help the incremental transition to export semantics, although it's still painful and too verbose. It should probably be extended with a table to selectively blacklist hints in order to focus on a particular set of hints being ported to export scoping, but the underlying mechanism is the same.

Note that due to the way auto and eauto work, Loose Hint Behaviour is an overapproximation. It might report used hints that are not even needed for the search to actually succeed.

[Zimmi48]

We discussed this issue and related ones in today's call and concluded that we should improve the warning message so that it clearly recommends two different course of actions for fixing the warning:

• if you are porting existing code to a new version of Coq, the most backward-compatible fix is to add Global (and thus it is the recommended way);
• if you are getting this warning while writing new code, you should always prefer the export attribute (and the warning message should show the syntax #[ export ]).

Also discussed was how to improve Loose Hint Behavior to make it more useful. One thing in particular is that it shouldn't warn on stdlib hints. There are several options:

• One way would be to remove global hints from the standard library. This is less backward-compatible but @JasonGross remarked that if we export the hints from the right files, then it is likely that users are already importing those files in their code. While today, it is expected that you rely on hints from modules that you didn't directly import but that you transitively required. It was noted that we don't have a feature for re-exporting only hints from a module. However, what we can do is to seal only hints in a sub-module and re-export that one wherever it makes sense. So this is doable with the current infrastructure.
• Another way (which could complement the previous one) would be to make it possible to disable the Loose Hint warning / error for some hints, e.g. by annotating them or adding them to a table. By default, it would be the case of the hints defined in the stdlib.

[JasonGross]

There's a third option, which is to export the hints from the right files without marking them as #[export]. This is completely backwards compatible and at the same time should ensure that most hints don't get used without being imported (since I believe the warning only occurs when the Global hint is used without being imported, not when any Global hint is used at all).

[Zimmi48]

completely backwards compatible

Completely backward-compatible? What if you used to import only the files which defined the hints?

[JasonGross]

Completely backward-compatible? What if you used to import only the files which defined the hints?

Then nothing would change? To be concrete, I'm proposing that we move all hints to their own module (without changing what file they're defined in), and exporting these modules from selected files that currently only import the enclosing file/module. Since the hints are Global and we do not change the file they're defined in, nor change any Requires, nor change any Imports nor Exports of modules containing anything other than Global hints, the behavior of Coq is unchanged except with respect to this warning. The benefit of doing this is that it allows us to figure out how to structure hints now, and paves the way to making all hints in the stdlib be marked export with fewer compatibility issues.

[Zimmi48]

OK, thanks for clarifying!

[andrew-appel]

In the end, I went through all of VST and edited every Hint (adding #[export], Global, or Local as necessary) to avoid the deprecation messages. I did this without using "Set Loose Hint Behavior" because, as discussed above, that is not very useful until some adjustments are made. VST was already using Hint in a way that almost every hint was intended as #[export]; this is what made it possible to make this change without the benefit of "Set Loose Hint Behavior".
So, in the end, I did "practically improve my Hint locality." I still think #[export] looks a bit ugly before every Hint.

[gares]

I still think #[export] looks a bit ugly before every Hint.

Hopefully at some point we will make it the default, and you will be able to remove it.

[ppedrot]

As far as I understand, we can close this issue.