Working with Pull Requests

The main difference between Gerrit changesets and GitHub pull requests is that changesets are based on single commits, while pull requests are based on branches. When considering this difference, most operations will be similar to Gerrit.

Creating a new pull request

1. Create a new branch for your pull request

   $ cd charm
   $ git branch featureX
   $ git checkout featureX
   # Edit files

2. Commit your changes to the new branch

   $ git commit

3. Push your changes

   $ git push
   # alternatively:
   $ git push origin featureX

   If you do not have write privileges to this repository, you can push the change to your fork instead:

   $ git push <forked_repo> featureX

4. Create pull request:

   https://github.com/UIUC-PPL/charm/pulls

5. After the pull request has been merged, you can delete the branch (locally and remotely):

   $ git branch -d featureX     # delete branch locally
   $ git push --delete featureX # delete it remotely; or delete in web interface
   

Updating a pull request

Commit to the same local branch and push that branch:

$ git commit
$ git push

When changing the history of a branch (e.g., by rebasing the branch, or by amending a commit that is already pushed), you might need to force-push it back to the repository (i.e, git push --force). Please use this sparingly.

Reviewing/CI

Each pull requests needs two approvals and needs to pass the Continuous Integration (CI) tests before merging.

We use Travis CI, CircleCI, and GitHub actions to test each pull request. Please see https://github.com/UIUC-PPL/charm/wiki/Continuous-integration-(CI) for more information.

Merging a pull request

We support two ways of merging a pull request: squash and merge and rebase and merge. We do not enable merge commits to keep the history simpler. These two options are available directly in the Web interface.

Squash and merge

Squash all commits into one commit and merge it to the main branch. This is the preferred option, especially for small changes, and mirrors how we used Gerrit.

Rebase and merge

Rebase all commits to top of the main branch and merge all commits. This is the preferred option for larger changes, for example, by having separate commits for the implementation of a feature and its documentation

Other possibilities (such as squashing only some commits and then merging multiple commits into master) are not directly supported by the GitHub's Web UI, but can be done manually on the command line (these might need to be force pushed to a branch).

Tools

Some tools help to simplify various aspects of working with GitHub:

Command line:

• https://hub.github.com/
• https://github.com/cli/cli

GUI

• Fork
• GitHub Desktop
• Sublime Merge