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.

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

[Merged by Bors] - doc(algebraic_hierarchy): advice for adding new typeclasses #6854

Closed
wants to merge 19 commits into from

Conversation

semorrison
Copy link
Collaborator

This is not intended as document describing all the design decisions behind our algebraic hierarchy, but rather some advice for contributors adding new typeclasses.

It can hopefully serve as a checklist for instances and definitions that should be made for any new algebraic structure being added to mathlib.

Please edit as you see fit, contribute new sections, etc. I haven't written anything yet about interactions with topology or order structures. Please consider this an invitation, or otherwise we can delete those headings later.

Thanks to @eric-wieser for providing the list of instances needed for each typeclass!


Open in Gitpod

@semorrison semorrison added the help-wanted The author needs attention to resolve issues label Mar 24, 2021
@ocfnash
Copy link
Collaborator

ocfnash commented Mar 25, 2021

This looks great, thanks for writing it.

I think it might also be helpful to include a some guidance about how to PR the work. E.g., one could:

  1. create one giant PR trying to cover all the bases, or
  2. create a series of dependent PRs trying to cover everything, or
  3. create a minimal PR and a collection of issues for the remaining points, or
  4. just PR a subset and live with the gaps, maybe return and fill some later, or
  5. something else.

Until recently, my experience has been that Mathlib has prospered with approach 4 but this may be changing.

@semorrison
Copy link
Collaborator Author

I think it might also be helpful to include a some guidance about how to PR the work. E.g., one could:

I've tried to address this in 8092aa0.

@semorrison semorrison added awaiting-review The author would like community review of the PR and removed help-wanted The author needs attention to resolve issues labels May 2, 2021
Copy link
Collaborator

@bryangingechen bryangingechen left a comment

Choose a reason for hiding this comment

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

This is great! It's not complete but it's already a great resource. We should keep working on this and keep it up to date; particularly as Lean 4 approaches.
bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels May 5, 2021
bors bot pushed a commit that referenced this pull request May 5, 2021
This is not intended as document describing all the design decisions behind our algebraic hierarchy, but rather some advice for contributors adding new typeclasses.

It can hopefully serve as a checklist for instances and definitions that should be made for any new algebraic structure being added to mathlib.

Please edit as you see fit, contribute new sections, etc. I haven't written anything yet about interactions with topology or order structures. Please consider this an invitation, or otherwise we can delete those headings later.

Thanks to @eric-wieser for providing the list of instances needed for each typeclass!



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@bors
Copy link

bors bot commented May 6, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title doc(algebraic_hierarchy): advice for adding new typeclasses [Merged by Bors] - doc(algebraic_hierarchy): advice for adding new typeclasses May 6, 2021
@bors bors bot closed this May 6, 2021
@bors bors bot deleted the hierarchy_design branch May 6, 2021 04:00
Vierkantor pushed a commit that referenced this pull request May 6, 2021
This is not intended as document describing all the design decisions behind our algebraic hierarchy, but rather some advice for contributors adding new typeclasses.

It can hopefully serve as a checklist for instances and definitions that should be made for any new algebraic structure being added to mathlib.

Please edit as you see fit, contribute new sections, etc. I haven't written anything yet about interactions with topology or order structures. Please consider this an invitation, or otherwise we can delete those headings later.

Thanks to @eric-wieser for providing the list of instances needed for each typeclass!



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

6 participants