feat: review claims via comments by Alex-Zughaid · Pull Request #1601 · leanprover-community/physlib

Alex-Zughaid · 2026-09-01T11:31:54Z

Allows reviewers to claim reviews by commenting claim
The default length is 2 days, but a user can type X days/weeks/hours after the claim command or type a specific date.
They can type disclaim to remove themselves.
Maximum time they can choose is 2 weeks.
24/48 hour warnings in the form of github comments.
If they are removed as a reviewer, they are mentioned in a comment again and also a message is sent to Zulip to let others know that the PR needs a new reviewer

[feat maintenance] Added actions scripts to count no. of reviewers

fix typo

Adds the Cloudflare Worker relay that bridges a Zulip outgoing webhook (bot receives a DM) to GitHub's repository_dispatch API, replacing the daily 8am cron trigger. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

.wrangler/ is gitignored going forward; this cache/account data shouldn't have been committed in the first place. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

This automation now lives at https://github.com/Alex-Zughaid/PhysLibBots instead of inside physlib itself. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

Backfills Jan-Jun 2026 (monthly-diffs/*.diff + index.json) and adds a scheduled workflow that generates the previous month's diff automatically on the 1st of each month, going forward.

Copilot attempt at making the diff automation workflow - happy with changes reviewed on Github

Instead of concatenating every commit's diff, compute a single diff between the last commit before the month started and the last commit within the month, strip all diff syntax, and keep only the raw lines that were added (grouped by file). Also fixes commit selection to walk the first-parent chain only - REF's history has merge commits, so two commits picked by date alone weren't guaranteed to be ancestors of each other, which was inflating some months' diffs by 5-6x.

Improved the readability of DIFF

Adds a small Verso (Manual genre) doc project that renders each month's added lines per file, then compiles that to a PDF with lualatex - mirrors how Verso builds its own User's Guide PDF. Backfills Jan-Jun 2026 and updates the scheduled workflow to build and commit the PDF each month (with Lake/Verso build caching, since a cold build compiles ~450 Lean files).

Removes the feature added in 94c58c1, reworked in 21992fb, and rebuilt on Verso/LaTeX in b0cc792: the generator scripts, the Verso doc project, the generated PDFs and index.json, and the scheduled workflow. The approach wasn't working out. Two problems drove this: - Month boundaries are resolved by walking --first-parent back from upstream/master's tip, which is required to stop non-linear history inflating a month's declaration count 5-6x. But the first-parent chain is not stable over time - a later merge can re-root the mainline, so regenerating a past month yields different contributors and line counts than the run that first produced it. - raw.githubusercontent.com serves the PDFs as application/octet-stream with X-Content-Type-Options: nosniff, so a browser can never render them inline; the links only ever downloaded a file. Co-Authored-By: Claude <noreply@anthropic.com>

github-actions · 2026-09-01T11:32:24Z

Thank you for this pull-request (PR). If this is your first PR, welcome to the community!

Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.

Some automated checks will be run on your PR. You can see the results of these checks at the buttom of your PR page. If any of these checks fail, you will need to fix the issues before your PR can be merged. You can learn more about these here, including how to run them locally, which is sometimes quicker than relying on the GitHub Actions. If you have never had a PR merged before, you may have to wait for a reviewer to manually start these checks (this is for security).
A reviewer will look at your PR and may ask you to make changes. This may happen a couple of days after you submit your PR, so you may need to be patient. But it should not be longer than that - if it is please bring it to the attention of the community on the Zulip. The level of review will depend on where your PR is submitted. If it is submitted to ./Physlib or ./QuantumInfo, the review will be more thorough than if it is submitted to ./PhyslibAlpha. You can find out more about what the review process is looking for in our review guidelines. If a reviewer adds an awaiting-author label to your PR, address the review comments, then please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.
The reviewer will either approve your PR, or request more changes (in which case we return to step 2). Once your PR is approved, it will be merged by a maintainer, this should happen shortly after approval, though you may get more comments at this stage.

Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages.

If you have any problems or questions, please reach out to the community on the Zulip.

Replaces the fixed `reviewing-in-1/2/3-days` labels with comment commands, so a reviewer can say `claim 5 days` rather than being limited to the windows someone thought to make a label for, and can claim without repository permissions. claim -- claim this PR for review, for the default 2 day window claim 5 days -- ... for a specific window (hours / days / weeks) claim 2026-08-01 -- ... until a specific date disclaim -- release the claim early The bot requests a review from the claimant, assigns them, applies `review-claimed` and keeps one status comment per PR whose hidden marker carries the whole claim record, edited in place as the claim is extended, completed or released. Reviewing completes the claim; `review_claim_expiry.yml` reminds the claimant 48h and 24h before the deadline and releases stale claims hourly, so nothing stays blocked forever. A claim that runs out without a review takes the claimant back off the PR as reviewer and assignee, and is announced on the `PR reviews` Zulip topic so that somebody else can pick the PR up -- using the same bot credentials as the workers in Alex-Zughaid/PhysLibBots. Only failures are announced. Missing Zulip secrets or a Zulip outage downgrade to a warning: releasing the claim on GitHub matters more than announcing it. A claim is cooperative rather than a lock: anyone may review a claimed PR. The one thing the bot refuses is silently overwriting a live claim -- a second `claim` is answered with who holds it and until when -- while the claimant can always `disclaim` and maintainers can release a claim on someone else's behalf. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Replaces the fixed `reviewing-in-1/2/3-days` labels with comment commands, so a reviewer can say `claim 5 days` rather than being limited to the windows someone thought to make a label for, and can claim without repository permissions. claim -- claim this PR for review, for the default 2 day window claim 5 days -- ... for a specific window (hours / days / weeks) claim 2026-08-01 -- ... until a specific date disclaim -- release the claim early The bot requests a review from the claimant, assigns them, applies `review-claimed` and keeps one status comment per PR whose hidden marker carries the whole claim record, edited in place as the claim is extended, completed or released. Reviewing completes the claim; `review_claim_expiry.yml` reminds the claimant 48h and 24h before the deadline and releases stale claims hourly, so nothing stays blocked forever. A claim that runs out without a review takes the claimant back off the PR as reviewer and assignee, and is announced on the `PR reviews` Zulip topic so that somebody else can pick the PR up -- using the same bot credentials as the workers in Alex-Zughaid/PhysLibBots. Only failures are announced. Missing Zulip secrets or a Zulip outage downgrade to a warning: releasing the claim on GitHub matters more than announcing it. A claim is cooperative rather than a lock: anyone may review a claimed PR. The one thing the bot refuses is silently overwriting a live claim -- a second `claim` is answered with who holds it and until when -- while the claimant can always `disclaim` and maintainers can release a claim on someone else's behalf. All three jobs are guarded on `github.repository`, as in `add_label_from_diff.yaml` and `pr_size_label.yaml`, so that forks do not run them. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Alex-Zughaid · 2026-09-02T08:43:34Z

claim

jstoobysmith · 2026-09-02T10:06:51Z

What happens when they review the PR, will they still get a comment?

Alex-Zughaid · 2026-09-02T10:18:19Z

What happens when they review the PR, will they still get a comment?

They don't get a comment and they aren't removed as a reviewer

jstoobysmith · 2026-09-02T10:26:12Z

Move to the main scripts file if possible?

Ports the claim logic from JavaScript running inside `actions/github-script` to Python, and moves it next to the repository's other Python tooling in `scripts/` rather than hiding it under `.github/scripts/`. The two workflows are now thin wrappers: each sparse-checks-out that one file and runs `python scripts/review_claim.py comment|review|expire`. The script is stdlib-only -- urllib against the REST API -- so the jobs need no dependency install, and it can be run by hand against a repository with a GITHUB_TOKEN. Behaviour is unchanged, except that the claim record in the status comment now stores ISO 8601 timestamps rather than epoch milliseconds, which reads better for anyone looking at the comment source. The jobs run the runner's preinstalled `python3` rather than setting up their own: the script is stdlib-only, so `actions/setup-python` bought nothing but a Node 20 deprecation warning and a slower job. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

jstoobysmith

Approved. Will merge shortly

Alex-Zughaid and others added 30 commits July 20, 2026 17:02

script with gh actions to find busy reviewers

071619f

Merge pull request #1 from Alex-Zughaid/github-reviewer-bot

850df50

[feat maintenance] Added actions scripts to count no. of reviewers

fix typo

fa6364a

Merge pull request #2 from Alex-Zughaid/github-reviewer-bot

e686209

fix typo

updated comments and check all PRs (not just last 30 days)

2ae17c8

dm

9f20a75

fix indent error

7e775c2

fix function error

35e133b

get rid of exception error

6981ba3

userID instead of email

3ddf58a

line numbers and labels

8363061

Merge branch 'master' into github-reviewer-bot

d17fbea

tidy up file

a65e180

add recently opened PRs to the summary

26498e0

repo updates

88d3ac7

implemented a few claude comments

9ef8d1d

Switch Repo Updates trigger to Zulip DM via repository_dispatch

330d8c9

Adds the Cloudflare Worker relay that bridges a Zulip outgoing webhook (bot receives a DM) to GitHub's repository_dispatch API, replacing the daily 8am cron trigger. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

Create wrangler-account.json

e29b19d

Merge branch 'leanprover-community:master' into master

79cf43f

Merge branch 'github-reviewer-bot'

d95b2fe

Remove Wrangler local cache from version control

c6ac999

.wrangler/ is gitignored going forward; this cache/account data shouldn't have been committed in the first place. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

change so doesnt post to thread

d33c7e3

Move repo-updates workflow, script, and Zulip relay to PhysLibBots

ee3ba0f

This automation now lives at https://github.com/Alex-Zughaid/PhysLibBots instead of inside physlib itself. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

Add monthly diff generation for physlib-website's Monthly Updates page

94c58c1

Backfills Jan-Jun 2026 (monthly-diffs/*.diff + index.json) and adds a scheduled workflow that generates the previous month's diff automatically on the 1st of each month, going forward.

Merge pull request #7 from Alex-Zughaid/monthly-diffs-automation

d42a8a5

Copilot attempt at making the diff automation workflow - happy with changes reviewed on Github

Merge pull request #8 from Alex-Zughaid/monthly-diffs-added-lines-only

079b0e7

Improved the readability of DIFF

Merge remote-tracking branch 'upstream/master'

5eae07e

github-actions Bot added the medium label Sep 1, 2026

Alex-Zughaid force-pushed the github-review-claim-labels branch from 37e01c3 to 24a20a0 Compare September 1, 2026 11:47

github-actions Bot added large and removed medium labels Sep 1, 2026

Alex-Zughaid force-pushed the github-review-claim-labels branch from 24a20a0 to c3195dc Compare September 1, 2026 14:49

Alex-Zughaid force-pushed the github-review-claim-labels branch from c3195dc to 012ad62 Compare September 2, 2026 08:06

Alex-Zughaid changed the title ~~GitHub review claim labels~~ feat(ci): review claims via claim / disclaim comments Sep 2, 2026

Alex-Zughaid changed the title ~~feat(ci): review claims via claim / disclaim comments~~ feat(ci): review claims via comments Sep 2, 2026

merge

08791e7

Alex-Zughaid marked this pull request as ready for review September 2, 2026 08:59

Update ReviewGuidelines.md

872d7d6

Alex-Zughaid changed the title ~~feat(ci): review claims via comments~~ feat: review claims via comments Sep 2, 2026

jstoobysmith reviewed Sep 2, 2026

View reviewed changes

Comment thread .github/scripts/review-claim.js Outdated

jstoobysmith Sep 2, 2026

Copy link
Copy Markdown

Member

Choose a reason for hiding this comment

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

Move to the main scripts file if possible?

Alex-Zughaid force-pushed the github-review-claim-labels branch from f8c8aff to dad2ba3 Compare September 2, 2026 17:01

jstoobysmith approved these changes Sep 3, 2026

View reviewed changes

jstoobysmith added the ready-to-merge This PR is approved and will be merged shortly label Sep 3, 2026

jstoobysmith merged commit c9ae1ba into leanprover-community:master Sep 3, 2026
9 checks passed

Navigation Menu

Uh oh!

feat: review claims via comments - #1601

feat: review claims via comments#1601
jstoobysmith merged 35 commits into
leanprover-community:masterfrom
Alex-Zughaid:github-review-claim-labels

Alex-Zughaid commented Sep 1, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Sep 1, 2026

Uh oh!

Alex-Zughaid commented Sep 2, 2026

Uh oh!

jstoobysmith commented Sep 2, 2026

Uh oh!

Alex-Zughaid commented Sep 2, 2026

Uh oh!

jstoobysmith Sep 2, 2026

Uh oh!

jstoobysmith left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

Alex-Zughaid commented Sep 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Sep 1, 2026

Uh oh!

Alex-Zughaid commented Sep 2, 2026

Uh oh!

jstoobysmith commented Sep 2, 2026

Uh oh!

Alex-Zughaid commented Sep 2, 2026

Uh oh!

jstoobysmith Sep 2, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Alex-Zughaid commented Sep 1, 2026 •

edited

Loading