Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

chore: changes required for leanprover/lean4#2783 #331

Closed
wants to merge 6 commits into from
Closed

chore: changes required for leanprover/lean4#2783 #331

wants to merge 6 commits into from

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented Oct 30, 2023

These are the changes required for leanprover/lean4#2783. Please review skeptically!

@kim-em kim-em added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. depends on core changes This PR need only be reviewed after changes land in Lean core. labels Oct 30, 2023
@digama0
Copy link
Member

digama0 commented Oct 30, 2023

This seems to contain more than just leanprover/lean4#2783 . Should this perhaps be a PR which targets the nightly-testing branch instead? I'm not really sure how the review process for these kind of PRs is supposed to work (or where I should push suggested changes), as they can't be merged as is to main.

@digama0
Copy link
Member

digama0 commented Oct 30, 2023

We also need to restore a bunch of @[simp] attributes on List.Basic definitions and remove the named equation theorems (or keep them but remove the @[simp] attribute). This is that big attribute [simp] block in Data.List.Init.Lemmas that had to be broken up because of the issue that leanprover/lean4#2783 fixes.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Oct 31, 2023
@kim-em kim-em added the v4.4.0 label Nov 2, 2023
@kim-em kim-em changed the base branch from main to bump/v4.4.0 November 2, 2023 01:48
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. and removed merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. labels Nov 2, 2023
@kim-em kim-em changed the base branch from bump/v4.4.0 to nightly-testing-2023-11-06 November 10, 2023 11:00
@kim-em kim-em added the merged-into-nightly-testing This has been merged into `nightly-testing`, and will join `main` when we update the toolchain. label Nov 10, 2023
@kim-em
Copy link
Collaborator Author

kim-em commented Nov 10, 2023

We also need to restore a bunch of @[simp] attributes on List.Basic definitions and remove the named equation theorems (or keep them but remove the @[simp] attribute). This is that big attribute [simp] block in Data.List.Init.Lemmas that had to be broken up because of the issue that leanprover/lean4#2783 fixes.

Could we please defer that? It seems this could be done optionally/later, and I am not keen for this to become a blocker for releasing a new version.

kim-em
kim-em commented Nov 10, 2023
View reviewed changes
Std/Classes/LawfulMonad.lean
Comment on lines +77 to +78
⟨(fun a => ⟨a, h a⟩) <$> x,
by simp (config := { unfoldPartialApp := true }) [← comp_map, Function.comp]⟩
Copy link
Collaborator Author

Choose a reason for hiding this comment

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

@digama0, in Mathlib we have the lemma Function.comp_def, and there I have used that to avoid needing unfoldPartialApp := true every time we want to unfold Function.comp.

Do you think I should move that up to Std?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Okay, I've done this in #367 now.

@kim-em
Copy link
Collaborator Author

kim-em commented Nov 10, 2023 •
edited
Loading

This seems to contain more than just leanprover/lean4#2783 . Should this perhaps be a PR which targets the nightly-testing branch instead? I'm not really sure how the review process for these kind of PRs is supposed to work (or where I should push suggested changes), as they can't be merged as is to main.

I've fixed this so it is now relative to nightly-testing-2023-11-06, i.e. the same nightly that the Lean PR was based off. It can't actually be merged as is: I think the right thing to do is just approve, and then when I do a bump PR for main that needs to include this I'll just link to this, and close after the bump PR has been merged.

@kim-em kim-em requested a review from digama0 November 10, 2023 23:22
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Nov 11, 2023
@kim-em kim-em mentioned this pull request Nov 16, 2023
Merged
@kim-em
Copy link
Collaborator Author

kim-em commented Nov 16, 2023

Closing this in favour of #367

@kim-em kim-em closed this Nov 16, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@digama0 digama0 Awaiting requested review from digama0

Assignees
No one assigned
Labels
awaiting-review This PR is ready for review; the author thinks it is ready to be merged. depends on core changes This PR need only be reviewed after changes land in Lean core. merged-into-nightly-testing This has been merged into `nightly-testing`, and will join `main` when we update the toolchain.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@kim-em @digama0 @leanprover-community-mathlib4-bot