From 5e2674d33aa456291156febb335cbb234c501b8c Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 5 Mar 2026 06:06:41 +0000 Subject: [PATCH 1/7] Create ReviewGuidelines.md --- docs/ReviewGuidelines.md | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 docs/ReviewGuidelines.md diff --git a/docs/ReviewGuidelines.md b/docs/ReviewGuidelines.md new file mode 100644 index 000000000..2451f114d --- /dev/null +++ b/docs/ReviewGuidelines.md @@ -0,0 +1,34 @@ +# Review guidelines + +Below we give guidelines to what reviews of pull-requests to PhysLib are looking for. +This list is not exhaustive and reviews are within the judgement of the reviewer. + +## Code quality + +- Correct abstraction of lemmas and definitions. +- Correct use of type theory in definitions. +- Correct use of lemmas from Mathlib, e.g. not reproving things which are already proved. +- Concise proofs where possible. + +In another programming language these points analogous to not just making sure you +have a function that does the right thing, but making sure that that function is +as efficient as possible, uses the best algorithm available etc. + +## Organization + +- Lemmas and definitions appear in the correct place +- Modules are easy to read and have a well-defined scope +- Any new correct files are suitably named. +- Any new correct files are suitably located. +- Modules have sufficent documentation to understand there flow. + +These points are about readability of the project as a whole and how easy it is to find results within the project. + +## Style conventions + +- Use less-then rather than greater-then. +- No new lines in proofs. +- Good use of `variables`. + +These points are related to how individual lemmas and theorems look, and how easy they are +to read. From 6b8150340d626e6e501c6492c1b2be81d1c28a12 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 5 Mar 2026 06:11:25 +0000 Subject: [PATCH 2/7] Update ReviewGuidelines.md --- docs/ReviewGuidelines.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/docs/ReviewGuidelines.md b/docs/ReviewGuidelines.md index 2451f114d..ba6b8b9a7 100644 --- a/docs/ReviewGuidelines.md +++ b/docs/ReviewGuidelines.md @@ -32,3 +32,11 @@ These points are about readability of the project as a whole and how easy it is These points are related to how individual lemmas and theorems look, and how easy they are to read. + +## PR and authorship + +- The author of the PR understands the material in the PR. +- The PR is concise and adds a single new concept (which may be multiple lemmas or definitions) + +These points are not to the code-base itself but the history of the project and how +easy it is for someone to find information on a given area from the git history. From e1fdc5316483622766d80760bebaa65665f4e774 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 5 Mar 2026 06:11:55 +0000 Subject: [PATCH 3/7] Update ReviewGuidelines.md --- docs/ReviewGuidelines.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/ReviewGuidelines.md b/docs/ReviewGuidelines.md index ba6b8b9a7..739515f9a 100644 --- a/docs/ReviewGuidelines.md +++ b/docs/ReviewGuidelines.md @@ -20,7 +20,7 @@ as efficient as possible, uses the best algorithm available etc. - Modules are easy to read and have a well-defined scope - Any new correct files are suitably named. - Any new correct files are suitably located. -- Modules have sufficent documentation to understand there flow. +- Modules have sufficient documentation to understand there flow. These points are about readability of the project as a whole and how easy it is to find results within the project. From 967880111d18e18e99e51e952207c7b9a67e7b6e Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 5 Mar 2026 06:15:04 +0000 Subject: [PATCH 4/7] feat: Add link --- docs/ReviewGuidelines.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/docs/ReviewGuidelines.md b/docs/ReviewGuidelines.md index 739515f9a..263740bfa 100644 --- a/docs/ReviewGuidelines.md +++ b/docs/ReviewGuidelines.md @@ -26,9 +26,11 @@ These points are about readability of the project as a whole and how easy it is ## Style conventions -- Use less-then rather than greater-then. -- No new lines in proofs. -- Good use of `variables`. +In addition to those here: + +https://leanprover-community.github.io/contribute/style.html + +- Use of `lemma` instead of `theorem` except for the most important results. These points are related to how individual lemmas and theorems look, and how easy they are to read. From 2374c45ee68349ba71fd4e2b40bf01612122c422 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 5 Mar 2026 06:16:24 +0000 Subject: [PATCH 5/7] feat: change description --- docs/ReviewGuidelines.md | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/docs/ReviewGuidelines.md b/docs/ReviewGuidelines.md index 263740bfa..f519c6e3c 100644 --- a/docs/ReviewGuidelines.md +++ b/docs/ReviewGuidelines.md @@ -14,7 +14,7 @@ In another programming language these points analogous to not just making sure y have a function that does the right thing, but making sure that that function is as efficient as possible, uses the best algorithm available etc. -## Organization +## Organization - Lemmas and definitions appear in the correct place - Modules are easy to read and have a well-defined scope @@ -22,7 +22,7 @@ as efficient as possible, uses the best algorithm available etc. - Any new correct files are suitably located. - Modules have sufficient documentation to understand there flow. -These points are about readability of the project as a whole and how easy it is to find results within the project. +These points are about navigability of the project as a whole and how easy it is to find results within the project. ## Style conventions @@ -32,9 +32,7 @@ https://leanprover-community.github.io/contribute/style.html - Use of `lemma` instead of `theorem` except for the most important results. -These points are related to how individual lemmas and theorems look, and how easy they are -to read. - +These points are related to the readability of the project and results therein. ## PR and authorship - The author of the PR understands the material in the PR. From 26222037c15ee3ed96a98a637c8f5de33141a9e2 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 6 Mar 2026 11:53:56 +0000 Subject: [PATCH 6/7] Update ReviewGuidelines.md Co-Authored-By: Daniel Morrison <39346894+morrison-daniel@users.noreply.github.com> --- docs/ReviewGuidelines.md | 46 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 45 insertions(+), 1 deletion(-) diff --git a/docs/ReviewGuidelines.md b/docs/ReviewGuidelines.md index f519c6e3c..f5e014097 100644 --- a/docs/ReviewGuidelines.md +++ b/docs/ReviewGuidelines.md @@ -1,8 +1,17 @@ # Review guidelines -Below we give guidelines to what reviews of pull-requests to PhysLib are looking for. +Below we give guidelines to what reviews of pull-requests (PRs) to PhysLib are looking for. This list is not exhaustive and reviews are within the judgement of the reviewer. +A good place to start for both authors and reviewers is: +- [What to consider when reviewing](https://leanprover-community.github.io/contribute/pr-review.html#what-to-consider-when-reviewing) + + +Note that your PR does not need to be perfect once you make it, we will work +with you to improve its quality, if you are also willing to work with us. Just do +your best. You should expect that about 50% of the work happens after you make your PR, this is normal +and it should not discourage you. + ## Code quality - Correct abstraction of lemmas and definitions. @@ -33,6 +42,7 @@ https://leanprover-community.github.io/contribute/style.html - Use of `lemma` instead of `theorem` except for the most important results. These points are related to the readability of the project and results therein. + ## PR and authorship - The author of the PR understands the material in the PR. @@ -40,3 +50,37 @@ These points are related to the readability of the project and results therein. These points are not to the code-base itself but the history of the project and how easy it is for someone to find information on a given area from the git history. + +## PR lengths + +As a rule of thumb: + +- < 50 lines = easy to check PR +- < 100 lines = average sized PR +- 100-200 lines = large PR, okay but try to break up if possible +- 200+ lines = very large PR, should be broken up into smaller pieces + +There is no strict rule, as some very large PRs can be very simple e.g. documentation +or file reorganization and some small PRs can be very complicated e.g. adding definitions. + +Remember, the reviewer needs to understand your PR and the more there is for them +to understand, the harder it is. + +Small PRs are generally good because: + +- Small changes can be merged faster and not get blocked by unrelated work +- Reduces the chance and impact of merge conflicts +- Easier for reviewers to understand + +## Tag system + +We operator a tag system with our PRs. This makes it easier for reviewers and authors to +understand where in the process PRs are. +- Please tag your PR with the appropraite `t-subject` tag. +- PRs marked as `draft` will not be reviewed. +- PRs marked with a `awaiting-author` tag will also not be reviwed until the author + as addressed any reviewer comments and has removed this tag. +- If your PR is not getting reviewed and you would like to draw attention to it, please + post [here](https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLib/topic/PR.20reviews/with/577663418). +- Once a PR is marked with a `ready-to-merge` the author does not need to do anything else, + the maintainers will make sure it gets merged into the project. From cc3917d3c8fe4b3aac1faa4bdd36a4e4df93b925 Mon Sep 17 00:00:00 2001 From: Daniel Morrison <39346894+morrison-daniel@users.noreply.github.com> Date: Sun, 8 Mar 2026 21:58:03 -0700 Subject: [PATCH 7/7] Spelling fixes --- docs/ReviewGuidelines.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/ReviewGuidelines.md b/docs/ReviewGuidelines.md index f5e014097..a9f03b505 100644 --- a/docs/ReviewGuidelines.md +++ b/docs/ReviewGuidelines.md @@ -76,9 +76,9 @@ Small PRs are generally good because: We operator a tag system with our PRs. This makes it easier for reviewers and authors to understand where in the process PRs are. -- Please tag your PR with the appropraite `t-subject` tag. +- Please tag your PR with the appropriate `t-subject` tag. - PRs marked as `draft` will not be reviewed. -- PRs marked with a `awaiting-author` tag will also not be reviwed until the author +- PRs marked with a `awaiting-author` tag will also not be reviewed until the author as addressed any reviewer comments and has removed this tag. - If your PR is not getting reviewed and you would like to draw attention to it, please post [here](https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLib/topic/PR.20reviews/with/577663418).