As a side note, since the stdlib fails on warnings I had to port its code in the big second commit. It was mostly automated with a script adding global annotations everywhere. Thankfully, global hints inside a section raise an error so it was just a matter of turning it into a local annotation whenever it failed. Interestingly this reveals that some files are oblivious to the implicit local scoping of section hints. Indeed, they define local hints inside a section that are not used anywhere, i.e. dead code. I did not change those instances but it would deserve a deeper scrutiny.

It was mostly automated with a script adding global annotations everywhere.

Will you make this script available?

Indeed, they define local hints inside a section that are not used anywhere, i.e. dead code. I did not change those instances but it would deserve a deeper scrutiny.

Maybe worth to address those while the iron is hot?

Well, the script is quite trivial:

#!/bin/bash

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

Well, the script is quite trivial

It can still save time to hundreds of users (or more)...

The refman failure seems to be the root of most CI errors, but I can't say I understand its source. Any idea?

Regarding the need to document this warning in the refman, this could also be done outside this PR, given that we are working on this section with @jfehrle in #13343.

I agree with your first point, but not quite with the second one as argued in the top post, since it will merely postpone the problem for those commands. It's true that when a warning is triggered, it is a good time to consider an change towards export, but unfortunately this semantic switch is going to be really painful for our users. It's basically requiring to rewrite your development, so it's unlikely that people will do the change on the spot. More likely, they will do it in at most two steps, i.e. mark everything global, and secondly in a hypothetical future change global to export. But that latter step is going to be horribly time-consuming.

Alternatively, I can swiftly implement export for those commands, and this can make it into 8.13 if there is support from the RMs.

Alternatively, I can swiftly implement export for those commands, and this can make it into 8.13 if there is support from the RMs.

That would be wonderful.

@Zimmi48 see #13388. Full speed ahead, this needs to be merged before the freeze!

aac-tactics will need an overlay because they are building with all warnings fatal

coq-community/aac-tactics#67

I suggest this alternative plan:

* 8.13: warn for all `Hint` commands that support the `export` attribute, are outside sections, and do not have an explicit locality attribute.

* 8.14: add support for the `export` attribute for the remaining `Hint` commands and introduce the warning for those commands.

* 8.15: make this warning fatal by default.

* 8.16: change the default, remove the warning.

If we agree on this I believe we shall create these milestones and already open these issues with priority blocker

@gares The 8.13 and 8.14 steps can be merged together now that export is supported by all hint commands.

My alternative plan is made obsolete by all Hint commands now supporting the export attribute. So we are back to the initial plan. However, I would not make each of the next steps blocking for a release because longer deprecation periods won't hurt (except our will to move forward of course 😉).

Explicitly writing the attribute is easy and can be done in a semi-automated way as I did for the stdlib. In that sense, it's reasonable that people will perform this step quickly.

Hum, I'm a bit lost. Are you saying that the new plan is:

• 8.14: make this warning fatal by default.
• 8.15: change the default, remove the warning.

In any case, please open issues, my message was just a reminder to do so.

Hum, I'm a bit lost. Are you saying that the new plan is:

• 8.14: make this warning fatal by default.

• 8.15: change the default, remove the warning.

Yes.

@gares CI failures are spurious, this is ready to merge.

See #13394 for the issue, although I personally don't believe adding an issue to an ocean of despair to track this kind of ongoing endeavours is an effective solution. I bet we'll have forgotten about that issue by the 8.14...

See #13394 for the issue, although I personally don't believe adding an issue to an ocean of despair to track this kind of ongoing endeavours is an effective solution. I bet we'll have forgotten about that issue by the 8.14...

Thanks. I did put priority blocked, and it will show up on the milestone for the next RM. He will then ping you I guess.

@coqbot merge now

@ppedrot This change has a major impact on existing proof scripts. I think it is worth double-checking with the community that you haven't overlooked anything. Could you please write down and post it (before 8.13 freeze) on coq-club/zulip:

1. a short description of: what is the current behavior, what is the transition behavior, what is the long-term behavior.
2. a short description of how users need to modify their scripts, how they can do it at minimal cost (with a pointer to your shell script).

For part 2, please make sure to cover the most frequent pattern, where there are essentially 3 kinds of hints:

• a "Hint" in a section => Can I leave the hint without any modifier? It would be so much simpler if we could leave section hints to have a "local" scope by default; and to target an implicitly-existing "local core" data base---but that's another story).
• a "Hint" in a file, with the intention of having it being exported to other files that "require" the file with the hint. => These are hints that should be tagged Export explicitly, right? (I personally find it legitimate for this information to be provided explicitly.)
• a "Hint" in a file, with the intention of having it scope only within the current. => Will I need to add a modifier on those? they could by default scope only within the current module/file, right?

Btw, we're talking about hints here. But what is the "export" status of notation, and coercions, etc. Do the behaviors need to change? If so, whey, how and when? Thanks.

@charguer here is a note about the changes: https://coq.discourse.group/t/change-of-default-locality-for-hint-commands-in-coq-8-13/1140.

Note that Export won't work (it's only available as an alias for #[ export ] for Set / Unset). You'll have to use #[ export ] for Hint commands.

Here is a script I found useful for performing the conversion. It corrects errors in the earliest contribution.

coq13.txt

@jfehrle Your wording improvements look good. If you open a PR with them, I'll merge it.