Invariants
- Each package in the project has two repositories associated with it: a public repository whose name is the name of the package (e.g.
ergm) and a private repository whose name is the name of the package suffixed by-private(e.g.,ergm-private). - The private repository mirrors the contents of the public repository and, in addition, it may have branches that are not in the public repository.
The following describes the “invariants” of the private and public repositories: the relationship between their contents that must hold at all times. If ever one is violated, it should be restored as quickly as possible.
- Any entity in the public repository must also be in the private repository. This includes commits, branches, and tags.
- The commit log of the private repository must be a superset of that of the public repository.
- Branches and tags with the same names must point to the same commits.
- The private repository may have commits, branches, etc. that the public repository does not have. These must not use names used in the public repository.
A corollary of that is that the master branches of the two repositories are always identical: it is always possible to immediately push commits in PKG@master into PKG-private@master and vice versa; and similarly for release branches.
The Statnet Janitor
The Statnet Janitor is a bot account that exists to run GitHub actions that attempt to maintain these invariants. Specifically:
- Whenever anything is pushed to the public repository, it is immediately force-pushed to the private repository with the same name.
- Whenever anything is pushed to the private repository, it if there is an object with the same name in the public repository, it is also immediately force-pushed to the public repository.
This ensures that anything in the public repository has an identical copy in the private, but not necessarily vice versa.
It is your responsibility to make sure you don’t clobber a branch you don’t intend to clobber.
FAQ for Contributing Users (i.e., those with pull access to the private repositories)
I found a bug or have a feature request. Under which repository should I create an issue ticket?
- Issues that pertain to the code both in public and in private repositories should be filed against the public repository.
- Feature requests should generally be filed against the public repository as well. Exceptions include:
- Feature requests that are specifically about some development exclusively in the private repository.
- Feature requests that involve unpublished research ideas.
Workflow for Developers
The following is mainly for those with push access to both the public and the private repository of a package and intends to operate on them directly, rather than, say, through pull requests. However, some conventions below, in particular, regarding formatting commit messages, applies in all cases.
Local setup
- Clone the private repository:
git clone git@github.com:statnet/PKG-private.git PKG
The repository will be cloned into PKG. Cloning automatically defines a remote repository, called origin, which tracks the GitHub repository. This can be verified with:
cd PKG
git remote -v
You can see all branches with:
git branch -a
- Add remotes pointing to the main public repo:
git remote add upstream git@github.com:statnet/PKG.git
Verify:
git remote -v
Updating local repository
Fetch updates:
git remote update
Pull updates:
git pull --all
Because the private repository is a superset of the public repository, this pull should not create conflicts (as long as there are no unpushed local commits).
Formulating commit messages
When referencing issues in commit messages, repository name must be specified:
Fixes statnet/PKG#314.→ public repo issueFixes statnet/PKG-private#314.→ private repo issueFixes #314.→ may have unpredictable effects
Pushing commits (private)
The following assumes that there are no conflicts with the remote branch; if there are, git fetch origin and merge and/or rebase.
Push a branch for the first time and set up tracking:
git push --set-upstream origin REFSPEC
Push all branches:
git push origin --all
Push tags:
git push origin --tags
Pushing commits (public)
Push a branch for the first time and set up tracking:
git push --set-upstream upstream REFSPEC
For existing shared branches (e.g., master), just push to upstream. It may be a good idea to fetch from both repositories, not because they may be different (as Statnet Janitor takes care of that) but because your local repository may not be aware that they are identical.
git fetch origin
git fetch upstream
git push upstream
This ensures that the two repositories remain in sync.
How should I name branches?
We use the following naming conventions.
test (public)
This branch is usually a copy of master with changes pushed to it to trigger the check GitHub actions etc. without going through the effort of creating a new branch.
dev (private)
Normally, new features should branch from master and eventually be merged back into master for public release. However, a number of unpublished changes has accumulated, and they have gone into the dev branch that can be found in some private repositories. (It is, in turn, branched from master and kept in sync with it.)
This branch is intended to be temporary and will eventually be merged into master. At this time, feature branches should only branch from dev if they absolutely require some feature in dev.
Issue-linked branches
The convention is to use i###-AAAAA, where #### is the number of the issue being addressed and AAAAA is the description.