Physlib

Community

Contributing via GitHub

A step-by-step guide to contributing to Physlib via GitHub, following our best practice guidlines

1. Deciding on a Problem to Work On

Creating a GitHub issue

Before starting any work, you can open an issue on the Physlib repository to describe the problem you are encountering or the feature you want to add. This makes maintainers aware of the work you plan on doing and helps with tracking the project.

  • —A clear title summarising the problem or feature.
  • —Explain the motivation for the feature.
  • —Any relevant links.
  • —A summary of the incorrect code (For bugs).
Open an Issue ↗

Asking the community

The Physlib community is full of members who can point you in the right direction if you want to discuss an idea before opening an issue. There is a Physlib channel on the Leanprover Zulip where you can post any questions you have.

Visit the Physlib Zulip ↗

2. Work on the Problem

Before writing any Lean, please read the Getting Started guide for how to install Physlib and write results in Lean according to our code quality standards.

Always create a new branch from the latest master branch before starting work. This ensures that your changes are based on the most recent version of the codebase and reduces the likelihood of merge conflicts. We recommend you use a git GUI if you are not familiar with the command line.

3. Make a Pull Request

Small pull-requests are better than large ones — even if it's just a single result. Follow the PR template provided by GitHub when opening your PR.

  1. Fork the Physlib repository to your GitHub account.
  2. Clone your forked repository to your local machine.
  3. Add the original repo as upstream: git remote add upstream https://github.com/leanprover-community/physlib.git
  4. Make your changes on a new branch (git switch -c my-branch).
  5. Push your branch to your fork.
  6. Open a pull request from your forked version to the main Physlib repository.

GitHub usually shows a banner offering to open the PR for you right after you push. If you don't see it, go to the compare page and click "compare across forks". Select your fork in the "head repository" dropdown, and the branch you want to merge in the "compare" dropdown.

Adding Labels

When opening a pull request, labels help the mainainers manage the review process. Please add comments so the bot can add labels for you. eg. commenting "awaiting-author" will add the awaiting-author label. You can view the full list of labels here.

Lifecycle of a PR

Once a reviewer looks at your PR, they will usually leave comments and add the awaiting-authorlabel. Once you have responded to the reviewer's comments and made any required changes, comment -awaiting-author to remove the label and let them know they should re-review the PR. Once they're happy, they'll mark it reviewer-approved. Then a maintainer can look at the PR and add the ready-to-merge label to add your change to the merge queue, where the final quality checks are run.

Other Common Labels

  • WIP — the PR still needs foundational work (e.g. it contains sorry) before it's ready for review. Use it to signal you're working on something you expect to finish soon.
  • help-wanted — directly soliciting contributions on an issue or PR.
  • easy— a trivial change (a single lemma, a typo fix, a diff under ~25 lines, no new definitions) that maintainers prioritise reviewing first to keep the queue moving. If you're unsure whether your PR qualifies, don't add it.
  • blocked-by-PR / blocked-by-mathlib-PR— this PR depends on another PR being merged first. Include the blocking PR's number in the title or a comment so reviewers know what to check first.
  • merge-conflict — your branch has diverged from master in a way Git can't resolve automatically. See GitHub's guide to resolving merge conflicts for how to fix it.

4. Managing the PR

After opening a PR, the maintainers will review the changes and provide feedback. Feel free to begin work on a separate PR in the meantime but be prepared to make changes to this one if required.

If you want a reviewer to be able to push fixes directly to your branch, you can grant them collaborator access via your fork's Settings → Collaborators. Once they accept, they can push to your PR branch directly.

If you get stuck at any point, the Lean Zulip is full of people who are happy to give advice.

5. Merging the PR

Once the reviewer is happy with the changes, they will merge the PR into the main branch. Physlib uses a merge queue to ensure that consecutive changes do not produce unexpected errors. This may result in your PR being rejected with errors you have not seen before.

Additional Guidance

Please use your real name in your GitHub account settings and commit author. Physlib uses GitHub account names in its automated documentation generation, so using your real name makes it easier for people to recognise your work.

If you are contributing to PhyslibAlpha, which sits downstream of Physlib, Lean code quality guidelines are less strict. However, please still follow the GitHub contribution guide.