GitHub for Mathematicians

A direct way to allow multiple people you trust to work on the same repository is to add these GitHub users as collaborators.

Collaborators are added by going to your repository’s Settings tab, using the Collaborators link in the sidebar. Each collaborator will need their own GitHub account, and must accept the invitation to collaborate before gaining access.

Once they have access, a collaborator can either use GitHub.dev (Note 2.4.2) or create their own Codespace (Definition 3.1.1).

Once a collaborator is working on a branch, they are free to edit as they wish, and can (and should) commit and push/sync with GitHub to persist their contributions to the team’s repository.

To facilitate communication among collaborators working on different branches, it’s good practice to open a draft pull request once a new branch is created.

With a draft pull request created, the contributor can continue to commit and push/sync to the branch until it is ready for review. The discussion features of GitHub can allow contributors to discuss the proposed changes, whether they are in draft or review-ready status.

Depending on the complexity or maturity of the project, you may wish to develop a review process with your collaborators, or simply use the PR workflow to clearly communicate when changes are being made to the main branch, and ensure no two collaborators make incompatible changes to the same branch. Whatever you choose, you’ll eventually want to incorporate these branched changes into your main branch.

As long as contributions are made using appropriate branches and pull requests, you will have minimal problems with conflicting changes made between different collaborators, with GitHub handling the merging process automatically, even if two collaborators edit the same file. (But not always, see Section 6.4.)

But a common error that I frequently make myself: what if you forget to create a branch with your work, and you acccidentally commit to main directly? The first safety rail I recommend is to set up a policy on your repository that will prevent this accidental commit to be pushed to GitHub.

Unfortunately, there’s no button to push that will fix a commit made to the local copy of main accidentally, but there is a quick-enough fix nonetheless.

BRANCH=my-new-branch

git stash
git branch $BRANCH
git reset --hard origin/main
git checkout $BRANCH
git stash pop

One great thing about working with open source on GitHub is that not only can you collaborate with your trusted colleagues, but you can also work with collaborators who do not have write access to your repository.

Managing contributions from forked repositories is done using the same workflow as we recommend for collaborating with trusted colleagues that you’ve given write access to your repository (Section 6.1). The only difference is that an outside collaborator is creating branches and making commits on their forked copy of your project, not a branch of your original repository. But GitHub still gives essentially the same options for the outside collaborator to create a pull request to your project, without given them access to any data you aren’t already sharing with the public.

Those of us who work in open source typically love getting pull requests from random collaborators. For example, if you find a typo in this book, you can fxi it by creating a fork at https://github.com/StevenClontz/github-for-mathematicians/fork, editing the appropriate source/*.ptx file to fix the word, and open a pull request.

Perhaps the most complicated scenario when collaborating on a Git repository is the dreaded merge conflict.

Handling merge conflicts can be tricky! Git/GitHub have various tools to help you review and correct a merge conflict. If you’re fortunate, you’ll be able to resolve things on the pull request page: see Resolving a merge conflict on GitHub

¹

docs.github.com/en/pull-requests/collaborating-with-pull-requests/addressing-merge-conflicts/resolving-a-merge-conflict-on-github

for full details.

You’ll be presented with files with some strange markers as in Listing 6.4.2. The lines between <<<<<<< HEAD and ======= were merged first, and the lines between ======= and >>>>>>> branch-a are the conflicting changes trying to be merged.

If you have questions, please
<<<<<<< HEAD
open an Issue
=======
ask them in Discussions.
>>>>>>> branch-a

You can then choose which change to retain, deleting all the extra <<<<<<< HEAD, =======, and >>>>>>> branch-a lines.

However, sometimes the merge conflict is too involved to be corrected using the web interface. In that situation, you will need to use a Codespace and follow the instructions at either Resolving a merge conflict using the command line

²

docs.github.com/en/pull-requests/collaborating-with-pull-requests/addressing-merge-conflicts/resolving-a-merge-conflict-using-the-command-line

or Using Git source control in VS Code | Merge conflicts

³

code.visualstudio.com/docs/sourcecontrol/overview#_merge-conflicts

.