Skip to content

Latest commit

 

History

History
260 lines (182 loc) · 8.79 KB

CONTRIBUTING.md

File metadata and controls

260 lines (182 loc) · 8.79 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

Every non-trivial PR must update the change log.

Changes for a given release should be split between the four sections: Breaking Changes, Features, Improvements, Bug Fixes.

Releases

Assuming the version to be released is l.m.n, as per semantic versioning, the current release process is as follows:

Prepare the release

  • Update CHANGES.md, adding the heading ## l.m.n over the unreleased changes.
  • Copy this section into a new file named ./script/release-l.m.n.txt
  • Mark the version as RELEASE via mvn versions:set -DnewVersion=l.m.n-RELEASE
  • Commit the changes: git add . && git commit -m "Prepare for release l.m."
  • Open a PR to merge unstable into master, titling it Release l.m.n

Cut the release

When the PR is merged into master:

  • Checkout master
  • Sync with upstream viagit pull origin master
  • Build the artifact with make
  • Post the relese with ./script/release vl.m.n ./scripts/release-l.m.n.txt

Publish a docker image

  • Build an updated docker container: docker build -t apalache/mv:l.m.n
  • Tag the new version as latest: docker tag apalache/mc:l.m.n latest
  • Push the new taged images to dockerhub: docker push apalache/mc:l.m.n && docker push apalache/mc:latest

Advance the version on unstable

  • Checkout unstable
  • Run mvn release:update-versions
  • Commit the chnages git add . && git commit -m "Bump version to l.m.(n+1)-SNAPSHOT" && git push

Announce the relesae

  • Post a notification to the (internal) #releases slack channel.