Skip to content

Latest commit

 

History

History
241 lines (159 loc) · 11.7 KB

CONTRIBUTING.md

File metadata and controls

241 lines (159 loc) · 11.7 KB

Contributing guidelines

Learn how the VERSE team develops the toolchain and how you can contribute.

Start here

Before you dive in, set up your development environment to automatically enforce our style guidelines and linting rules. These avoid needless nitpicking in code reviews.

We use this GitHub project to track and coordinate development.

  • All work starts by creating an issue.
  • The issue is done when the work is done, tested, reviewed, and merged.

Read contributing code for a step-by-step guide and an explanation of why we do things this way.

Finally, read through these best practices guidelines.

Wondering if the juice is worth the squeeze? Jump to Why this process?

Setting up your development environment

We currently don't have any specific environment setup, but will add information here as we progress in the project.

Contributing code

We are following Trunk Based Development methodology. Here's the development workflow.

  1. Create an issue
  2. Create a branch
  3. Write your code
  4. Create a PR and get it reviewed
  5. Merge your PR
  6. Delete your branch

Create an issue

Create a GitHub issue describing the change you're planning to make.

  • Assign it to yourself.
  • Add a label for your organization (Galois, UCam, etc.)
  • Add labels for the type of work (IDE, CN, documentation, etc.)

If you create the issue from the repo on GitHub, there are bug and feature issue templates to guide you through the process. Creating issues from the project board unfortunately cannot use the templates.

Creating an issue automatically adds it to the project board, which helps us track and prioritize ongoing work across different teams and organizations. Tying issues to development work (and PRs) also makes it easier to answer questions in the future, like "What went into the release we sent to the user study last year?" or "What exactly did we fix from the red team's report?"

Create a branch

Create a topic branch named XX-issue-name where XX is the issue number.

Naming branches this way makes it clear which branch corresponds to which issue and makes it easier to keep the repo clear of unused or outdated branches. An easy way to create a branch following this convention is to click the "create a branch" button on the issue page and then check out the newly created branch locally.

Write your code

Here are some things to consider as you develop on your branch:

  • Structure your changes into small commits that each address a specific task. See What goes in a commit?

  • Write unit and integration tests.

  • Push regularly to your remote branch. This saves your work and runs CI tests.

When you're done...

Create a PR and get it reviewed

When you are ready to have your changes reviewed, create a PR on GitHub.

  • Summarize your change.
  • Tag one or more reviewers.
  • Link to the issue it addresses using closes/resolves/fixes #XX, where XX is the issue number.

The PR template will guide this process.

At least one reviewer needs to approve your PR. The reviewer should either:

  • Request changes for blocking/breaking issues and tricky fixes that require re-reviewing.
  • Approve for suggestions/opinions that you trust the code author to consider and address as they see fit. Approving without comments or a simple LGTM is acceptable.
  • Comment for giving early feedback on a longer review.

For example, a reviewer marks a PR as Approved even though they added a couple of comments about the PR – the author can address (or ignore) them as they see fit, and then merge without another round of reviewing.

Consider reflecting significant change requests or discussion points back into the related issue(s) as appropriate.

Merge your PR

Before merging, see What goes in a commit? for guidelines on merging your branch commit history into main. The merge should create a merge commit which helps with tracing the commits to a particular issue.

Delete your branch

GitHub usually does this for you. Consider updating your local state with

git checkout main
git pull
git branch -d your-branch-name

Git will warn you if you try to delete a branch that hasn't been merged.

VERSE-specific guidelines

  • Use language-appropriate naming conventions for naming files and folders, and default to snake_case when in doubt. The only exceptions are:
    • the top-level files, such as README.md, CONTRIBUTING and such.
    • Dockerfile* is capitalized, per Docker naming conventions
    • Makefile* is capitalized, per GNU Make naming conventions
  • Include submodules at the point of use (e.g. ./foo/bar/my_submodule), rather than in the root directory (./my_submodule).

Coding principles

  • Explicit is better than implicit
  • Code should be written to be read, and not to make writing more convenient; assume that the person reading the code is you in a year
  • Comments are critical, and should prioritize explaining why rather than what
  • Similarly, good commit messages are required; good commit messages explain why a change was made (including links to issues where appropriate or reference to observed incorrect behaviors that may inform others who see similar failures) (more on this in Git guidelines)
  • Libraries should not call exit or produce console output (unless initiating a truly mandatory crash); libraries should not have fatal crashes
  • Prefer library-first development (the functionality of any program should be available as a library)
  • A clean version control history is important (e.g., to support bisecting and code understanding), but extensive history rewriting is not important (more on this in Git guidelines)

Git guidelines

General guidelines

  • Do not commit directly to main.

  • Do not merge WIP commits that break the build (required for git bisect). If you absolutely have to do this (e.g. to save your work at the end of the day before heading out for a long vacation), consider pushing those commits to a new feature branch, and then squash the commits at the end

  • Write short, useful commit messages with a consistent style (see What goes in a commit?).

  • Keep your topic branches small to facilitate review.

  • Before merging someone else's PR, make sure other reviewers' comments are resolved, and that the author considers the PR ready to merge.

  • For security-sensitive code, ensure your changes have received an in-depth review, preferably from multiple reviewers. Please consult Code reviews page for more details.

  • Rebasing before merging is not recommended (e.g. using git pull -r to fetch remote changes), as it necessitates force pushing to the feature branch. To avoid the need to rebase, keep your feature branches small.

  • Avoid git push --force to any branches. If you must (e.g. after an unavoidable rebase), prefer git push --force-with-lease --force-if-includes. See The Dark Side of the Force Push and --force considered harmful; understanding git's --force-with-lease.

  • [Optional] Configure Git so that your commits are signed.

What goes in a commit?

Follow these seven rules for writing commit messages.

Commits should be minimal self-contained changes, reflected in the commit message. This is an art we aspire to. See this article for an in-depth discussion.

For example, consider these sets of commit messages.

  • Add logging util to capture timing
  • Add new core algorithm, disabled by default
  • Add flag to use new core algorithm

is preferable to

  • Add new core algorithm with flag to enable

is preferable to

  • First attempt at core algorithm
  • Fix logging
  • Refactor logging fix
  • Fix up algorithm
  • WIP
  • Finish alg
  • Add flag

Small commits that each address a single, self-contained issue are easy to review, easy to trace in git log, and make git bisect much more effective.

Why support git bisect?

git bisect <known-good-commit> <known-bad-commit> is a debugging utility to find which commit first introduced a bug. Using a binary search, it will iteratively check out a commit between a known-good and known-bad commit; you will then run tests to determine if the bug is present and mark the commit "good" or "bad". Eventually, it will point you to the first bad commit.

This only works if every commit is well formed. Suppose you have an example that triggers a bug, and you use git bisect to build and test each commit on that example. Consider the following series of commits.

  1. Partially implements XX (broken)
  2. Finishes implementing XX (fixed)

When git bisect checks out (1), you will be unable to build the project or determine if the bug is present.

The guidelines in What goes in a commit? support git bisect by encouraging each commit to be small and self contained.

Why this process?

We are coordinating development across a variety of teams at different organizations around the world, and the project is expected to run for several years. Despite the long duration, our timeline is tight. Hence, we need to balance several concerns:

  • Visibility. We need to understand what work has been planned, started, completed, or blocked, and who is doing it, in order to prioritize our next steps as things slip or circumstances change. We use issues and the project board for this.

  • Traceability. When code changes, we need to understand why. This sometimes lives in commit messages, PR messages, issues, or a developer's head. In this project, we're standardizing on issues, which is why all work starts with an issue. Commit messages still give context for specific changes (details here); multiple commits may support a single issue.

  • Development best practices. Software engineering research and personal experience both suggest that coherent contribution guidelines ease development while raising the level of assurance. See here for motivation and details of specific best practices, some of which are adopted in this document.

  • Developer ergonomics. Development should focus on building neat stuff, not fighting a process. We don't want to add boilerplate for no reason.