Skip to content

Torus initial PR#1777

Open
felixpernegger wants to merge 2 commits into
mainfrom
toruspr
Open

Torus initial PR#1777
felixpernegger wants to merge 2 commits into
mainfrom
toruspr

Conversation

@felixpernegger
Copy link
Copy Markdown
Collaborator

@felixpernegger felixpernegger commented May 17, 2026

One part of #1770. (I got two likes and no comments, so why not add now)

This PR only contains trivial traits and almost completes the space already at the same time.

Funnily enough, I believe that the torus would be indistinguishable in pibase from S168 (projective plane) if it were not for p89 (fixed point property)

I set this PR partly up with claude code (telling it the traits and tell to adopt style) and it worked decently well (I fixed various stuff later, but it still definitely saved a lot of time)

This PR has low priority! (but I am not a believer in holding up making PRs for the sake of it)

@prabau
Copy link
Copy Markdown
Collaborator

prabau commented May 17, 2026

Hmm, ok. But if you have the attitude of creating PRs without waiting for existing work to be completed first, other people will start spending time creating their own PRs and not review yours anymore. :)

@felixpernegger
Copy link
Copy Markdown
Collaborator Author

Hmm, ok. But if you have the attitude of creating PRs without waiting for existing work to be completed first, other people will start spending time creating their own PRs and not review yours anymore. :)

All PRs opened by other people open right now (except #1426) require action by the author, which is partly why I added the awaiting author label.
But I see your point yeah

@felixpernegger
Copy link
Copy Markdown
Collaborator Author

@prabau I added the last sentence (This PR has low/high priority) to every of my open PRs now.
We are really having a review bottleneck, so I'll refrain from opening new PRs.

The most important one is #1775. #1725 is relatively big but I think really a good addition and #1776 good to have for the reasons I pointed out there. All the trait PRs by me are really not so important.
And #1426 is very frozen in time even though it is an important property (I'll get to it one time)

@prabau
Copy link
Copy Markdown
Collaborator

prabau commented May 17, 2026

Ok. I'll start taking a look at #1775 tomorrow.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants