Skip to content

Commit

Permalink
Add comments about what to contribute to mathlib
Browse files Browse the repository at this point in the history
  • Loading branch information
kbuzzard committed Sep 18, 2024
1 parent cc33737 commit d443615
Showing 1 changed file with 12 additions and 1 deletion.
13 changes: 12 additions & 1 deletion templates/contribute/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,21 @@ 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 covered in an undergraduate or graduate level course in a research mathematics department? If not, then the material may not 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.

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.

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.
Expand Down

0 comments on commit d443615

Please sign in to comment.