Outdated contribution guidelines

Stream: mathlib4

[Michael Rothgang]

@Damien Thomine just pointed out to me that the [contribution guidelines] are not fully updated for the switch to forks. They indicated that this paragraph (at the very beginning) is incomplete: you also want to configure your fork somehow.

To get started, you'll need a local copy of mathlib. First, you'll need to go to https://github.com/leanprover-community/mathlib4 and click "Fork" in the top right, to make your own fork of the repository. Your fork is at https://github.com/USER/mathlib4. Now make a local clone of the repository.

[Michael Rothgang]

Looking closely, I found two more bugs on the page:

Sometimes you may not want to create a new branch, but instead work on a branch that someone else created, or you created from a different computer. In that case you need to use git switch their_new_branch (note there is no -c here).

is wrong now, it's not as simple from a fork. gh pr checkout 12345 works, as the git guide recommends.

Once you've opened a PR to the main mathlib repository (see below), continuous integration will automatically kick in at this point. You can view the output by visiting https://github.com/leanprover-community/mathlib4/tree/my_new_branch (There will be a green tick on the line describing the most recent commit if everything works, otherwise a yellow circle if CI is still working, or a red cross if something went wrong. Click on the red cross to see details.) You can also check CI status on the command line by installing hub and running hub ci-status.

is also not as simple.

I'm tempted to say that most of these should be fixed by pointing to the other page instead.

[Bryan Gin-ge Chen]

Thanks for the report! I think I was the last person to edit that file so I have some responsibility here, but unfortunately I won't have time to fix this myself in the near future. I will be happy to merge PR(s) improving the text there though!

[Johan Commelin]

Some fixes in https://github.com/leanprover-community/leanprover-community.github.io/pull/662

[Michael Rothgang]

I just gave it a look: basically, looks good to me.