Version Control

Vampire uses the git VCS. All changes are made by authorised persons merging branches from others into master after review. master should always build and be generally sane, but may not be a stable release.

Try and keep pull requests short and making exactly one change. This makes it easier for review, to avoid breaking things, and makes your life easier as master is less likely to change significantly underneath you. Many seemingly-large changes can be broken down into smaller steps! However, there are occasions which justify long-lived branches.

To make a change, start by making a personal branch. Call it something related to the feature, but also prepend your name to avoid clashes. For example, michael-static-assert removed the old static assertion mechanism in favour of C++11's static_assert. You can then make commits to this branch and create a PR on GitHub when the work in the branch is ready for review.

Commits can be kept tidy by occasionally rewriting history, provided nobody is using your branch. If you have pushed commits to remote and want to rewrite them, you can carefully use git push --force-with-lease to push the rewritten commits while not accidentally breaking other people's work.

If master changes under you in such a way that you want to reconcile the two (e.g. before a PR), you have two options:

1. git rebase rewrites history, roughly pretending that you made changes starting from a later point in the parent branch. This keeps commit history neat and is the preferred option if nobody is currently using your branch and if a rebase is feasible.
2. Otherwise, merging master into your branch is OK as well and can be easier for large changes.

On Merge Commits

Please, oh please, use "git pull --rebase" This can be even configured globally. To explain: While it is fine to have merge-commits as a documentation for where a long-lived feature branch joined master (or where a long lived feature branch had to be synced with master by mergeing with it), "git pull --rebase" prevents you from creating a useless merge commit on pulling a branch that your colleague recently modified. (This can happen, for instance, when someone reviewing your pull request fixes a tiny bug, while you were in the meantime fixing another.)