Skip to content

Git And Pull Request Workflow

This guide is for contributors working on the project through GitHub pull requests.

Each contributor should clone the repo on the machine where they will work, set up the relevant container environment, do new work on a branch, and submit a pull request when the work is ready for review.

1. Clone The Repo

Using SSH keys for GitHub access is recommended. See GitHub's guide to connecting to GitHub with SSH.

Clone the repository on either your local machine or the lab server:

git clone git@github.com:milonemario/hct-tower.git
cd hct-tower

Note: when working on the lab server, clone the repo in your home directory, not in a shared folder.

Then set up the runtime environment for that machine:

2. Start New Work From main

Keep main as the clean shared baseline. Do not commit directly to main.

Before starting new work:

git checkout main
git pull origin main

Create a new branch for the task:

git checkout -b feature/short-description

Use lowercase, hyphen-separated branch names. Prefer this format:

type/short-description

Recommended branch types:

  • feature/: new project functionality
  • fix/: bug fixes
  • docs/: documentation-only changes
  • analysis/: empirical analysis work
  • model/: model training, evaluation, or scoring changes
  • data/: data-building or data-contract changes
  • infra/: containers, Slurm, dependencies, or tooling

Examples:

  • docs/container-guides
  • model/eval-metrics-slices
  • analysis/main-results-table
  • infra/slurm-submit-defaults

If there is a GitHub issue number, include it near the front:

feature/123-short-description

3. If You Accidentally Work On main

This is common and fixable. If you started work on local main by mistake, move the work to a new branch before pushing.

If the changes are not committed yet:

git status
git checkout -b feature/short-description
git add path/to/changed-file
git commit -m "type: brief description"
git push -u origin feature/short-description

If the changes were already committed on local main, create a branch at the current commit:

git status
git checkout -b feature/short-description
git push -u origin feature/short-description

Then return local main to the shared GitHub version:

git checkout main
git fetch origin
git reset --hard origin/main

After this, the new branch contains the work and local main is clean again. If commits were already pushed directly to main, pause and ask a project maintainer before trying to undo them. Note that the main barnch is protected on github to avoid direct pushes so this should not happen.

4. Commit And Push During Development

Commit focused chunks of work as you go:

git status
git add path/to/changed-file
git commit -m "docs: clarify local container setup"

Commit messages should be short and action-oriented. A useful pattern is:

type: brief description

Examples:

  • docs: add local container guide
  • model: export observed match scores
  • analysis: add main results scaffold
  • infra: update slurm submission wrapper

Push your branch to GitHub:

git push -u origin feature/short-description

After the first push, later pushes can use:

git push

It is fine to push work-in-progress commits to your own branch. Avoid force-pushing shared branches. If you need to clean up your own branch history, use git push --force-with-lease, not plain --force.

5. Keep Your Branch Up To Date

If main changes while you are working, update your branch before opening or finalizing a pull request:

git checkout main
git pull origin main
git checkout feature/short-description
git merge main

Resolve conflicts locally, run the relevant checks, then commit and push the merge result.

6. Open A Pull Request

When the work is ready for review, open a pull request from your branch into main.

The pull request should include:

  • what changed
  • why it changed
  • how to test or reproduce the result
  • any known limitations or follow-up work

Keep pull requests focused. If a branch starts mixing unrelated work, split it into separate branches and pull requests.

A project maintainer reviews the pull request and merges it into main when it is ready. There may be more than one project maintainer. Do not merge your own pull request unless a project maintainer has explicitly asked you to do so.

7. After The Pull Request Is Merged

Return to main, update it, and delete the local branch if you no longer need it:

git checkout main
git pull origin main
git branch -d feature/short-description

You can also delete the remote branch after merge:

git push origin --delete feature/short-description

Then start the next task from the updated main.