Skip to content

feat: use supplied structure fields left to right and eta reduce terms in structure instance elaboration#2478

Merged
kim-em merged 2 commits intoleanprover:masterfrom
mattrobball:reduce_etas
Feb 1, 2024
Merged

feat: use supplied structure fields left to right and eta reduce terms in structure instance elaboration#2478
kim-em merged 2 commits intoleanprover:masterfrom
mattrobball:reduce_etas

Conversation

@mattrobball
Copy link
Copy Markdown
Contributor

@mattrobball mattrobball commented Aug 29, 2023 •
edited
Loading

Modifies the structure instance elaborator to

  1. Fill in missing fields from sources in strict left-to-right order. In {a, b with}, sometimes the elaborator
    would ignore a even if both a and b provided the same field, depending on what subobject fields they had.
  2. Use the sources, or subobjects of the sources, to fill in entire subobjects of the target structure as much as possible.
    Currently, a field cannot be filled directly by a source itself resulting in the term being eta expanded.
    This change avoids this unnecessary and surprisingly costly extra eta expansion.

Adds two new tests to illustrate the performance benefit (one courtesy @semorrison). These are currently failing on master and succeed on this branch.

There is one additional test to exercise the changes to the elaboration of structure instances.

Changes to make mathlib build are in leanprover-community/mathlib4#9843

Closes #2451

@github-actions
Copy link
Copy Markdown
Contributor

github-actions bot commented Aug 29, 2023

Thanks for your contribution! Please make sure to follow our Commit Convention.

@mattrobball mattrobball changed the title Tweak structure instance elaboration to eliminate un-needed eta expansions of terms feat: modify structure instance elaboration to eliminate un-needed eta expansions of terms Aug 29, 2023
@mattrobball
Copy link
Copy Markdown
Contributor Author

mattrobball commented Aug 30, 2023

awaiting-review

@github-actions github-actions bot added the awaiting-review Waiting for someone to review the PR label Aug 30, 2023
kim-em
kim-em reviewed Aug 30, 2023
View reviewed changes
kim-em
kim-em reviewed Aug 30, 2023
View reviewed changes
kim-em
kim-em reviewed Aug 30, 2023
View reviewed changes
kim-em
kim-em reviewed Aug 30, 2023
View reviewed changes
kim-em
kim-em reviewed Aug 30, 2023
View reviewed changes
kim-em
kim-em reviewed Aug 30, 2023
View reviewed changes
kim-em
kim-em reviewed Aug 30, 2023
View reviewed changes
kim-em
kim-em reviewed Aug 30, 2023
View reviewed changes
kim-em
kim-em reviewed Aug 30, 2023
View reviewed changes
@kim-em
Copy link
Copy Markdown
Collaborator

kim-em commented Aug 30, 2023

awaiting-author

@github-actions github-actions bot added awaiting-author Waiting for PR author to address issues and removed awaiting-review Waiting for someone to review the PR labels Aug 30, 2023
@mattrobball
Copy link
Copy Markdown
Contributor Author

mattrobball commented Aug 30, 2023

Thanks for the comments. Hopefully, they are addressed with these changes.

awaiting-review

@github-actions github-actions bot added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Aug 30, 2023
@mattrobball
Copy link
Copy Markdown
Contributor Author

mattrobball commented Aug 30, 2023

awaiting-author

@github-actions github-actions bot added awaiting-author Waiting for PR author to address issues and removed awaiting-review Waiting for someone to review the PR labels Aug 30, 2023
@mattrobball
Copy link
Copy Markdown
Contributor Author

mattrobball commented Aug 30, 2023

awaiting-review

@github-actions github-actions bot added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Aug 30, 2023
kim-em
kim-em reviewed Aug 31, 2023
View reviewed changes
kim-em
kim-em reviewed Aug 31, 2023
View reviewed changes
@kim-em
Copy link
Copy Markdown
Collaborator

kim-em commented Aug 31, 2023

Can you please rebase on master so we get a mathlib-compatible release to try out?

@digama0 digama0 mentioned this pull request Nov 7, 2023
Open
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 8, 2023
Trigger CI for leanprover/lean4#2478
31cec75
@ghost ghost added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-mathlib CI has verified that Mathlib builds against this PR and removed builds-mathlib CI has verified that Mathlib builds against this PR breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Nov 8, 2023
@Kha Kha requested review from Kha and leodemoura as code owners November 20, 2023 08:15
@mattrobball mattrobball requested a review from tydeu as a code owner December 11, 2023 17:45
@tydeu
Copy link
Copy Markdown
Member

tydeu commented Dec 11, 2023

@mattrobball You appear to have accidently committed src/lake/lakefile.olean to this branch.

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 11, 2023
Trigger CI for leanprover/lean4#2478
f6d20ab
@kim-em
Copy link
Copy Markdown
Collaborator

kim-em commented Dec 12, 2023

There's no associated mathlib PR for this at the moment, right?

@mattrobball mattrobball mentioned this pull request Dec 12, 2023
Closed
eric-wieser
eric-wieser reviewed Dec 20, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Dec 20, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Dec 21, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Dec 21, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Dec 21, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Dec 21, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Jan 15, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

Whoops, I never submitted these suggestions:

@mattrobball
Copy link
Copy Markdown
Contributor Author

mattrobball commented Jan 16, 2024

awaiting-review

@Vierkantor Vierkantor mentioned this pull request Jan 16, 2024
Closed
2 tasks
@eric-wieser eric-wieser mentioned this pull request Jan 19, 2024
Closed
@kbuzzard
Copy link
Copy Markdown
Contributor

kbuzzard commented Jan 19, 2024

Note the substantial speedup to mathlib which comes with this PR.

@mattrobball mattrobball mentioned this pull request Jan 23, 2024
Closed
kmill
kmill approved these changes Jan 31, 2024
View reviewed changes
Copy link
Copy Markdown
Collaborator

@kmill kmill left a comment

Choose a reason for hiding this comment

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

Thanks for all the work getting this to this point! I'm looking forward to seeing this merged.

It looks good to me. I see it's not rebased onto the most current nightly, so please do that to be sure the CI goes through.

tests/lean/run/463.lean Outdated

def foo (s : C) : B := {s with} -- works in lean 4, works in lean 3
def bar (s : D) : B := {s with} -- works in lean 4, fails in lean 3
-- def bar (s : D) : B := {s with} -- works in lean 4, fails in lean 3
Copy link
Copy Markdown
Collaborator

@kmill kmill Jan 31, 2024

Choose a reason for hiding this comment

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

Correct me if I'm wrong, you don't need to comment this out, right?

You can add a comment that this is not necessarily meant to succeed.

Copy link
Copy Markdown
Contributor Author

@mattrobball mattrobball Jan 31, 2024

Choose a reason for hiding this comment

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

Doesn’t it fail a test because this errors?

Copy link
Copy Markdown
Contributor Author

@mattrobball mattrobball Jan 31, 2024

Choose a reason for hiding this comment

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

Added a comment referencing the PR number

@kim-em kim-em mentioned this pull request Feb 1, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

@kmill kmill kmill approved these changes

@leodemoura leodemoura Awaiting requested review from leodemoura

@Kha Kha Awaiting requested review from Kha

@tydeu tydeu Awaiting requested review from tydeu

+1 more reviewer

@eric-wieser eric-wieser eric-wieser approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@kmill kmill

Labels

awaiting-review Waiting for someone to review the PR builds-mathlib CI has verified that Mathlib builds against this PR Mathlib4 high prio Mathlib4 high priority issue 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.

RFC: tweak structure instance elaboration to avoid un-needed eta expansion

8 participants

@mattrobball @kim-em @leodemoura @tydeu @kbuzzard @kmill @eric-wieser @digama0