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 AlgebraicGeometry.EllipticCurve.Weierstrass #5294

Closed
wants to merge 31 commits into from
Closed

[Merged by Bors] - feat: port AlgebraicGeometry.EllipticCurve.Weierstrass #5294

wants to merge 31 commits into from

Conversation

Multramate
Copy link
Collaborator

Open in Gitpod

xroblot and others added 17 commits June 19, 2023 14:38
@xroblot
feat: port RingTheory.Norm
bdc2c99
@xroblot
Initial file copy from mathport
cdef654
@xroblot
automated fixes
7f30d15 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@xroblot
WIP
a3af661
@xroblot
Some progress
5b313bf
@riccardobrasca
modify instance
90e9248
@riccardobrasca
better
1863946
@riccardobrasca @sgouezel
Update Mathlib/Algebra/EuclideanDomain/Instances.lean
baafcc2 
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
@xroblot
From Trace
8443f99
@xroblot
Instances mayhem
9cea04a
@xroblot
Merge remote-tracking branch 'origin/RB/change_instance' into port/Ri…
1bc6293 
…ngTheory.Norm
@xroblot
So easy now
4332258
@xroblot
comments
2a61ddd
@xroblot
Remove names
a853275
@Multramate
feat: port AlgebraicGeometry.EllipticCurve.Weierstrass
70f89a8
@Multramate
Initial file copy from mathport
bcf62b4
@Multramate
automated fixes
718828e 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@Multramate Multramate added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Jun 20, 2023
@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jun 20, 2023
@Multramate Multramate added the help-wanted The author needs attention to resolve issues label Jun 20, 2023
@semorrison semorrison removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jun 20, 2023
@ChrisHughes24
Copy link
Member

I'll tag the authors @kbuzzard and @Multramate to decide on the simp normal form. Either b₂ should not be marked simp or variableChange_b₂, or some other changes should be made.

@Multramate
Copy link
Collaborator Author

Apart from the unexpected need to increase maxHeartbeats in a new auxiliary definition quotientSpanCXSubCXSubCAlgEquiv, the only thing left is to deal with the issue in CoordinateRing, which will arise again when porting the Point dependent.

@ChrisHughes24
Copy link
Member

Apart from the unexpected need to increase maxHeartbeats in a new auxiliary definition quotientSpanCXSubCXSubCAlgEquiv, the only thing left is to deal with the issue in CoordinateRing, which will arise again when porting the Point dependent.

What is the issue in CoordinateRing?

@Multramate
Copy link
Collaborator Author

Apart from the unexpected need to increase maxHeartbeats in a new auxiliary definition quotientSpanCXSubCXSubCAlgEquiv, the only thing left is to deal with the issue in CoordinateRing, which will arise again when porting the Point dependent.

What is the issue in CoordinateRing?

It's mentioned in the comments below the porting note. Basically there's a instance unification bug in Lean 3 that made some definitions very slow, and the fix was to make CoordinateRing an irreducible definition locally. In Lean 4 I can't seem to add local attributes, and seems like I can't avoid making CoordinateRing completely reducible. It's only visible in a downstream file but it's probably good to deal with this now.

@semorrison
Copy link
Contributor

I think we don't know whether this reducibility problem is still an issue at all in lean 4, so there's no point waiting on this PR. We should just be aware we may need to revisit this file when we get to the downstream ones.

I left many comments about the porting notes. If they could be fixed up, I'm otherwise happy.

@semorrison semorrison added awaiting-author A reviewer has asked the author a question or requested changes and removed help-wanted The author needs attention to resolve issues awaiting-review The author would like community review of the PR labels Jun 27, 2023
@Multramate Multramate added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 28, 2023
@semorrison
Copy link
Contributor

bors d+

@bors
Copy link

bors bot commented Jun 28, 2023

✌️ Multramate can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated and removed awaiting-review The author would like community review of the PR labels Jun 28, 2023
@Multramate @semorrison
Update Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
83aa1d7 
Co-authored-by: Scott Morrison <scott@tqft.net>
@Multramate
Copy link
Collaborator Author

bors r+

bors bot pushed a commit that referenced this pull request Jun 28, 2023
@Multramate @xroblot
@riccardobrasca @ChrisHughes24 @mo271
feat: port AlgebraicGeometry.EllipticCurve.Weierstrass (#5294)
1ecea4a 
Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com>
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
Co-authored-by: Moritz Firsching <firsching@google.com>
@bors
Copy link

bors bot commented Jun 28, 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 AlgebraicGeometry.EllipticCurve.Weierstrass [Merged by Bors] - feat: port AlgebraicGeometry.EllipticCurve.Weierstrass Jun 28, 2023
@bors bors bot closed this Jun 28, 2023
@bors bors bot deleted the port/AlgebraicGeometry.EllipticCurve.Weierstrass branch June 28, 2023 02:21
kbuzzard pushed a commit that referenced this pull request Jul 6, 2023
@Multramate @xroblot
@riccardobrasca @ChrisHughes24 @mo271 @kbuzzard
feat: port AlgebraicGeometry.EllipticCurve.Weierstrass (#5294)
d4126d4 
Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com>
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
Co-authored-by: Moritz Firsching <firsching@google.com>
semorrison pushed a commit that referenced this pull request Aug 14, 2023
@Multramate @xroblot
@riccardobrasca @ChrisHughes24 @mo271 @semorrison
feat: port AlgebraicGeometry.EllipticCurve.Weierstrass (#5294)
a6c2854 
Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com>
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
Co-authored-by: Moritz Firsching <firsching@google.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison left review comments

Assignees
No one assigned
Labels
delegated mathlib-port This is a port of a theory file from mathlib.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@Multramate @ChrisHughes24 @semorrison @xroblot @riccardobrasca @mo271