Tweak the warning for arbitrary term hints. #12678
Conversation
ppedrot
force-pushed
the
tweak-hint-constr-warning
branch
from
0a9b3ae
to
9f2c91e
Compare
| @@ -64,11 +64,11 @@ let project_hint ~poly pri l2r r = | |||
| (info, false, true, Hints.PathAny, Hints.IsGlobRef (Names.GlobRef.ConstRef c)) | |||
|
|
|||
| let warn_deprecated_hint_constr = | |||
| CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated" | |||
| CWarnings.create ~name:"fragile-hint-constr" ~category:"automation" | |||
There was a problem hiding this comment.
Note that @SkySkimmer recently introduced the "fragile" category, which could also be relevant in this case (so far, it only has one warning).
vernac/comHints.ml
Outdated
| "Declaring arbitrary terms as hints is deprecated; declare a global \ | ||
| reference instead") | ||
| "Declaring arbitrary terms as hints is fragile; it is recommended to \ | ||
| declare a global reference instead") |
There was a problem hiding this comment.
The term "global reference" may be too technical in this context?
There was a problem hiding this comment.
What would you prefer to have there?
There was a problem hiding this comment.
No concrete idea, as discussed on the 8.12 release thread on Zulip I found the warning a bit confusing for users; in the sense that if I'm a user what I'm supposed to do here; why is this fragile? Am I in danger or not? It would be a bit messy that we have users adding dozens of new dummy definitions just to find out that we can support this better.
Maybe it would be good to add some documentation on the hint command itself.
Going back to the comment, I dunno, maybe "top-level constant" or "give the hint a name"; I'm sorry I don't have a better idea.
There was a problem hiding this comment.
I think "global reference" is OK as it is used sometimes in the documentation, but I do prefer the suggestion of "top-level constant".
There was a problem hiding this comment.
Constructors are ok too though
There was a problem hiding this comment.
and variables (eg from pose)
There was a problem hiding this comment.
The warning will not trigger for those, so I think it's fine.
This is about the third time I try to kill this file but for some reason it is still here.
ppedrot
force-pushed
the
tweak-hint-constr-warning
branch
from
9f2c91e
to
f41fcca
Compare
|
@ejgallego Can we merge this now? |
I guess so; should we add an entry in the refman? |
It would be good to do so if this does delay the release too much. |
I am not what is the sphinx magic to document a warning, the text could be something such as:
Indeed it was no 100% to me what the user-visible drawbacks are. |
|
@ppedrot would you mind filling in the ??? in
|
|
Anyways let's merge this one now and do the backport. |
|
To document a warning, use |
Fixes #11970.