Skip to content

[Merged by Bors] - chore(AtLocation): clean up backtick handling#37999

Closed
grunweg wants to merge 4 commits intoleanprover-community:masterfrom
grunweg:backticks-atlocation
Closed

[Merged by Bors] - chore(AtLocation): clean up backtick handling#37999
grunweg wants to merge 4 commits intoleanprover-community:masterfrom
grunweg:backticks-atlocation

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Apr 13, 2026

Make errors in AtLocation surround the tactic name with backticks by default. This fixes a few error messages to comply with mathlib's style guide.

Extracted from #37899.

Open in Gitpod

@grunweg
chore(AtLocation): clean up backtick handling
6cc7c33 
Make errors in AtLocation surround the tactic name with backticks by default.
This fixes a few error messages to comply with mathlib's style guide.

Extracted from leanprover-community#37899.
@grunweg grunweg added easy < 20s of review time. See the lifecycle page for guidelines. t-meta Tactics, attributes or user commands awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Apr 13, 2026
@grunweg grunweg requested a review from adomani April 13, 2026 13:20
This was referenced Apr 13, 2026
Closed
Open
@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 13, 2026 •
edited
Loading

PR summary 0b45e1648d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@grunweg grunweg removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 13, 2026
@grunweg grunweg mentioned this pull request Apr 13, 2026
Closed
1 task
@grunweg grunweg requested a review from thorimur April 13, 2026 15:32
@grunweg grunweg mentioned this pull request Apr 13, 2026
Open
5 tasks
thorimur
thorimur reviewed Apr 14, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@thorimur thorimur left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good! I'm suggesting putting the assumption about proc in the docstring so writers can see it at the call site. :) I think these suggestions should be all of them.

I looked up other uses of the transform* functions used here, and apparently they weren't using backticks! So this looks like a good change. :)

maintainer delegate

@thorimur
Copy link
Copy Markdown
Contributor

thorimur commented Apr 14, 2026

Let me alert the bot, it seems to have missed the edit:

maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 14, 2026

🚀 Pull request has been placed on the maintainer queue by thorimur.

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 14, 2026
@adomani
Copy link
Copy Markdown
Contributor

adomani commented Apr 14, 2026

Thanks for the PR and the review!

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 14, 2026

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@mathlib-triage mathlib-triage bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Apr 14, 2026
grunweg and others added 2 commits April 14, 2026 11:42
@grunweg @thorimur
Apply suggestions from code review
530feb6 
Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>
@pre-commit-ci-lite
[pre-commit.ci lite] apply automatic fixes
d361f98
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Apr 14, 2026

Thanks for the quick review!
bors merge

mathlib-bors bot pushed a commit that referenced this pull request Apr 14, 2026
@grunweg
chore(AtLocation): clean up backtick handling (#37999)
24d5e2d 
Make errors in AtLocation surround the tactic name with backticks by default. This fixes a few error messages to comply with mathlib's style guide.

Extracted from #37899.
@mathlib-triage mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Apr 14, 2026
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 14, 2026

Canceled.

Address comments or fix if necessary, and then someone with permission can run bors r+.

@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Apr 14, 2026

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Apr 14, 2026
@grunweg @pre-commit-ci-lite
chore(AtLocation): clean up backtick handling (#37999)
10b21fc 
Make errors in AtLocation surround the tactic name with backticks by default. This fixes a few error messages to comply with mathlib's style guide.

Extracted from #37899.

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 14, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(AtLocation): clean up backtick handling [Merged by Bors] - chore(AtLocation): clean up backtick handling Apr 14, 2026
@mathlib-bors mathlib-bors bot closed this Apr 14, 2026
@grunweg grunweg deleted the backticks-atlocation branch April 14, 2026 10:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@thorimur thorimur thorimur left review comments

@adomani adomani Awaiting requested review from adomani

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors. t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@grunweg @thorimur @adomani