JMRI Code: GitHub Administration
BackgroundJMRI uses GitHub to host our main code repository, releases and downloads and issues lists. It also hosts several related repositories.
The rest of this page records how we configure and use GitHub, along with associated procedures.
Related info on other pages:
- Continuous Integration - doesn't really talk about how GitHub is configured for this, nor how the services are configured
- Labels on Issues/PRs
- The release process works with GitHub repositories, Issues and releases.
Merging a PRJMRI's Github is configured with the following automations and requirements for merging a Pull Request:
- All required CI tests have passed for the Pull Request
- There has been at least one review from a non-author JMRI developer that accepts the Pull Request
- There are no reviews requesting changes
- The Pull Request has been in-queue for at least a day to allow people to take a look at them
- The original author of the Pull Request has been assigned to the Pull Request
- These rules apply to all members of the development team, including administrators, with the exception when CI tests do not report back correctly. In these situations, they are able to override the otherwise blocked PR but should add a note mentioning this fact. Inappropriate use of this override can be challenged by JMRI developers on the jmri-developers list.
If you want a bit more time before somebody merges a PR, either start a review saying that or set "WIP" in the title while explaining why in a comment.
When reviewing a pull request, the focus should be on function and not style. The following should be considered when reviewing a pull request:
- Does the Pull Request function as described by the author?
- Does the Pull Request add something positive to JMRI? This may include, but is not limited to:
- New features
- Fixing issues in existing code
- Improve some the development or CI process
- Unless it has previously been discussed on
and agreed to,
the PR does not take anything away or make anything more difficult.
This may include, but is not limited to:
- Removes features
- Adds to developer workload
- Is a incomplete change to structure or practice that will require future work by others
If there are any concerns about any of the above, the reviewer should either ask a question about the pull request or request changes. Significant discussions should move to the jmri-developers list to make sure people are aware of them.
When restarting CI after a failure, please copy at least a few lines around the relevant part of the log to a comment. It can be very useful to attach the entire raw log if the failure is obscure, novel or otherwise needs investigation.
When merging a PR, please do the following:
- Add any assignments beyond the original submitter. The original submitter may be assigned automatically through a github action, but if not please add them. Developers, Reviewers and Maintainers can be assigned to any PR, but other people who create PRs can only be assigned to their own. By assigning the PR, we make it easy to find what non-developers have contributed.
- Set the current milestone on the PR.
How we use GitHub teams
GitHub provides support for teams to control access to various GitHub features. We use three different ones:
- Have the "Triage" permissions, which allows editing of PRs, including adding/changing labels, releases, and other properties.
- In addition to "Triage" permissions also has "Write" permissions which allows reviewing of PRs, but are blocked from merging to the "master" branch (subject to other rules and restrictions)
- In addition to "Triage" permissions also has "Write" permissions which allows merging PRs (subject to other rules and restrictions)
Terms for adding people to developer team - still being developed
- Have to have a real name on their GitHub account?
- Have to subscribe (and stay subscribed) to jmri-developers?
- Have to have worked on something other than their own projects?