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

.github/workflows/review_claim.yml

@@ -0,0 +1,86 @@
+# Review claims: `claim` / `disclaim` commands on a pull request.
+#
+# To avoid two reviewers (human or AI) picking up the same PR, a reviewer says
+# what they intend to review and claims it:
+#
+#   claim              -- claim this PR for review, for the default 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 assigns the claimant, applies the `review-claimed` label and keeps a
+# single status comment recording the deadline.  Claiming again extends the
+# window; submitting a review completes the claim.  Stale claims are released
+# automatically by `review_claim_expiry.yml`, so nothing stays blocked forever.
+#
+# A claim is cooperative, not a lock: it signals intent so that others can steer
+# around it, and anyone remains free to review the PR.
+#
+# As in `labels_from_comment.yml`, a command is a whole line of the comment, so
+# that a comment merely discussing claims does not trigger one.  Commands need
+# no repository permissions -- anyone can claim a review.
+#
+# The work itself is in `scripts/review_claim.py`.
+
+name: Review claims
+
+on:
+  issue_comment:
+    types: [created]
+  pull_request_review:
+    types: [submitted]
+
+# Limit permissions for GITHUB_TOKEN for the entire workflow
+permissions:
+  contents: read
+  issues: write         # Only allow issue/PR comments, labels and reactions
+  pull-requests: write  # Only allow PR comments/labels/assignees
+  # All other permissions are implicitly 'none'
+
+jobs:
+  command:
+    name: Handle claim command
+    runs-on: ubuntu-latest
+    # Cheap prefilter: only comments on PRs, and only ones that mention a command
+    # at all, reach the checkout below.  `disclaim` contains `claim`, so one test
+    # covers both; the capitalised variant is here because expressions have no
+    # case-insensitive compare, while the parser itself accepts any casing.
+    #
+    # Don't run on forks, where we wouldn't have permission to act on the PR anyway.
+    if: >-
+      github.repository == 'leanprover-community/physlib' &&
+      github.event_name == 'issue_comment' &&
+      github.event.issue.pull_request &&
+      github.event.comment.user.type != 'Bot' &&
+      (contains(github.event.comment.body, 'claim') ||
+       contains(github.event.comment.body, 'Claim'))
+    steps:
+      - name: Check out the claim script
+        uses: actions/checkout@v7.0.0
+        with:
+          sparse-checkout: scripts/review_claim.py
+          sparse-checkout-cone-mode: false
+          persist-credentials: false
+      - name: Claim or disclaim
+        run: python3 scripts/review_claim.py comment
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+  complete:
+    name: Complete claim on review
+    runs-on: ubuntu-latest
+    # Don't run on forks, where we wouldn't have permission to act on the PR anyway.
+    if: >-
+      github.repository == 'leanprover-community/physlib' &&
+      github.event_name == 'pull_request_review'
+    steps:
+      - name: Check out the claim script
+        uses: actions/checkout@v7.0.0
+        with:
+          sparse-checkout: scripts/review_claim.py
+          sparse-checkout-cone-mode: false
+          persist-credentials: false
+      - name: Clear the claim once its claimant has reviewed
+        run: python3 scripts/review_claim.py review
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/review_claim_expiry.yml

@@ -0,0 +1,57 @@
+# Gives review claims a time to live, so that nothing stays blocked forever.
+#
+# A reviewer claims a PR by commenting `claim` (see `review_claim.yml`).  This
+# workflow runs hourly and, for every PR carrying the `review-claimed` label:
+#
+#   * @-mentions the claimant 48h and then 24h before the deadline, skipping a
+#     reminder that is not shorter than the window they asked for;
+#   * once the deadline passes, completes the claim quietly if they did review
+#     in time, and otherwise releases it -- dropping the label and taking the
+#     claimant off the PR as reviewer and assignee -- announcing the release on
+#     Zulip so that somebody else picks the PR up.
+#
+# The deadline is read back out of the claim's status comment, so extending a
+# claim (`claim` again) moves the deadline and resets its reminders with it.
+#
+# The work itself is in `scripts/review_claim.py`.
+
+name: Expire review claims
+
+on:
+  schedule:
+    # hourly, so a deadline or a reminder is never overshot by more than an hour
+    - cron: '0 * * * *'
+  workflow_dispatch:
+
+# Limit permissions for GITHUB_TOKEN for the entire workflow
+permissions:
+  contents: read
+  issues: write         # Only allow reading/labelling issues
+  pull-requests: write  # Only allow PR comments/labels/assignees
+  # All other permissions are implicitly 'none'
+
+jobs:
+  expire:
+    name: Expire review claims
+    runs-on: ubuntu-latest
+    # Don't run on forks, where we wouldn't have permission to act on the PR anyway.
+    if: github.repository == 'leanprover-community/physlib'
+    steps:
+      - name: Check out the claim script
+        uses: actions/checkout@v7.0.0
+        with:
+          sparse-checkout: scripts/review_claim.py
+          sparse-checkout-cone-mode: false
+          persist-credentials: false
+      - name: Remind and expire
+        run: python3 scripts/review_claim.py expire
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          # Same bot credentials as the Physlib Zulip bots.  Missing secrets
+          # downgrade to a warning rather than failing the job: releasing the
+          # claim on GitHub matters more than announcing it.
+          ZULIP_SITE: ${{ secrets.ZULIP_SITE }}
+          ZULIP_BOT_EMAIL: ${{ secrets.ZULIP_BOT_EMAIL }}
+          ZULIP_BOT_API_KEY: ${{ secrets.ZULIP_BOT_API_KEY }}
+          ZULIP_STREAM: ${{ secrets.ZULIP_STREAM }}
+          ZULIP_TOPIC: PR reviews

docs/ReviewGuidelines.md

@@ -84,3 +84,20 @@ understand where in the process PRs are.
   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.
+
+## Claiming a PR for review
+
+To keep track of PRs, reviewers can "claim" PRs and promise to review them within a certain timeframe. Failing to submit a review in that time will trigger a workflow which removes them and a Zulip bot notifies the community.
+
+1. **Claim it.** Comment `claim` on the PR. The bot requests a review from you, assigns
+   you, applies the `review-claimed` label and leaves a status comment recording the
+   deadline. For a custom window, comment `claim 5 days` (hours, days and weeks all work)
+   or `claim 2026-08-01`; `claim` uses the default of 2 days.
+2. **You are reminded.** The bot @-mentions you 48 hours and then 24 hours before the
+   deadline.
+3. **It expires.** Claims carry a time to live (2 days by default, 14 days max) and are
+   released automatically if they go stale, so nothing stays blocked forever. Comment
+   `claim` again to extend, or `disclaim` to release early. Submitting a review completes
+   the claim and clears the label.
+4. **A missed claim is announced.** If the deadline passes with no review, you are removed
+   as reviewer and assignee, and a message goes to the `PR reviews` topic on Zulip.