Bad line number for warning about implicit Global on Instance

[RalfJung]

Description of the problem

The following code:

Class Test := { wit : nat }.

Instance test: Test.
Proof. constructor. exact 0. Qed.

produces a warning on Coq master:

File "/tmp/test2.v", line 4, characters 29-33:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]

However, the line number of the warning is wrong: it points at the Qed, when it really should point at the Instance since that is where the problem lies.

This is particularly annoying since it means automatic scripts that parse these warnings to add the missing explicit Global will edit the wrong line. (I found such scripts to be the only way to actually deal with this warning -- we get many dozens of these warnings in basically each of our developments; fixing them all by hand would be horrible.)

Coq Version

Coq master

[Alizter]

cc @ppedrot

[ppedrot]

Unfortunately I don't think there is an easy way for that. When porting the code, the script I wrote was performing a reverse lookup with a bounded number of lines to find the corresponding instance command. Quite hackish but was working OK in most of the cases. See ppedrot@ba3f284.

[Alizter]

So I take it the locality check is being performed at qed time. Is there anyway to do a preliminary check before entering proof mode?

Also, this might be a bit hackish, but isn't there code to jump to the start of a deceleration? I've seen this behaviour when trying to Qed an invalid CoFixpoint. So it seems to me that such information can be stored.

[RalfJung]

Or maybe a way to remember the spam (line and column) of the declaration so that we Qed time one can still print warnings pointing at the declaration?

[SkySkimmer]

See #14705

[RalfJung]

Is there any chance this can be backported to the 8.14 branch? Right now all developments being ported to 8.14 show massive amounts of warnings about unqualified Instance, so an automated script is pretty much the only way to get those developments ported (other than silencing the warning) -- however, not only does Coq not offer such a script (so everyone has to write their own hacks), the script will also do the wrong thing because the line numbers are incorrect. The only way to get correct line numbers is to port the development all the way to 8.15, which is a lot of extra work and might not be possible if some dependencies are not ready yet.

EDIT: Ah I see this is already tracked at #15030.