-
Notifications
You must be signed in to change notification settings - Fork 133
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
Add comments about what is in scope for mathlib #526
Open
kbuzzard
wants to merge
2
commits into
lean4
Choose a base branch
from
kbuzzard-mathlib-scope
base: lean4
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
+14
−1
Open
Changes from all commits
Commits
Show all changes
2 commits
Select commit
Hold shift + click to select a range
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -10,10 +10,23 @@ to make the process of contributing as smooth as possible. | |
- The explanation of [naming conventions](naming.html). | ||
- The [documentation guidelines](doc.html). | ||
|
||
Once you have code that you'd like to contribute, you should open a PR. | ||
## What to contribute to mathlib | ||
|
||
The first question you will need to consider is whether the material you want to contribute is a good fit for `mathlib`. Whilst there is no formal description of exactly what mathlib's remit is, here are some questions which you can ask about your proposed contribution. | ||
|
||
* Is the material typically taught or studied in a mathematics department? Would it naturally be part of an undergradute or graduate course, or research level study group? If not, then the material may not be in scope for `mathlib`. | ||
* Is the topic of the material contained within the [mathematical interests of the `mathlib` maintainers](https://github.com/leanprover-community/mathlib4?tab=readme-ov-file#maintainers)? If not, then the maintainers might find your code hard to maintain as lean and `mathlib` evolve over time, which again makes it not a good fit for `mathlib`. | ||
|
||
In particular the remit of mathlib should *not* be thought of as "all of mathematics and related areas". As the number of open PRs increases, the maintainers will sometimes need to make some hard decisions. | ||
|
||
An issue related to the fact that the expertise of the maintainers may not cover all of mathematics: you may want to think about *who* is going to review your potential PR. Contributors are encouraged to seek out reviewers for their PRs. A PR reviewer does *not* have to be a maintainer! Contributions from reviewers, especially new reviewers, are essentially always welcome. | ||
|
||
If it is not completely clear to you that the code in your project is a good fit for mathlib, you might want to consider creating a standalone repository, and adding `mathlib` as a dependency. There are many Lean repositories on github, indexed by [reservoir](https://reservoir.lean-lang.org). This solution is a particularly good fit for projects in areas which do not align with the expertise of the mathlib maintainers. | ||
|
||
## Working on mathlib | ||
|
||
If you believe that your code does belong in mathlib, you should open a PR. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This sentence duplicates the first sentence in the section |
||
|
||
We use `git` to manage and version control `mathlib`. | ||
The `master` branch is the "production" version of mathlib. | ||
It is essential that everything in the master branch compiles without errors, and there are no `sorry`s. | ||
|
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Somewhere you should also say: "Discuss on Zulip whether this is a good topic to add"