Skip to content

Commit

Permalink
strengthen encouragement to use real names on Zulip (#588)
Browse files Browse the repository at this point in the history
and slightly reorganize "working on mathlib" instructions

---------

Co-authored-by: Eric Wieser <[email protected]>
  • Loading branch information
robertylewis and eric-wieser authored Jan 29, 2025
1 parent 9d7e71b commit 2064756
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 8 deletions.
2 changes: 1 addition & 1 deletion data/community.md
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ You can browse public discussions on the most popular “channels” without reg

We welcome you to register for the Zulip chat,
which will let you participate in the discussions.
Registering with your real name is preferred, but not required.
We strongly prefer that you use your real name as your display name.
Starting by briefly introducing yourself in the
[*new members* channel](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members)
is also appreciated.
Expand Down
16 changes: 9 additions & 7 deletions templates/contribute/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -20,14 +20,16 @@ It is essential that everything in the master branch compiles without errors, an
To ensure this, we only commit changes to `master` that have passed automated Continuous Integration ("CI") tests, and have been approved by mathlib maintainers.

While you're working on a new contribution to `mathlib`, you should do this on a different branch.
It's okay to do this in your own fork of the `mathlib` repository,
or you can introduce yourself on Zulip and ask for write access to non-`master` branches of the mathlib repository,
you can either [make your own thread](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members) to introduce yourself, or ask for access in
It's okay to do this in your own fork of the `mathlib` repository.

Eventually, to make a pull request, you'll need to migrate your work to a branch of the main mathlib repository,
as our CI works better this way.
It's polite to prefix the branch name with your github username, so it's easier for us to clean up clutter.
To work in the main repository, you can introduce yourself on Zulip and ask for write access to non-`master` branches of the mathlib repository.
Either [make your own thread](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members) to introduce yourself, or ask for access in
[this topic](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/github.20permission).
Please include your GitHub username in your request (and add this username to your Zulip profile, using the personal settings panel).
It's polite to prefix the branch name with your username, so it's easier for us to clean up clutter.
(Once you're making a pull request, we'll ask you to do so from a branch of the mathlib repository,
rather than from your own fork, as CI works better this way.)
Please include your GitHub username in your request and add this username to your Zulip profile, using [the personal settings panel](https://leanprover.zulipchat.com/#settings/profile).
We also strongly encourage setting your display name on Zulip to be your real name.

Typical workflow:
* To get started, you'll need a local copy of mathlib.
Expand Down

0 comments on commit 2064756

Please sign in to comment.