Skip to content

feat: Update Readme with PhysilbAlpha#1170

Open
jstoobysmith wants to merge 2 commits into
leanprover-community:masterfrom
jstoobysmith:readme-update
Open

feat: Update Readme with PhysilbAlpha#1170
jstoobysmith wants to merge 2 commits into
leanprover-community:masterfrom
jstoobysmith:readme-update

Conversation

@jstoobysmith

Copy link
Copy Markdown
Member

Updating the Readme with a description of PhysilbAlpha.

@jstoobysmith jstoobysmith requested a review from Timeroot June 11, 2026 12:12
@github-actions

Copy link
Copy Markdown
Contributor

Thank you for this PR, which will now be reviewed. Please
see our review guidelines
if you are not familiar with the process. You should expect a back and forth
with a reviewer before your PR is merged. See also that link for how to
add appropriate labels to your PR. The PR will also go through a number
of automated checks. You can learn more about these here,
including how to run them locally.

If you want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.

@morrison-daniel

Copy link
Copy Markdown
Collaborator

We may want to describe what the review standard is, even if it is low so it's clear why a PR would pass/not pass

Clarified the review standards for PhyslibAlpha and its contribution maintenance policy.
@jstoobysmith

Copy link
Copy Markdown
Member Author

@morrison-daniel Done

@morrison-daniel morrison-daniel left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll approve so you can merge if you want, but feel free to wait for more feedback

Comment thread README.md

## PhyslibAlpha

PhyslibAlpha sits downstream of `./Physlib` (within the same repository). The core idea is that PhyslibAlpha has a lower review-standards then Physlib making it easier to get large PRs, AI-generated content, or formalizations which are not-quite-perfect in. PRs for PhyslibAlpha must pass basic linter checks, described [here](https://github.com/leanprover-community/physlib/blob/master/scripts/PhyslibAlpha/README.md). PRs must also undergo a light 'one-look' review checking 1) Whether the content is main-stream physics, 2) Whether it looks reasonable (no axioms, easy to read etc.), 3) Whether it is within the right place within PhyslibAlpha (mirroring its place in Physlib).

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
PhyslibAlpha sits downstream of `./Physlib` (within the same repository). The core idea is that PhyslibAlpha has a lower review-standards then Physlib making it easier to get large PRs, AI-generated content, or formalizations which are not-quite-perfect in. PRs for PhyslibAlpha must pass basic linter checks, described [here](https://github.com/leanprover-community/physlib/blob/master/scripts/PhyslibAlpha/README.md). PRs must also undergo a light 'one-look' review checking 1) Whether the content is main-stream physics, 2) Whether it looks reasonable (no axioms, easy to read etc.), 3) Whether it is within the right place within PhyslibAlpha (mirroring its place in Physlib).
PhyslibAlpha sits downstream of `./Physlib` (within the same repository). The core idea is that PhyslibAlpha has a lower review-standards then Physlib making it easier to contribute large PRs, AI-generated content, or formalizations which are not-quite-perfect. PRs for PhyslibAlpha must pass basic linter checks, described [here](https://github.com/leanprover-community/physlib/blob/master/scripts/PhyslibAlpha/README.md). PRs must also undergo a light 'one-look' review checking 1) Whether the content is main-stream physics, 2) Whether it looks reasonable (no axioms, easy to read etc.), 3) Whether it is within the right place within PhyslibAlpha (mirroring its place in Physlib).

Small fix to make the sentence easier to read

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants