| copyright |
|---|
Copyright (c) Runtime Verification, Inc. All Rights Reserved. |
Thank you for making a contribution to the K Framework. This document explains the steps that need to be followed to get your changes reviewed, tested and merged into K. If you have any questions about this process or K in general, please get in touch via our Discord Server or Matrix Room.
If you are using K and want to report something that doesn't work as you expect, the best way to do so is to open an issue against the K repository. Please make sure to include as much relevant information as possible in your issue to help us reproduce it. We will reply to you with any questions we have about the issue, then triage it to get fixed.
We welcome contributions to K from the community. Because running the K test suite uses our private compute resources, there are a few steps to go through to get your changes tested and merged.
For external contributors, please fork the K repository following the Github documentation. Commit any changes you make to a branch on your fork.
The first step is to develop and test your changes locally. Follow the instructions in the K README to build and test the project with your changes included. The most important tests to run are the K integration tests:
$ make -C k-distribution/tests/regression-new --jobs $(nproc) --output-syncIf your changes only apply to documentation, you can skip the testing phase.
Once you have tested your change locally, push your commits to your fork of K
and open a pull request (PR), again following the Github documentation. In
the pull request, please indicate what tests you have run locally on your
changes (e.g. "I have run the K integration tests locally"). Because this PR is
coming from an external fork, the K test suite and CI process will not run. This
is expected behaviour. Additionally, please make sure that the commit history in
your PR is clean by rebasing any messy or partial commits. Finally, it
is important that your commits are based on the K develop branch.
Next, please request a review from a K maintainer on your PR. The last person to modify the files you are changing is a good start, or if you're not sure, tag @baltoli as a fallback.
Once your code has been reviewed by a K maintainer, we will open a new PR that includes your commits with proper attribution. Doing so allows us to run our internal CI processes once we are happy with your code. If the tests pass, we will merge the PR and close your original PR. If changes need to be made subsequently to get tests to pass, they will need to be pushed to your original fork branch.
K is licensed under the BSD 3-Clause License. If you make changes to K via a pull request, your changes will automatically be licensed under the same license following Github's terms of service.
If you are an RV-internal K developer, please take ownership of any community pull requests you review, and make sure that they end up getting merged promptly following these instructions.
First, review the code in the original PR as you would normally. If you are happy with the changes made, then create a new branch of your local K repo referencing the external PR number:
$ git checkout -b adopt-pr-$NUMBERThen, add the external user's fork to your local repo as a remote:
$ git remote add temp-k-fork https://github.com/$USER/k.git
$ git fetch temp-k-forkYou can now cherry-pick the commit range in the user's PR onto your local branch:
$ git cherry-pick $START..$ENDFinally, push your branch to runtimeverification/k and open a PR as usual. CI
should run as expected, and you can request a secondary RV-internal code review
as you would for one of your own PRs. Double-check that the external user is
credited as the commit author in the Github UI.
If further changes need to be made by the external user, you can cherry-pick their changes over to your branch as before.
Once your duplicated PR is merged, you can close (not merge) the user's original PR and remove your remote pointing to their fork.
$ git remote rm temp-k-fork