Reporting Problems with TARDIS

How-To Guide: Report Issues

TARDIS is under constant development, so bugs, inconsistencies, and missing functionality can occur. File issues on the official GitHub repository:

https://github.com/tardis-sn/tardis

Interested users are encouraged to contribute to TARDIS development by following the development workflow.

Pull Requests

How-To Guide: Open a Pull Request

When you are ready for review or merge consideration:

  1. Go to your fork, for example https://github.com/your-user-name/tardis.

  2. Use the branch dropdown to select the branch with your changes.

  3. Click the pull request button.

  4. Enter a title and an explanation of what you have done.

  5. Include anything that needs particular attention, such as a complicated change or code you are unsure about.

  6. If the request is not ready to merge, say so in the pull request message and set the pull request to Draft using the drop-down menu. Opening an unfinished pull request can still be a good way to start a preliminary code review.

  7. Build documentation for the pull request using the documentation preview process so reviewers can see how notebooks, docstrings, and API docs render.

Example pull request description:

How-To Guide: Review Pull Requests

GitHub supports line comments and discussion threads on pull requests. Sometimes it is easier to demonstrate a suggested change by making a pull request on a pull request.

Add pull request refs to the upstream remote in .git/config:

[remote "upstream"]
    url = git@github.com:tardis-sn/tardis.git
    fetch = +refs/heads/*:refs/remotes/upstream/*
    fetch = +refs/pull/*/head:refs/remotes/upstream/pr/*

Fetch upstream:

git fetch upstream

You can then check out a pull request branch, for example pull request 116:

git checkout upstream/pr/116

This leaves you in a detached HEAD state. Create a branch for your changes:

git checkout -b helping-with-PR116

After making and committing your changes, push them to your fork:

git push origin helping-with-PR116

How-To Guide: Update a Pull Request

Pull requests often remain open while feedback is added and other pull requests are merged. If changes on trunk affect your work, merge the trunk into your feature branch.

Fetch trunk and switch to your branch:

git fetch upstream
git checkout cool-feature

Merge upstream trunk into your feature branch:

git merge upstream/master

Resolve any merge conflicts and commit the changes.

If the feature branch is already on GitHub, push after merging:

git push origin cool-feature