Skip to content

Latest commit

 

History

History
277 lines (196 loc) · 9.01 KB

CONTRIBUTING.md

File metadata and controls

277 lines (196 loc) · 9.01 KB
Raw

Contributing

Thank you for your interest in contributing to Apalache!

Apalache is a symbolic model checker for TLA+.

The easiest way to contribute is to open a new issue to report a bug or a feature request. If you want to contribute to the code base, searching for "help wanted" is a good place to start. If you would like to begin working on an existing issue, please indicate so by leaving a comment. If you'd like to work on something else, open an issue to start the discussion.

The rest of this document outlines the best practices for contributing to Apalache:

Table of Contents

Decision Making

When contributing to the project, the following process leads to the best chance of landing changes:

  1. All work on the code base should be motivated by a Github Issue. The issue helps capture the problem we're trying to solve and allows for early feedback.
  2. Once the issue is created, maintainers may request more detailed documentation in the form of a Request for Comment (RFC) or Architectural Decision Record (ADR).
  3. Discussion at the RFC stage will build collective understanding of the dimensions of the problem and help structure conversations around trade-offs.
  4. When the problem is well understood but the solution leads to large structural changes to the code base, these changes should be proposed in the form of an ADR. The ADR will help build consensus on an overall strategy to ensure the code base maintains coherence in the larger context. If you are not comfortable with writing an ADR, you can open a less-formal issue and the maintainers will help you turn it into an ADR.
  5. When the problem and proposed solution are well understood, implementation can begin by opening a pull request.

Making a pull request

We develop on the unstable branch and release stable code on master.

Nontrivial changes should start with a draft pull request against unstable. The draft signals that work is underway. When the work is ready for feedback, hitting "Ready for Review" will signal to the maintainers that you are ready for them to take a look.

Where possible, implementation trajectories should aim to proceed as a series of small, logically distinct, incremental changes, in the form of small PRs that can be merged quickly. This helps manage the load for reviewers and reduces the likelihood that PRs will sit open for longer.

Each stage of the process is aimed at creating feedback cycles which align contributors and maintainers to make sure:

  • Contributors don’t waste their time implementing/proposing features which won’t land in main.
  • Maintainers have the necessary context in order to support and review contributions.

Dependencies

For setting up the local build, see the instructions on building form source.

Environment

The necessary shell environment is specified in .envrc. You can:

  • use direnv to load the environment automatically
  • source this file manually from your shell
  • or use it as a reference for what to put in your preferred rc files

Development Environment

If you use a different development environment or editor set up, please document it here!

IntelliJ IDEA

Download the community edition of IntelliJ IDEA and set up a new project.

Emacs

You can use the metals Scala language server together with lsp-mode for a nice IDE experience in the world's best lisp driven operating system.

Install metals-emacs

Arch

Using yay to install from AUR:

yay -Syu metals

Doom Emacs

Doom Emacs streamlines configuration and installation:

Edit your ~/.doom.d/init.el, to uncomment scala and configure it use lsp:

       (scala              ; java, but good
        +lsp)

Run doom sync and restart. That's it.

If you hit any snags, you might also consult this writeup

Vanilla Emacs

For installation and configuration in vanilla emacs, see https://scalameta.org/metals/docs/editors/emacs.html

Testing

Unit tests

Run the units

make test

Integration tests

Installing Dependencies

We use mdx for CLI integration tests.

Here is a platform agnostic installation recipe:

# Install opam
sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)
# Install mdx
opam install mdx

For alternative installation methods for opam, see https://opam.ocaml.org/doc/Install.html

Running the tests

To build a fresh executable and run all the integration tests, execute

make integration

For more details on running the integration tests, see ./test/tla/cli-integration-tests.md.

Continuous Integration

We run continuous integration tests using GitHub actions.

The CI configuration is located in .github/workflows/main.yml.

Changelog

Structure

./UNRELEASED.md : A living record of the changes not yet released.

./RELEASE-NOTES.md : A frozen record documenting the changes added since the last release, only present in release-commits.

./CHANGES.md : The accumulated history of all the changes, across all versions.

Recording changes

Every non-trivial PR must update the unreleased changes log.

Changes for a given release should be split between the five sections:

  1. Breaking Changes
  2. Features
  3. Improvements
  4. Bug Fixes
  5. Documentation

Releases

You must have release-me installed and configured with a token. See https://pypi.org/project/release-me/

Assuming the current version recorded in the project's .pom files is l.m.n-SNAPSHOT, the manual release process is as follows:

Prepare the release

  • git checkout unstable && git pull
  • Run ./script/release-prepare.sh to
    • create and checkout a branch release/l.m.n.
    • prepare an commit a release commit [release] l.m.n
  • Run ./script/version-bump.sh to
    • update the changelog
    • bump the version number
    • commit the changes
  • Open a PR merging the newly created branch into unstable, with the title Release l.m.n.
  • Get the PR reviewed and merged and DO NOT SQUASH THE CHANGES on merge.

If you need to set a specific version (e.g., to increment to a major version), override the RELEASE_VERSION when preparing the release:

RELEASE_VERSION=l.m.n ./script/release-prepare.sh

Cut the release

When the PR is merged into unstable: