-
Notifications
You must be signed in to change notification settings - Fork 93
Developer's Guide
AleksandarZeljic edited this page Jun 22, 2020
·
4 revisions
Acknowledgment: This document is adapted from CVC4 Developer guide.
Contributors to Marabou are expected to create their own fork of the Marabou repository. All changes that should be merged into master should be submitted and reviewed via pull requests. The only exception to that rule are very minor changes (e.g., typos in comments) by developers with write access which may be pushed directly onto master after all Travis builds succeeded.
- All changes to be merged should reside on a branch of your fork.
- Travis workers on the main Marabou repository are shared by everyone and
should primarily be used for testing pull requests and
master
. You get separate Travis workers for testing branches on your fork, so it is highly encouraged that you use this for your own and the team's benefit. - If you made major changes, break down your changes into small chunks and submit a pull request for each chunk in order to make reviewing less painful.
- It is recommended to not commit work in progress. You should always create pull requests for self-contained finished chunks. New features that are too big for one pull request should be split into smaller (self-contained) pull requests.
- Travis workers on the main Marabou repository are shared by everyone and
should primarily be used for testing pull requests and
- Create a pull request via GitHub and select at least one reviewer.
- one reviewer for minor changes
- two or more reviewers for everything that is not a minor change
- You need approval for your pull request from one (minor changes) or two (more than minor changes) reviewers before you can merge your pull request.
- Commits pushed to the pull request should only contain fixes and changes
related to reviewer comments.
- We require that pull requests are up-to-date with
master
before they can be merged. You can either update your branch on the GitHub page of your pull request or you can (while you are on the branch of your pull request) merge the currentmaster
usinggit pull origin master
(this creates a merge commit that can be squashed when merging the pull request) and thengit push
to update the pull request.
- We require that pull requests are up-to-date with
- Merging pull requests to master. This step can be done on the GitHub page of
your pull request.
- Merging is only possible after Travis has succeeded.
- Authors of a pull request are expected to perform the merge if they have write access to the repository (reviewers should not merge pull requests of developers that have privileges to do that themselves).
- Creating merge commits for pull requests is discouraged (we prefer a linear history) and therefore disabled via the GitHub interface.
- Squash commits are preferred over rebase commits.
- if the intermediate commits are not of general interest, do a squash commit
- In most cases, Github should automatically add the pull request number
(
#<number>
) to the title of the commit. Do not remove the number and add it if it is missing (useful for debugging/documentation purposes).
- Each
TODO
/FIXME
must link to a GitHub issue. - Recursion should be justified by a comment in the code and avoided if possible.
Unit tests test a small portion (a unit) of the code base. We use CxxTest to implement the unit tests.