[Merged by Bors] - doc(Tactic/ToAdditive/Frontend): more helpful error message when a name cannot be tr…#21716
[Merged by Bors] - doc(Tactic/ToAdditive/Frontend): more helpful error message when a name cannot be tr…#21716
Conversation
…ansported This would have helped me in #21422.
|
@YaelDillies Would you like to review this error message change? |
PR summary ff46efcfd3Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
| throwError "to_additive: the generated additivised name equals the original name {src}.\ | ||
| Usually, this means you need to name your declaration correctly \ | ||
| (e.g., name instances with a name that can be additivised). \ | ||
| Sometimes, this means you need to extend to_additive to handle the new names." |
There was a problem hiding this comment.
What about
| throwError "to_additive: the generated additivised name equals the original name {src}.\ | |
| Usually, this means you need to name your declaration correctly \ | |
| (e.g., name instances with a name that can be additivised). \ | |
| Sometimes, this means you need to extend to_additive to handle the new names." | |
| throwError "to_additive: the generated additivised name equals the original name {src},\ | |
| meaning that no part of the name was additivised.\ | |
| Check that your declaration name is correct\ | |
| (if your declaration is an instance, try name it)\ | |
| or provide an additivised name using the 'to_additive my_add_name' syntax." |
I'm not sure how relevant the part about instance is. I think something telling you to check the declaration name of an instance will immediately make you think of naming the instance. Otherwise it would be cool to give that part of the error message iff the erroring declaration is in fact an instance (we should be able to access this information here, right?)
There was a problem hiding this comment.
I like your suggestion. (I'm adding a test locally, hence tweaking it to make line breaks nice etc.)
There was a problem hiding this comment.
Accessing if this is part of an instance: this should be possible, to_additive takes a Syntax as input: however, I'd need to thread this all the way into targetName. Are you sure this is really useful?
There was a problem hiding this comment.
No, I think it would be cool, but not necessarily useful
There was a problem hiding this comment.
Then let me punt on this in favour of other changes I could make.
YaelDillies
left a comment
There was a problem hiding this comment.
Thanks!
maintainer delegate
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
bors d+ |
|
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: damiano <adomani@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
|
Thanks for the helpful reviews, all three of you! |
|
This PR was included in a batch that was canceled, it will be automatically retried |
|
Pull request successfully merged into master. Build succeeded: |
…ansported
This would have helped me in #21422.