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

[Merged by Bors] - feat: port RingTheory.Polynomial.Hermite.Basic #3967

Closed
wants to merge 23 commits into from
Closed

[Merged by Bors] - feat: port RingTheory.Polynomial.Hermite.Basic #3967

wants to merge 23 commits into from

Conversation

EmilieUthaiwat
Copy link
Collaborator

Open in Gitpod

@EmilieUthaiwat EmilieUthaiwat added mathlib-port This is a port of a theory file from mathlib. WIP Work in progress labels May 14, 2023
@EmilieUthaiwat EmilieUthaiwat marked this pull request as ready for review May 14, 2023 13:32
@EmilieUthaiwat EmilieUthaiwat added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels May 14, 2023
kbuzzard
kbuzzard reviewed May 14, 2023
View reviewed changes
Copy link
Member

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

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

Thanks a lot! I've left some suggestions. Please choose how to deal with them, resolve the conversations and change the tag back to awaiting-review.

Mathlib/RingTheory/Polynomial/Hermite/Basic.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/Polynomial/Hermite/Basic.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/Polynomial/Hermite/Basic.lean Outdated Show resolved Hide resolved
@kbuzzard kbuzzard added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels May 14, 2023
@eric-wieser eric-wieser mentioned this pull request May 14, 2023
Closed
eric-wieser
eric-wieser requested changes May 14, 2023
View reviewed changes
Copy link
Member

@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.

The port dashboard says that you should ping @lukemantle before porting this file, as they are maybe still working on this in mathlib3. Did you do so?

@eric-wieser
Copy link
Member

(I now see that due to an error in the dashboard page this message was unfortunately not visible)

@EmilieUthaiwat
Copy link
Collaborator Author

Yes, there is no comment on the port status page I see so I did not know I had to ping @lukemantle. I apologize for this.

@eric-wieser
Copy link
Member

No worries, this is certainly not your fault. The mistake was caused by a file rename in mathlib3 without updating the corresponding name on the dashboard

@EmilieUthaiwat EmilieUthaiwat removed the awaiting-author A reviewer has asked the author a question or requested changes label May 14, 2023
@jakelev
Copy link
Collaborator

jakelev commented May 14, 2023 •
edited

Hey, thanks for porting this! @lukemantle was my student and I can say that he's not working actively on the project any more; I have taken over with merging his PRs into mathlib3. That said, there's still one last PR to do (the explicit formula for the coefficient of a Hermite polynomial) which is currently waiting on #18994. Can this PR perhaps wait til that #18994 and the followup PR are done?

I could also put the new code into a new file when I PR it, which would mean it wouldn't require further edits to the work you've done here.

@kbuzzard
Copy link
Member

Oh thanks for spotting this Eric! When I was reviewing the PR I only compared the diff with the output of mathlib3port so I also missed this message.

@eric-wieser
Copy link
Member

@EmilieUthaiwat, to confirm your work is not wasted. We can leave this PR open, and git will be able to merge in any subsequent changes.

I can take care of this when @jakelev's work is done.

@eric-wieser eric-wieser added the WIP Work in progress label May 14, 2023
@EmilieUthaiwat
Copy link
Collaborator Author

@jakelev I am of course fine with waiting until #18994 and the followup PR are done before switching back to the awaiting-review tag.

Personally, I do not mind doing further edits to this PR if it makes more sense to add the new code to this file. Should it not make much difference where the new code is, then I also think it would be better to create a separate file.

@EmilieUthaiwat
Copy link
Collaborator Author

@eric-wieser Thank you!

@jakelev jakelev mentioned this pull request May 19, 2023
Closed
@jakelev
Copy link
Collaborator

jakelev commented May 19, 2023

@EmilieUthaiwat @eric-wieser The last PR is ready #19044.

@EmilieUthaiwat
Copy link
Collaborator Author

The PR https://github.com/leanprover-community/mathlib/pull/19044 has been merged into mathlib3. Could someone please tell me what I should do to port the merged changes?

@eric-wieser eric-wieser force-pushed the port/RingTheory.Polynomial.Hermite.Basic branch from 82886cb to 7599358 Compare June 9, 2023 15:01
@eric-wieser
Copy link
Member

I just rebased

@EmilieUthaiwat
Copy link
Collaborator Author

Thank you for having rebased! I finished fixing the file.

@EmilieUthaiwat EmilieUthaiwat added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Jun 10, 2023
jcommelin
jcommelin approved these changes Jun 13, 2023
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@semorrison semorrison added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Jun 13, 2023
bors bot pushed a commit that referenced this pull request Jun 13, 2023
@eric-wieser @EmilieUthaiwat
feat: port RingTheory.Polynomial.Hermite.Basic (#3967)
765d910 
Co-authored-by: Emilie Uthaiwat <emiliepathum@gmail.com>
Co-authored-by: EmilieUthaiwat <102412311+EmilieUthaiwat@users.noreply.github.com>
@bors
Copy link

bors bot commented Jun 13, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: port RingTheory.Polynomial.Hermite.Basic [Merged by Bors] - feat: port RingTheory.Polynomial.Hermite.Basic Jun 13, 2023
@bors bors bot closed this Jun 13, 2023
@bors bors bot deleted the port/RingTheory.Polynomial.Hermite.Basic branch June 13, 2023 07:01
alexkeizer pushed a commit that referenced this pull request Jun 22, 2023
@eric-wieser @EmilieUthaiwat @alexkeizer
feat: port RingTheory.Polynomial.Hermite.Basic (#3967)
b228013 
Co-authored-by: Emilie Uthaiwat <emiliepathum@gmail.com>
Co-authored-by: EmilieUthaiwat <102412311+EmilieUthaiwat@users.noreply.github.com>
semorrison pushed a commit that referenced this pull request Jun 25, 2023
@eric-wieser @EmilieUthaiwat @semorrison
feat: port RingTheory.Polynomial.Hermite.Basic (#3967)
c40dcc7 
Co-authored-by: Emilie Uthaiwat <emiliepathum@gmail.com>
Co-authored-by: EmilieUthaiwat <102412311+EmilieUthaiwat@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kbuzzard kbuzzard kbuzzard left review comments

@eric-wieser eric-wieser eric-wieser requested changes

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@EmilieUthaiwat @eric-wieser @jakelev @kbuzzard @jcommelin @semorrison