Skip to content

[Merged by Bors] - feat(Tactic): add syntax for convert!, convert_to!, ac_change!#39715

Closed
Vierkantor wants to merge 2 commits into
leanprover-community:masterfrom
Vierkantor:convert-bang-alias
Closed

[Merged by Bors] - feat(Tactic): add syntax for convert!, convert_to!, ac_change!#39715
Vierkantor wants to merge 2 commits into
leanprover-community:masterfrom
Vierkantor:convert-bang-alias

Conversation

@Vierkantor

@Vierkantor Vierkantor commented May 22, 2026

Copy link
Copy Markdown
Contributor

This PR prepares for #39039 by adding the required syntax. Once this PR is in, we'll do a global find and replace for changing convert to convert! (without changing the behaviour), and finally we will enable the new behaviour for convert.

Open in Gitpod

@Vierkantor
feat(Tactic): add syntax for convert!, convert_to!, ac_change!
381a876 
This PR prepares for leanprover-community#39039 by adding the required syntax. Once this PR is in, we'll do a global find and replace for changing `convert` to `convert!` (without changing the behaviour), and finally we will enable the new behaviour for `convert`.
@Vierkantor
Vierkantor requested a review from grunweg May 22, 2026 16:24
@Vierkantor Vierkantor added the t-meta Tactics, attributes or user commands label May 22, 2026
@github-actions

github-actions Bot commented May 22, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 7111187e10

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 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.
No changes to weak technical debt.

grunweg
grunweg reviewed May 22, 2026
View reviewed changes

@grunweg grunweg left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Thanks! I have one nit (see below), which can be addressed post-merge.
bors merge

Comment thread Mathlib/Tactic/Convert.lean
@@ -173,6 +175,14 @@ example (p q : Nat → Prop) (h : ∀ ε > 0, p ε) :
syntax (name := convert) "convert" Lean.Parser.Tactic.optConfig " ←"? ppSpace term (" using " num)?
(" with" (ppSpace colGt rintroPat)*)? : tactic

@[tactic_alt convert]
syntax (name := convert!) "convert!" Lean.Parser.Tactic.optConfig " ←"? ppSpace term

@grunweg grunweg May 22, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Is there a reason you went from Parser.Tactic.optConfig to Lean.Parser.Tactic.optConfig?

In any case, this can be an easy follow-up PR which I would insta-merge --- so let me record this for us to discuss later tonight.

@mathlib-triage mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 22, 2026
@grunweg grunweg mentioned this pull request May 22, 2026
Open
3 tasks
mathlib-bors Bot pushed a commit that referenced this pull request May 22, 2026
@Vierkantor
feat(Tactic): add syntax for convert!, convert_to!, ac_change! (#…
898167a 
…39715)

This PR prepares for #39039 by adding the required syntax. Once this PR is in, we'll do a global find and replace for changing `convert` to `convert!` (without changing the behaviour), and finally we will enable the new behaviour for `convert`.

Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
@mathlib-bors

mathlib-bors Bot commented May 22, 2026

Copy link
Copy Markdown
Contributor

Build failed (retrying...):

mathlib-bors Bot pushed a commit that referenced this pull request May 22, 2026
@Vierkantor
feat(Tactic): add syntax for convert!, convert_to!, ac_change! (#…
43ed5bb 
…39715)

This PR prepares for #39039 by adding the required syntax. Once this PR is in, we'll do a global find and replace for changing `convert` to `convert!` (without changing the behaviour), and finally we will enable the new behaviour for `convert`.

Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
@mathlib-bors

mathlib-bors Bot commented May 22, 2026

Copy link
Copy Markdown
Contributor

Build failed:

Fix if necessary, and then someone with permission can run bors r+ or bors retry.

grunweg
grunweg reviewed May 22, 2026
View reviewed changes
Comment thread Mathlib/Tactic/Convert.lean
@@ -274,8 +296,13 @@ example (a b c d e f g N : ℕ) : (a + b) + (c + d) + (e + f) + g ≤ N := by
```
-/
syntax (name := acChange) "ac_change " term (" using " num)? : tactic
syntax (name := acChange!) "ac_change! " term (" using " num)? : tactic

@grunweg grunweg May 22, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

The docBlame linter complains about this one. Probably just a missing inherit_doc or tactic_alt.

@grunweg

grunweg commented May 22, 2026

Copy link
Copy Markdown
Contributor

bors d+

@mathlib-bors

mathlib-bors Bot commented May 22, 2026

Copy link
Copy Markdown
Contributor

✌️ Vierkantor 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 the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label May 22, 2026
@Vierkantor

Vierkantor commented May 22, 2026

Copy link
Copy Markdown
Contributor Author

Let's just bors this, so we don't have to wait.

bors r+

mathlib-bors Bot pushed a commit that referenced this pull request May 22, 2026
@Vierkantor
feat(Tactic): add syntax for convert!, convert_to!, ac_change! (#…
860f946 
…39715)

This PR prepares for #39039 by adding the required syntax. Once this PR is in, we'll do a global find and replace for changing `convert` to `convert!` (without changing the behaviour), and finally we will enable the new behaviour for `convert`.

Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
@grunweg grunweg mentioned this pull request May 22, 2026
Closed
1 task
@mathlib-bors

mathlib-bors Bot commented May 22, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title feat(Tactic): add syntax for convert!, convert_to!, ac_change! [Merged by Bors] - feat(Tactic): add syntax for convert!, convert_to!, ac_change! May 22, 2026
@mathlib-bors mathlib-bors Bot closed this May 22, 2026
RaggedR pushed a commit to RaggedR/mathlib4 that referenced this pull request May 24, 2026
@Vierkantor @RaggedR
feat(Tactic): add syntax for convert!, convert_to!, ac_change! (l…
b86af76 
…eanprover-community#39715)

This PR prepares for leanprover-community#39039 by adding the required syntax. Once this PR is in, we'll do a global find and replace for changing `convert` to `convert!` (without changing the behaviour), and finally we will enable the new behaviour for `convert`.

Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026
@Vierkantor @b-mehta
feat(Tactic): add syntax for convert!, convert_to!, ac_change! (l…
ebfd650 
…eanprover-community#39715)

This PR prepares for leanprover-community#39039 by adding the required syntax. Once this PR is in, we'll do a global find and replace for changing `convert` to `convert!` (without changing the behaviour), and finally we will enable the new behaviour for `convert`.

Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
@Vierkantor @Bergschaf
feat(Tactic): add syntax for convert!, convert_to!, ac_change! (l…
6cfe45a 
…eanprover-community#39715)

This PR prepares for leanprover-community#39039 by adding the required syntax. Once this PR is in, we'll do a global find and replace for changing `convert` to `convert!` (without changing the behaviour), and finally we will enable the new behaviour for `convert`.

Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@grunweg grunweg grunweg left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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.

2 participants

@Vierkantor @grunweg