Skip to content

Developer's Guide

Jump to bottom
AleksandarZeljic edited this page Jul 1, 2019 · 4 revisions

Contributing to Marabou

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.

Pull Requests

  1. 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.
  2. 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
  3. 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.
  4. 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 current master using git pull origin master (this creates a merge commit that can be squashed when merging the pull request) and then git push to update the pull request.
  5. 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).

Coding Style Guidelines

  • Each TODO/FIXME must link to a GitHub issue.
  • Traversing expressions must not be done recursively if the data structure can be deeply nested. Recursion should be justified by a comment in the code and avoided if possible.

TODO: add more

Formatting with clang-format

To set-up the git clang-format plugin, follow these steps:

  • Download the git-clang-format script from here
  • Make it executable (chmod +x git-clang-format)
  • Put it somewhere in your path
  • Check that git clang-format -h works (notice there's no dash after git)

Before committing, you can run:

git add --update         # Stage your changes
git clang-format HEAD    # Format the changed lines

If you want to format changes from multiple commits, e.g. the last ten commits, do:

git clang-format HEAD~10 # Format the changes in the last ten commits

For (neo)vim there is the vim-clang-format plugin for formatting files and blocks of code. For emacs there is the analogous clang-format.el.

Clang-format uses a configuration file that describes the formatting style. Make sure that you use the .clang-format file in the Marabou repository (this should happen automatically with git clang-format).

Checking the Code Coverage of Unit/System/Regression Tests

TODO:

Communicating with the User

TODO: Do we have/want equivalent features? TODO: Update examples All output should go through Debug, Warning, Notice, Chat, and Trace.

Examples:

#include "util/output.h"
Marabou::Debug("arith") << "foo!";                                                      // prints "foo!" if arith debugging is on
Marabou::Warning() << "Equivalence classes didn't get merged.";                         // prints unless user gave -q or in SMT-COMP mode
Marabou::Notice() << "Hi, so you don't get bored, here are some statistics: " << stats; // if user gives -v
Marabou::Chat() << "I feel like doing some theory propagation.";                        // if user gives -vv
Marabou::Trace("arith") << "<ralph>I'm now calling a function!</ralph>";                // if user gives -vvv

For non-debug/tracing builds, Marabou::Debug/Trace are a no-op respectively and everything will be inlined away.

Assertions

TODO: Update after new assertions have been implemented.

Testing

In this section, we explain the three different types of tests we do in Marabou: regression tests, unit tests and system tests.

Regression Tests

Regression tests consist of input files with expected outcomes, so they perform end-to-end testing.

Unit Tests

TODO: Do we use this already? Unit tests test a small portion (a unit) of the code base. We use CxxTest to implement the unit tests. To run the unit tests, CxxTest needs to be installed on the machine.

TODO: Explain details

System Tests

TODO: Explain details

Clone this wiki locally