feat(ci): review claims via claim / disclaim comments

[Alex-Zughaid]

Replaces the fixed reviewing-in-1/2/3-days labels from the first draft of this PR with
comment commands, modelled on the intentions bot.
Two reasons the label version was worse: a window had to have been thought of in advance
and made into a label, and applying a label needs repository permissions that a first-time
reviewer does not have.

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 a single status comment per PR. Claiming again extends the window; submitting a review completes the claim.
Stale claims are released hourly, so nothing stays blocked forever.

Default window	2 days
Maximum window	14 days (longer requests are clamped, and the claimant is told)
Reminders	@-mention at 48h and 24h before the deadline
On expiry	reviewer, assignee and label removed; @-mention comment; announced on Zulip
On review	label removed, assignee kept, claim marked completed

A claim is cooperative, not 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. The claimant can always disclaim, and maintainers can release someone
else's claim without waiting for it to time out.

Zulip

A claim that runs out without a review is announced on the PR reviews topic, so that
somebody else can pick the PR up:

Review claim expired on physlib#123: Some PR title

octocat claimed this review until 2026-09-03 12:00 UTC, but no review arrived, so they
have been removed as a reviewer and the PR is back in the review queue. It is open for
anyone to claim.

Only failures are announced — a claim that is honoured, extended or disclaimed is nobody
else's business. This uses the ZULIP_SITE, ZULIP_BOT_EMAIL, ZULIP_BOT_API_KEY and
ZULIP_STREAM secrets already set on this repository, hitting the same /api/v1/messages
endpoint as postToZulip in PhysLibBots.
Missing secrets or a Zulip outage downgrade to a warning: releasing the claim on GitHub
matters more than announcing it. The claimant is named rather than @-mentioned, since a
GitHub login is not a Zulip name.

Design notes

• One place for the state. The whole claim record lives in a hidden marker in the bot's
  status comment, edited in place rather than reposted. Extending a claim moves the deadline
  and resets its reminders with it, and a PR ends up with at most one status comment.
• Commands are whole lines, as in labels_from_comment.yml, so a comment discussing
  claims does not trigger one. Any casing works; the last command in a comment wins.
• No duplicate or stale nudges. Each reminder carries a marker keyed to the deadline.
  GitHub silently skips scheduled runs under load, so reminders are checked smallest-first:
  waking with 20h left sends the 24h reminder, not a wrong "48 hours are left" one.
• The review request is best-effort. Claiming needs no repository permissions, but
  GitHub refuses a review request for a non-collaborator or for the PR's own author, so
  that call is allowed to fail while the label and assignee always land.
• Shared logic lives in .github/scripts/review-claim.js, pulled in by both workflows
  via a sparse checkout, rather than being copied between them.
• Unlike add_label_from_diff.yaml and pr_size_label.yaml, these carry no
  github.repository == 'leanprover-community/physlib' guard — that guard makes those two
  workflows no-ops in this fork, and these are meant to run here.

Testing

28 unit assertions over the command grammar, window parsing (including clamping, past dates
and garbage) and the marker round-trip, plus 20 scenarios driven through both workflows
against a mock Octokit: claim, extend, claim over someone else's claim, over-long window,
unparseable window, disclaim by claimant / by a non-claimant / by a maintainer / with
nothing held, prose that merely mentions claiming, review by the claimant and by a
stranger, every reminder threshold, an already-posted reminder, a skipped scheduled run, an
already-reviewed claimant, expiry with and without a review, and a stale label with no
claim record, plus the Zulip path with secrets present, with secrets absent, and with the
Zulip API returning 500 — in both failure cases the GitHub-side release still completes.

Label review-claimed created; the three unused reviewing-in-* labels have been deleted.

🤖 Generated with Claude Code

[github-actions]

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.

1. 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).

2. 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.

3. 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.