Change of default locality for Hint commands in Coq 8.13

[ppedrot]

This small note describes a plan to change the default semantics of Hint commands w.r.t. scoping.

Summary of the situation

As for most commands, when declaring hints one can choose a locality that will change their scoping behaviour. As of 8.13, we have three possible explicit locality qualifiers for hint commands, namely:

• “local”
• “export” (introduced in 8.12 for basic hint commands, and in 8.13 for the remaining ones)
• “global”

The behaviour of those qualifiers depends on whether the command is issued within a section or not.

Inside a section:

• “local” means that the hint completely disappears at section closing time
• “export” is forbidden
• “global” is forbidden

Outside of a section:

• “local” means that the hint completely disappears at module closing time
• “export” means that the hint is made available whenever its enclosing module is imported
• “global” means that the hint is made available whenever its enclosing library (i.e. the toplevel module) is merely required

The “global” behaviour is frowned upon, because it makes writing modular libraries very hard. It is virtually impossible to control the order in which modules are actually required, and because module require is transitive, it is very easy to break a downstream development if some file in a library changes the set of files it requires. As such, the use of the “global” qualifier should be avoided.

Unfortunately, when a hint command has no explicit locality qualifier, as of 8.13 it defaults to the wrong behaviour outside of sections. Namely,

• inside of a section, the default is “local” (fine, and the only allowed qualifier anyways)
• outside of a section, the default is “global” (← THIS IS THE PROBLEM)

Since most people do not like to write text they deem useless, it means that many developments define global hints without even realizing. This creates a lot of modularity issues.

Towards a change of default behaviour

Since “global” should be avoided, the default implicit locality should not be “global”. One thus needs to change the default locality to the one that is more modular, i.e. “export”.

Unfortunately again, bluntly turning the default to “export” would be a very backwards-incompatible change. Therefore, the change needs to be incremental. The change of default is to be performed in three steps that will be synchronized with Coq releases.

• Step 1 (Coq 8.13): adding a hint without a locality qualifier outside of a section is temporarily deprecated. One has to explicitly write the corresponding attribute, otherwise a warning is triggered.

• Step 2 (Probably Coq 8.14): this warning is turned into an error by default.

• Step 3 (Probably Coq 8.15): the warning is removed, and hints without a locality outside of sections are allowed again, but this time their default behaviour is now “export”.

Note that hints inside a section are totally unaffected by these incremental changes.

The step increment is not necessarily going to be increased at a distance of only one release, if we realize that the explicit annotation process is not performed fast enough in the wild.

What I, the maintainer of a Coq library, have to do

TL;DR

In Coq 8.13

You should explicitly add a locality qualifier to every hint declaration outside of a section from your library. Choosing the right qualifier depends on your situation.

QUICK & DIRTY

You should use the backwards-compatible #[global] attribute.

The following script uses a dumb pattern-matching to do that semi-automatically.

#!/bin/bash
# Invoke as ./script.sh MYLIBRARYFOLDER

pattern() {
  PATTERN="s/^\(\s*\)$1/\1#[global]\n\1$1/g"
  sed -i "$PATTERN" $2
}

for i in $(find $1 -name "*.v");
do
pattern "Hint Resolve" $i
pattern "Hint Immediate" $i
pattern "Hint Extern" $i
pattern "Hint Constructors" $i
pattern "Hint Unfold" $i
pattern "Hint Variables" $i
pattern "Hint Constants" $i
pattern "Hint Transparent" $i
pattern "Hint Opaque" $i
done

This is a stupid sed, so in particular it will also add a #[global] attribute to hints inside a section, which will fail at runtime. You will have to remove those attributes by hand. It will also probably miss a few hints that do not conform to the regexp, but those ones will trigger the warning.

(VERY) SLOW & BETTER

We recommend that you consider using the backwards-incompatible #[export] attribute instead. This change will be very work-intensive, because you will need to track the uses of your hints and explicity import modules that were only (possibly silently) required before. Since importing a module also imports a lot of unrelated stuff (e.g. notations…) this will be a mess and it might need a reorganization of the library. Yet, it will result in a more modular library so this is a very welcome change. It will also affect your downstream users, because Require-scoping sucks, but once again it is a one-time investment.

Note that you can first go for the quick-n-dirty solution, then in a second time incrementally convert your library to the recommended export locality. It will be less easy to realize that you defined a global hint though.

In Coq 8.14

Nothing.

In Coq 8.15

You will be able to remove the explicit annotation if you want. We might provide an option to do that in a more transparent way starting from 8.14.

To insist: hints inside a section are totally unaffected by these incremental changes. You don’t have to do anything for those, and actually all flags that succeed have the same semantics.

[Blaisorblade]

@ppedrot

• “export” is forbidden
• “global” is forbidden

Really? I’ve used several Global Hint in Sections, especially Global Instance (just rechecked). Is this a mistake, a regression, or an intentional change?

[ppedrot]

What version are you using? Coq 8.10 already forbids global hints in a section and I am too lazy to check for prior versions.

EDIT: The last version whose binaries are compiled on my machine is Coq 8.6 and it was already forbidden.

[ppedrot]

I think that you are confusing hints and typeclass instances. While the latter also defines hints in the typeclass_instance database, it is not the only action performed by this command, as it also registers meta-data for the typeclass algorithm. As such, Instance is not considered a Hint command. Unfortunately, Instance does not support the export attribute yet, so we will have to perform the same kind of process for typeclass instances as well in a later version. But it can be done independently.

[charguer]

@ppedrot Thanks for the note.

so we will have to perform the same kind of process for typeclass instances as well in a later version

Is this a good idea to perform twice the same process, once for hints, and once for typeclass instance, not in a synchronized way? This would only add yet more confusion, don’t you think?

[charguer]

One thing that is kind of unsatisfying is that if I have a library that already intends to use “local only” hints, then I will have to edit my files twice, once to add “local” (for step 1), then once to remove it (at step 3), because I see no reason of leaving a “Local” annotation in front of every hint in my files for ever if this annotation matches the behavior.

Perhaps I’d be tempted to just skip a couple versions, rather than going through the sed process?
A more user-friendly, equivalent solution to skipping versions might be to provide, at step 2, a warning flag that I can turn off to disable the error, in other words, allowing me to anticipate on the long-term behavior (step3). Typically, warnings are used to make life easier for backward-compatibility, but here it would be used to make it easier for forward-compatibility.

[SkySkimmer]

@charguer

One thing that is kind of unsatisfying is that if I have a library that already intends to use “local only” hints, then I will have to edit my files twice, once to add “local” (for step 1), then once to remove it (at step 3), because I see no reason of leaving a “Local” annotation in front of every hint in my files for ever if this annotation matches the behavior.

Local matches the default behaviour only in sections, where you don’t need to change anything.
The outside section default behavour is planned to be export.

[charguer]

The outside section default behavour is planned to be export.

Ah, sorry, I had misread something and thought that “local” would be the default.

My long-term vision of Coq is one where (1) everything would be local by default, to discourage pollution of the global environment, and (2) one could define in a library bundles of “stuff” (hints, notations, coercions, instances) that library users would be free to load on a per-need basis. With that goal in mind, while waiting for the notion of “bundles of stuff” to exist, the “export” flag would remain the mean to package things away, by attaching them to the current module. In other words, I would naturally suggest “local to the module” to be the default, and “export” to be explicitly required.

But I understand that my long-term plans might be too far away from the existing design to be considered today.

[tchajed]

I ported Iris automatically using a slightly different script approach. The idea was to modify any line where Coq emitted the warning. Here’s a script to do that parsing, fix.py:

#!/usr/bin/env python3

import sys
import re

error_re = re.compile(r"""^File "(?P<file>[^"]*)", line (?P<line>[0-9]+), characters .*:""")

for line in map(str.rstrip, sys.stdin):
    m = error_re.match(line)
    if m:
        file, line = m.group("file"), m.group("line")
        print(f"gsed -i '{line}s/^/Global /' '{file}'")

Now we can gather up all the commands needed and run them: make 2>&1 | ./fix.py > fixes.sh && bash fixes.sh.

This worked for us because -deprecated-hint-without-locality was the only warning being generated.

[RalfJ]

@SkySkimmer

Local matches the default behaviour only in sections, where you don’t need to change anything.
The outside section default behavour is planned to be export.

FWIW, I think the fact that the default depends on whether or not this is inside a Section is bad. This means when I review a PR, I need to look not just at the diff but also be aware everywhere whether some code is inside a Section or not – which might be impossible to tell from the diff alone.

As far as I understand, this is because Global/Extern Hint just does not work inside Section. In that case I’d rather have a bare Hint fail, such that explicit Local Hint is required. IMO, that’s much better than just changing the default. If Coq added a flag to enforce this, I’d enable it in Iris immediately.

Of course, @charguer’s proposal of making Local the default would also nicely solve this issue.

[RalfJ]

@ppedrot

The “global” behaviour is frowned upon, because it makes writing modular libraries very hard. It is virtually impossible to control the order in which modules are actually required, and because module require is transitive, it is very easy to break a downstream development if some file in a library changes the set of files it requires. As such, the use of the “global” qualifier should be avoided.

I agree that the behavior of Global is bad. However, it actually has one nice consequence: it provides a way that I can import (some of) the interesting “side-effects” of a library without having its names shadow other names I imported before. Often I care for a library only to obtain its notations, typeclass instances, canonical instances, things like that, but I do not actually intend to refer to any of its names directly. In that case, importing the library does “too much”, and that can actually be a problem when imports are otherwise carefully ordered to perform selective shadowing of named identifiers, or when the import messes up the scope stack (this actually is a regular problem, with imports randomly putting nat_scope vs Z_scope on top of the stack; also see this issue).

Clearly, Global is not a proper solution to this, since it provides no opt-out and since it only applies to TC instances and hints. But in some sense this change removes a bit of (accidental?) expressiveness from the Coq module system. See this Iris issue for some more discussion around when to Import vs Export and the problems that come with it (and that currently cannot be avoided, I think).

[Blaisorblade]

You’re right I confused confusing hints and instances…

@ppedrot

Unfortunately, Instance does not support the export attribute yet, so we will have to perform the same kind of process for typeclass instances as well in a later version. But it can be done independently.

If the change is independent, either Hints for typeclasses remain Global for now, or instances must be replaced by #[export] Hint Resolve commands.

[Zimmi48]

In Coq 8.14, there is also a warning being generated for instances (Instance) outside a section without an explicit locality. To automatically add #[ global ] to those, I recommend following the approach of @tchajed rather than @ppedrot because since #[ global ] is actually also supported on instances inside sections, adding it blindly everywhere would produce a change of behavior for those instances inside sections.

EDIT: this might be difficult to do in practice because of `Instance` raises locality warning at `Qed` / `Defined` time. · Issue #15030 · coq/coq · GitHub

[RalfJ]

@Zimmi48

To automatically add #[ global ] to those, I recommend following the approach of @tchajed rather than @ppedrot because since #[ global ] is actually also supported on instances inside sections, adding it blindly everywhere would produce a change of behavior for those instances inside sections.

That won’t work though since Coq 8.14 prints the wrong line numbers in these warnings. I don’t currently know of a way to automatically fix these deprecation warnings in Coq 8.14 (and a manual fix is out of the questions due to the sheer number of warnings).