Skip to content

perf: don't try to synthesize implicit arguments in identifiers in rw - #14593

Closed
JovanGerb wants to merge 3 commits into
leanprover:masterfrom
JovanGerb:Jovan-rw-ident
Closed

perf: don't try to synthesize implicit arguments in identifiers in rw#14593
JovanGerb wants to merge 3 commits into
leanprover:masterfrom
JovanGerb:Jovan-rw-ident

Conversation

@JovanGerb

@JovanGerb JovanGerb commented Jul 29, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

This PR is a test to see if we can save time by not trying to synthesize instance implicit arguments of identifiers in rw. Note that the same optimization already exists in apply .

Additionally, this PR tries to address the following bug in using rw for unfolding:

class A where

def Foo [A] := True

example : letI : A := {}; Foo := by
  rw [Foo] -- Failed to rewrite using equation theorems for `Foo`

@JovanGerb

JovanGerb commented Jul 29, 2026

Copy link
Copy Markdown
Contributor Author

!bench mathlib

@leanprover-radar

leanprover-radar commented Jul 29, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for leanprover-community/mathlib4-nightly-testing@c1f300f against leanprover-community/mathlib4-nightly-testing@51fd0ce are in. There are significant results. @JovanGerb

  • 🟥 main exited with code 1

No significant changes detected.

@JovanGerb JovanGerb mentioned this pull request Jul 29, 2026
Closed
@JovanGerb

JovanGerb commented Jul 29, 2026

Copy link
Copy Markdown
Contributor Author

changelog-language

Do I need this to trigger a toolchain?

@JovanGerb
JovanGerb marked this pull request as ready for review July 29, 2026 15:30
@JovanGerb
JovanGerb requested a review from kim-em as a code owner July 29, 2026 15:30
@JovanGerb

JovanGerb commented Jul 29, 2026

Copy link
Copy Markdown
Contributor Author

Does it need to be not a draft?

@github-actions github-actions Bot added the changelog-language Language features and metaprograms label Jul 29, 2026
@github-actions github-actions Bot added toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN labels Jul 29, 2026
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Jul 29, 2026
@leanprover-bot

leanprover-bot commented Jul 29, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Jul 29, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14593
a5a46c0
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 29, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14593
f5e2860
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jul 29, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14593
e8526eb
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jul 29, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Jul 29, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

@JovanGerb JovanGerb closed this Jul 29, 2026
@JovanGerb JovanGerb reopened this Jul 29, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Jul 29, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14593
2db702a
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 29, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14593
d04a843
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jul 29, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14593
f5149e9
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Jul 30, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14593
6b7d198
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 30, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14593
e87d6ba
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jul 30, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14593
8204148
@JovanGerb JovanGerb closed this Aug 10, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-manual CI has verified that the Lean Language Reference builds against this PR changelog-language Language features and metaprograms mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@JovanGerb @leanprover-radar @leanprover-bot