From c3195dc4195c5021889f577cf99414580937a675 Mon Sep 17 00:00:00 2001 From: Alex-Zughaid <117576511+Alex-Zughaid@users.noreply.github.com> Date: Tue, 1 Sep 2026 12:46:54 +0100 Subject: [PATCH 1/4] feat(ci): review claims, modelled on the intentions bot 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 --- .github/scripts/review-claim.js | 286 ++++++++++++++++++++++ .github/workflows/review_claim.yml | 195 +++++++++++++++ .github/workflows/review_claim_expiry.yml | 156 ++++++++++++ docs/ReviewGuidelines.md | 35 +++ 4 files changed, 672 insertions(+) create mode 100644 .github/scripts/review-claim.js create mode 100644 .github/workflows/review_claim.yml create mode 100644 .github/workflows/review_claim_expiry.yml diff --git a/.github/scripts/review-claim.js b/.github/scripts/review-claim.js new file mode 100644 index 0000000000..aed4b47159 --- /dev/null +++ b/.github/scripts/review-claim.js @@ -0,0 +1,286 @@ +// Shared helpers for the review claim workflows. +// +// A claim is a promise to review a PR within a window: a reviewer comments +// `claim` (optionally with a window) and the bot records that promise, reminds +// them as the deadline approaches and releases the claim if it goes stale. +// +// The whole state of a claim lives in one bot-maintained comment per PR, in a +// hidden marker holding a JSON record. That comment is edited in place rather +// than reposted, so a PR accumulates at most one claim status comment however +// many times the claim is extended, and there is nothing to keep in sync +// anywhere else. +// +// Used by `.github/workflows/review_claim.yml` (commands) and +// `.github/workflows/review_claim_expiry.yml` (reminders and expiry). + +const CLAIM_LABEL = 'review-claimed'; +const MARKER_PREFIX = ''; + +const HOUR_MS = 60 * 60 * 1000; +const DAY_MS = 24 * HOUR_MS; + +// A review claim is a short promise, so the windows are much tighter than the +// roadmap intentions this is modelled on. +const DEFAULT_WINDOW_MS = 2 * DAY_MS; +const MAX_WINDOW_MS = 14 * DAY_MS; +const MIN_WINDOW_MS = 1 * HOUR_MS; + +// Reminders are @-mentions sent this many hours before the deadline. A +// reminder is skipped when it is not shorter than the window itself, so a +// 24 hour claim is never warned about 24 hours before it ends. Ascending, so +// that the smallest applicable reminder wins if a scheduled run is skipped. +const REMINDERS_HOURS = [24, 48]; + +const UNITS = { + hour: HOUR_MS, hours: HOUR_MS, + day: DAY_MS, days: DAY_MS, + week: 7 * DAY_MS, weeks: 7 * DAY_MS, +}; + +/** Format a timestamp the way the bot's comments always spell one out. */ +const formatUTC = when => new Date(when).toISOString().replace('T', ' ').slice(0, 16) + ' UTC'; + +/** Spell a duration back to the claimant, so they can check what was understood. */ +function describeWindow(ms) { + const round = value => Number(value.toFixed(1)).toString(); + if (ms % DAY_MS === 0 && ms >= DAY_MS) { + const days = ms / DAY_MS; + return days % 7 === 0 + ? `${round(days / 7)} week${days === 7 ? '' : 's'}` + : `${round(days)} day${days === 1 ? '' : 's'}`; + } + const hours = ms / HOUR_MS; + return `${round(hours)} hour${hours === 1 ? '' : 's'}`; +} + +/** + * Parse the argument of a `claim` command into a deadline. + * + * Accepts an empty argument (the default window), ` hours|days|weeks`, or an + * absolute `YYYY-MM-DD` date, which is read as the end of that day UTC. Over-long + * windows are clamped rather than rejected, and the caller is told via `clamped`. + */ +function parseWindow(argument, now) { + const trimmed = (argument || '').trim().toLowerCase(); + + let until; + if (trimmed === '') { + until = now + DEFAULT_WINDOW_MS; + } else if (/^\d{4}-\d{2}-\d{2}$/.test(trimmed)) { + until = Date.parse(`${trimmed}T23:59:59Z`); + if (Number.isNaN(until)) return { error: `\`${trimmed}\` is not a real date.` }; + } else { + const match = trimmed.match(/^(\d+)\s*(hour|hours|day|days|week|weeks)$/); + if (!match) { + return { + error: `I could not read \`${trimmed}\` as a window. Use \`claim\`, ` + + '`claim 5 days` (or hours/weeks), or `claim 2026-08-01`.', + }; + } + until = now + Number(match[1]) * UNITS[match[2]]; + } + + if (until - now < MIN_WINDOW_MS) { + return { error: 'That window is already over. Pick a deadline in the future.' }; + } + const clamped = until - now > MAX_WINDOW_MS; + if (clamped) until = now + MAX_WINDOW_MS; + return { until, clamped }; +} + +/** + * Read a command out of a comment body. + * + * As elsewhere in this repository, a command is a whole line: the bot reacts to + * a line whose entire content, up to whitespace, is the command, so that a + * comment merely discussing claims does not trigger one. The last command in a + * comment wins. + */ +function parseCommand(body) { + const lines = (body || '').replace(/\r/g, '').split('\n'); + let command = null; + for (const line of lines) { + const trimmed = line.trim(); + const claim = trimmed.match(/^claim\b(.*)$/i); + if (claim) command = { name: 'claim', argument: claim[1] }; + else if (/^disclaim$/i.test(trimmed)) command = { name: 'disclaim' }; + } + return command; +} + +/** The status comment among an already-fetched list, or null if there is none. */ +function pickStatusComment(comments) { + return [...comments].reverse() + .find(comment => comment.body && comment.body.includes(MARKER_PREFIX)) || null; +} + +/** The bot's status comment for this PR, or null if it has never claimed one. */ +async function findStatusComment(github, { owner, repo, issue_number }) { + const comments = await github.paginate(github.rest.issues.listComments, { + owner, repo, issue_number, per_page: 100, + }); + return pickStatusComment(comments); +} + +/** The claim record carried by a status comment, or null if it is unreadable. */ +function readClaim(comment) { + if (!comment || !comment.body) return null; + const start = comment.body.indexOf(MARKER_PREFIX); + if (start === -1) return null; + const end = comment.body.indexOf(MARKER_SUFFIX, start); + if (end === -1) return null; + const json = comment.body.slice(start + MARKER_PREFIX.length, end); + try { + return JSON.parse(json); + } catch (error) { + return null; + } +} + +/** Render the status comment body for a claim record. */ +function renderStatus(claim) { + const marker = MARKER_PREFIX + JSON.stringify(claim) + MARKER_SUFFIX; + + if (claim.state === 'released') { + return [marker, `Review claim by @${claim.claimant} released. This PR is back in the review queue.`].join('\n'); + } + if (claim.state === 'completed') { + return [marker, `Review claim by @${claim.claimant} completed — thanks for the review.`].join('\n'); + } + if (claim.state === 'expired') { + return [ + marker, + `Review claim by @${claim.claimant} expired on ${formatUTC(claim.until)} without a review.`, + 'This PR is back in the review queue.', + ].join('\n'); + } + + const window = describeWindow(claim.until - claim.claimedAt); + const reminders = REMINDERS_HOURS + .filter(hours => hours * HOUR_MS < claim.until - claim.claimedAt) + .sort((a, b) => b - a); + + return [ + marker, + `**@${claim.claimant} has claimed this PR for review** until ${formatUTC(claim.until)} (${window}).`, + '', + reminders.length + ? `I will remind them here ${reminders.map(h => `${h}h`).join(' and ')} before that runs out.` + : 'That window is too short for a reminder, so there will not be one.', + 'If no review lands in time the claim is released automatically and this PR returns to', + 'the review queue.', + '', + 'Comment `claim` to extend, `claim 5 days` / `claim 2026-08-01` for a specific window, or', + '`disclaim` to release it early. A claim is cooperative, not a lock: it signals intent so', + 'that others can steer around it, and anyone is still free to review this PR.', + ].join('\n'); +} + +/** Create or edit the single status comment carrying the claim record. */ +async function writeStatus(github, { owner, repo, issue_number }, claim, existing) { + const body = renderStatus(claim); + if (existing) { + await github.rest.issues.updateComment({ owner, repo, comment_id: existing.id, body }); + return existing; + } + const { data } = await github.rest.issues.createComment({ owner, repo, issue_number, body }); + return data; +} + +/** + * Has the claimant looked at the PR since claiming it? A submitted review or an + * inline review comment both count; a plain issue comment deliberately does not. + */ +async function hasReviewedSince(github, { owner, repo, issue_number }, claimant, since) { + const reviews = await github.paginate(github.rest.pulls.listReviews, { + owner, repo, pull_number: issue_number, per_page: 100, + }); + if (reviews.some(review => + review.user.login === claimant && Date.parse(review.submitted_at) >= since)) return true; + + const reviewComments = await github.paginate(github.rest.pulls.listReviewComments, { + owner, repo, pull_number: issue_number, per_page: 100, + }); + return reviewComments.some(comment => + comment.user.login === claimant && Date.parse(comment.created_at) >= since); +} + +/** + * Put the claimant on the PR as both assignee and requested reviewer. + * + * Requesting a review is the half that shows up in everyone's review queue, but + * GitHub refuses it for a non-collaborator and for the PR's own author, and + * claiming deliberately needs no permissions -- so that half is best-effort. + */ +async function takeClaim(github, core, { owner, repo, issue_number }, claimant) { + await github.rest.issues.addLabels({ owner, repo, issue_number, labels: [CLAIM_LABEL] }) + .catch(error => core.warning(`#${issue_number}: could not label: ${error.message}`)); + await github.rest.issues.addAssignees({ owner, repo, issue_number, assignees: [claimant] }) + .catch(error => core.warning(`#${issue_number}: could not assign '${claimant}': ${error.message}`)); + await github.rest.pulls.requestReviewers({ owner, repo, pull_number: issue_number, reviewers: [claimant] }) + .catch(error => core.warning(`#${issue_number}: could not request review from '${claimant}': ${error.message}`)); +} + +/** + * Drop the claim label and, when a claimant is given, take them back off the PR + * as reviewer and assignee. Every step tolerates its target being gone already. + */ +async function releaseClaim(github, core, { owner, repo, issue_number }, claimant) { + await github.rest.issues.removeLabel({ owner, repo, issue_number, name: CLAIM_LABEL }) + .catch(error => core.warning(`#${issue_number}: could not remove '${CLAIM_LABEL}': ${error.message}`)); + if (!claimant) return; + await github.rest.issues.removeAssignees({ owner, repo, issue_number, assignees: [claimant] }) + .catch(error => core.warning(`#${issue_number}: could not unassign '${claimant}': ${error.message}`)); + await github.rest.pulls.removeRequestedReviewers({ owner, repo, pull_number: issue_number, reviewers: [claimant] }) + .catch(error => core.warning(`#${issue_number}: could not drop the review request for '${claimant}': ${error.message}`)); +} + +/** + * Announce something on Zulip, using the same bot credentials and message API as + * the workers in Alex-Zughaid/PhysLibBots. + * + * A missing or broken Zulip setup must never take a workflow down with it: the + * GitHub side of an expiry has already happened by the time this is called, so a + * failure here is warned about and swallowed. + */ +async function notifyZulip(core, content) { + const { ZULIP_SITE, ZULIP_BOT_EMAIL, ZULIP_BOT_API_KEY, ZULIP_STREAM, ZULIP_TOPIC } = process.env; + if (!ZULIP_SITE || !ZULIP_BOT_EMAIL || !ZULIP_BOT_API_KEY || !ZULIP_STREAM) { + core.warning('Zulip is not configured (ZULIP_SITE / ZULIP_BOT_EMAIL / ZULIP_BOT_API_KEY / ZULIP_STREAM), skipping the announcement.'); + return false; + } + + // `to` takes a stream name or a stream id, so ZULIP_STREAM can be either. + const body = new URLSearchParams({ + type: 'stream', to: ZULIP_STREAM, topic: ZULIP_TOPIC || 'PR reviews', content, + }); + const credentials = Buffer.from(`${ZULIP_BOT_EMAIL}:${ZULIP_BOT_API_KEY}`).toString('base64'); + + try { + const response = await fetch(`${ZULIP_SITE.replace(/\/$/, '')}/api/v1/messages`, { + method: 'POST', + headers: { + Authorization: `Basic ${credentials}`, + 'Content-Type': 'application/x-www-form-urlencoded', + }, + body, + }); + if (!response.ok) { + core.warning(`Zulip API error: ${response.status} ${await response.text()}`); + return false; + } + return true; + } catch (error) { + core.warning(`Could not reach Zulip: ${error.message}`); + return false; + } +} + +module.exports = { + CLAIM_LABEL, HOUR_MS, DAY_MS, REMINDERS_HOURS, + DEFAULT_WINDOW_MS, MAX_WINDOW_MS, + formatUTC, describeWindow, parseWindow, parseCommand, + pickStatusComment, findStatusComment, readClaim, renderStatus, writeStatus, + hasReviewedSince, takeClaim, releaseClaim, notifyZulip, +}; diff --git a/.github/workflows/review_claim.yml b/.github/workflows/review_claim.yml new file mode 100644 index 0000000000..5d76e44c6f --- /dev/null +++ b/.github/workflows/review_claim.yml @@ -0,0 +1,195 @@ +# 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. + +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. + if: >- + 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 helpers + uses: actions/checkout@v7.0.0 + with: + sparse-checkout: .github/scripts + persist-credentials: false + - name: Claim or disclaim + uses: actions/github-script@v7 + with: + script: | + const claims = require(`${process.env.GITHUB_WORKSPACE}/.github/scripts/review-claim.js`); + const { owner, repo } = context.repo; + const issue_number = context.payload.issue.number; + const target = { owner, repo, issue_number }; + const actor = context.payload.comment.user.login; + const commentId = context.payload.comment.id; + const now = Date.now(); + + const command = claims.parseCommand(context.payload.comment.body); + if (!command) { + core.info('No claim command in this comment.'); + return; + } + + const react = content => github.rest.reactions.createForIssueComment({ + owner, repo, comment_id: commentId, content, + }).catch(error => core.warning(`Could not react: ${error.message}`)); + + const reject = async message => { + await react('confused'); + await github.rest.issues.createComment({ + owner, repo, issue_number, body: `@${actor} ${message}`, + }); + }; + + const statusComment = await claims.findStatusComment(github, target); + const current = claims.readClaim(statusComment); + const active = current && current.state === 'active' ? current : null; + + if (command.name === 'disclaim') { + if (!active) { + core.info(`#${issue_number}: nothing to disclaim.`); + await react('confused'); + return; + } + // The claimant can always let go; a maintainer can release someone + // else's claim without waiting for it to time out. + let permitted = active.claimant === actor; + if (!permitted) { + const { data: access } = await github.rest.repos.getCollaboratorPermissionLevel({ + owner, repo, username: actor, + }).catch(() => ({ data: { permission: 'none' } })); + permitted = ['admin', 'maintain', 'write'].includes(access.permission); + } + if (!permitted) { + await reject( + `this PR is claimed by @${active.claimant} until ${claims.formatUTC(active.until)}, ` + + 'and only they (or a maintainer) can release it. It will be released ' + + 'automatically if no review arrives by then.'); + return; + } + + core.info(`#${issue_number}: ${actor} released the claim held by ${active.claimant}.`); + await claims.releaseClaim(github, core, target, active.claimant); + await claims.writeStatus(github, target, + { ...active, state: 'released', releasedBy: actor }, statusComment); + await react('+1'); + return; + } + + // Someone else's live claim is not silently overwritten: the point of + // the whole mechanism is that a second reviewer finds out before + // duplicating the work. + if (active && active.claimant !== actor) { + await reject( + `this PR is already claimed by @${active.claimant} until ` + + `${claims.formatUTC(active.until)}. It will be released automatically if no ` + + 'review arrives by then, and you are still free to review it in the meantime ' + + '— a claim signals intent rather than locking anyone out.'); + return; + } + + const window = claims.parseWindow(command.argument, now); + if (window.error) { + await reject(window.error); + return; + } + + const claim = { + state: 'active', + claimant: actor, + // Extending keeps the original claim time, so the status comment + // keeps describing the window the claimant actually asked for. + claimedAt: now, + until: window.until, + }; + + await claims.takeClaim(github, core, target, actor); + await claims.writeStatus(github, target, claim, statusComment); + await react('+1'); + + if (window.clamped) { + await github.rest.issues.createComment({ + owner, repo, issue_number, + body: `@${actor} that window was longer than the ` + + `${claims.describeWindow(claims.MAX_WINDOW_MS)} maximum, so I shortened it to ` + + `${claims.formatUTC(window.until)}. Comment \`claim\` again to extend it later.`, + }); + } + core.info(`#${issue_number}: ${actor} claimed until ${new Date(window.until).toISOString()}.`); + + complete: + name: Complete claim on review + runs-on: ubuntu-latest + if: github.event_name == 'pull_request_review' + steps: + - name: Check out the claim helpers + uses: actions/checkout@v7.0.0 + with: + sparse-checkout: .github/scripts + persist-credentials: false + - name: Clear the claim once its claimant has reviewed + uses: actions/github-script@v7 + with: + script: | + const claims = require(`${process.env.GITHUB_WORKSPACE}/.github/scripts/review-claim.js`); + const { owner, repo } = context.repo; + const issue_number = context.payload.pull_request.number; + const target = { owner, repo, issue_number }; + const reviewer = context.payload.review.user.login; + + const statusComment = await claims.findStatusComment(github, target); + const current = claims.readClaim(statusComment); + if (!current || current.state !== 'active' || current.claimant !== reviewer) { + core.info(`#${issue_number}: review by ${reviewer} does not close an active claim.`); + return; + } + + core.info(`#${issue_number}: ${reviewer} reviewed, completing their claim.`); + // The label goes, but the assignee stays: they are engaged with this + // PR now, which is the opposite of the case the expiry job handles. + await claims.releaseClaim(github, core, target, null); + await claims.writeStatus(github, target, + { ...current, state: 'completed' }, statusComment); diff --git a/.github/workflows/review_claim_expiry.yml b/.github/workflows/review_claim_expiry.yml new file mode 100644 index 0000000000..f6da10ff10 --- /dev/null +++ b/.github/workflows/review_claim_expiry.yml @@ -0,0 +1,156 @@ +# 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 the assignee +# and saying so -- putting the PR back into the general review queue. +# +# 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. + +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 + steps: + - name: Check out the claim helpers + uses: actions/checkout@v7.0.0 + with: + sparse-checkout: .github/scripts + persist-credentials: false + - name: Remind and expire + uses: actions/github-script@v7 + env: + # Same bot credentials as the workers in Alex-Zughaid/PhysLibBots. + # 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 + with: + script: | + const claims = require(`${process.env.GITHUB_WORKSPACE}/.github/scripts/review-claim.js`); + const { owner, repo } = context.repo; + const now = Date.now(); + + const issues = await github.paginate(github.rest.issues.listForRepo, { + owner, repo, state: 'open', labels: claims.CLAIM_LABEL, per_page: 100, + }); + + for (const issue of issues) { + // `listForRepo` returns issues and PRs alike; we only want PRs. + if (!issue.pull_request) continue; + const issue_number = issue.number; + const target = { owner, repo, issue_number }; + + // One fetch serves both the claim record and the reminder markers. + const comments = await github.paginate(github.rest.issues.listComments, { + owner, repo, issue_number, per_page: 100, + }); + const statusComment = claims.pickStatusComment(comments); + const claim = claims.readClaim(statusComment); + if (!claim || claim.state !== 'active') { + core.warning(`#${issue_number}: labelled '${claims.CLAIM_LABEL}' with no active claim; clearing the label.`); + await claims.releaseClaim(github, core, target, null); + continue; + } + + const hoursLeft = (claim.until - now) / claims.HOUR_MS; + + if (now < claim.until) { + // Smallest reminder that is both due and shorter than the window: + // if a scheduled run is skipped and we come back with 20h left, + // that sends the 24h reminder rather than a stale 48h one. + const due = claims.REMINDERS_HOURS.find(hours => + hours * claims.HOUR_MS < claim.until - claim.claimedAt && hoursLeft <= hours); + if (due === undefined) { + core.info(`#${issue_number}: ${claim.claimant} has ${hoursLeft.toFixed(1)}h left, no reminder due.`); + continue; + } + if (await claims.hasReviewedSince(github, target, claim.claimant, claim.claimedAt)) { + core.info(`#${issue_number}: ${claim.claimant} has already reviewed, skipping the ${due}h reminder.`); + continue; + } + + // Keyed to the deadline, so the hourly runs in between do not + // repeat a reminder and an extension earns a fresh set. + const marker = ``; + if (comments.some(comment => comment.body && comment.body.includes(marker))) { + core.info(`#${issue_number}: ${due}h reminder for ${claim.claimant} already posted.`); + continue; + } + + core.info(`#${issue_number}: posting the ${due}h reminder for ${claim.claimant}.`); + await github.rest.issues.createComment({ + owner, repo, issue_number, + body: [ + marker, + `@${claim.claimant} about ${due} hours are left on your review claim for this PR,` + + ` which runs out at ${claims.formatUTC(claim.until)}.`, + '', + 'Reviewing it before then completes the claim. Comment `claim` to give yourself', + 'more time, or `disclaim` to hand it back to the review queue.', + ].join('\n'), + }); + continue; + } + + const reviewed = await claims.hasReviewedSince(github, target, claim.claimant, claim.claimedAt); + core.info(`#${issue_number}: claim by ${claim.claimant} ran out; reviewed=${reviewed}.`); + + if (reviewed) { + // The label goes, but the assignee stays: they did the work. + await claims.releaseClaim(github, core, target, null); + await claims.writeStatus(github, target, { ...claim, state: 'completed' }, statusComment); + continue; + } + + await claims.releaseClaim(github, core, target, claim.claimant); + await claims.writeStatus(github, target, { ...claim, state: 'expired' }, statusComment); + // The status comment is edited rather than reposted, which notifies + // nobody, so the release itself gets its own @-mention. + await github.rest.issues.createComment({ + owner, repo, issue_number, + body: [ + `@${claim.claimant} your review claim on this PR ran out at ` + + `${claims.formatUTC(claim.until)} without a review, so I have removed you as a`, + 'reviewer and assignee.', + '', + 'This PR is back in the general review queue. Comment `claim` if you would still', + 'like to take it.', + ].join('\n'), + }); + + // Zulip only hears about the failures: a claim that was honoured is + // not news, and the point of announcing this one is that the PR now + // needs somebody else. GitHub logins are not Zulip names, so the + // claimant is named rather than @-mentioned. + await claims.notifyZulip(core, [ + `**Review claim expired** on [${repo}#${issue_number}](${issue.html_url}): ${issue.title}`, + '', + `\`${claim.claimant}\` claimed this review until ${claims.formatUTC(claim.until)}, 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`.', + ].join('\n')); + } diff --git a/docs/ReviewGuidelines.md b/docs/ReviewGuidelines.md index e1941f0ce9..b27f340336 100644 --- a/docs/ReviewGuidelines.md +++ b/docs/ReviewGuidelines.md @@ -84,3 +84,38 @@ 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 avoid two reviewers (human or AI) reviewing the same PR, say what you intend to review +and claim it. This is powered by the review claim workflows in `.github/workflows` and the +`review-claimed` label. + +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`; bare `claim` uses the default of 2 days. Claiming needs no + repository permissions, so the review request is best-effort -- GitHub does not let + non-collaborators be requested as reviewers. +2. **You are reminded.** The bot @-mentions you 48 hours and then 24 hours before the + deadline. A reminder that is not shorter than the window you asked for is skipped, so a + one-day claim is never warned about a day in advance. +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 saying + the PR needs somebody else. Only failures are announced -- a claim you honour, extend or + `disclaim` is nobody else's business. + +A claim is cooperative, not a hard lock: it signals intent so that others can steer around +you, and anyone remains free to review a claimed PR. What the bot will not do is silently +overwrite someone else's live claim -- a second `claim` is answered with who holds it and +until when. The claimant can always `disclaim`, and maintainers can release a claim held by +someone else without waiting for it to time out. + +The Zulip announcement uses the `ZULIP_SITE`, `ZULIP_BOT_EMAIL`, `ZULIP_BOT_API_KEY` and +`ZULIP_STREAM` repository secrets, the same bot credentials as the workers in +[PhysLibBots](https://github.com/Alex-Zughaid/PhysLibBots). If they are missing the claim +still expires on GitHub and only the announcement is skipped. From 012ad627f6a0deaf93ed10867a42d2674d5c2944 Mon Sep 17 00:00:00 2001 From: Alex-Zughaid <117576511+Alex-Zughaid@users.noreply.github.com> Date: Tue, 1 Sep 2026 12:46:54 +0100 Subject: [PATCH 2/4] feat(ci): review claims, modelled on the intentions bot 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 --- .github/scripts/review-claim.js | 286 ++++++++++++++++++++++ .github/workflows/review_claim.yml | 200 +++++++++++++++ .github/workflows/review_claim_expiry.yml | 158 ++++++++++++ docs/ReviewGuidelines.md | 35 +++ 4 files changed, 679 insertions(+) create mode 100644 .github/scripts/review-claim.js create mode 100644 .github/workflows/review_claim.yml create mode 100644 .github/workflows/review_claim_expiry.yml diff --git a/.github/scripts/review-claim.js b/.github/scripts/review-claim.js new file mode 100644 index 0000000000..aed4b47159 --- /dev/null +++ b/.github/scripts/review-claim.js @@ -0,0 +1,286 @@ +// Shared helpers for the review claim workflows. +// +// A claim is a promise to review a PR within a window: a reviewer comments +// `claim` (optionally with a window) and the bot records that promise, reminds +// them as the deadline approaches and releases the claim if it goes stale. +// +// The whole state of a claim lives in one bot-maintained comment per PR, in a +// hidden marker holding a JSON record. That comment is edited in place rather +// than reposted, so a PR accumulates at most one claim status comment however +// many times the claim is extended, and there is nothing to keep in sync +// anywhere else. +// +// Used by `.github/workflows/review_claim.yml` (commands) and +// `.github/workflows/review_claim_expiry.yml` (reminders and expiry). + +const CLAIM_LABEL = 'review-claimed'; +const MARKER_PREFIX = ''; + +const HOUR_MS = 60 * 60 * 1000; +const DAY_MS = 24 * HOUR_MS; + +// A review claim is a short promise, so the windows are much tighter than the +// roadmap intentions this is modelled on. +const DEFAULT_WINDOW_MS = 2 * DAY_MS; +const MAX_WINDOW_MS = 14 * DAY_MS; +const MIN_WINDOW_MS = 1 * HOUR_MS; + +// Reminders are @-mentions sent this many hours before the deadline. A +// reminder is skipped when it is not shorter than the window itself, so a +// 24 hour claim is never warned about 24 hours before it ends. Ascending, so +// that the smallest applicable reminder wins if a scheduled run is skipped. +const REMINDERS_HOURS = [24, 48]; + +const UNITS = { + hour: HOUR_MS, hours: HOUR_MS, + day: DAY_MS, days: DAY_MS, + week: 7 * DAY_MS, weeks: 7 * DAY_MS, +}; + +/** Format a timestamp the way the bot's comments always spell one out. */ +const formatUTC = when => new Date(when).toISOString().replace('T', ' ').slice(0, 16) + ' UTC'; + +/** Spell a duration back to the claimant, so they can check what was understood. */ +function describeWindow(ms) { + const round = value => Number(value.toFixed(1)).toString(); + if (ms % DAY_MS === 0 && ms >= DAY_MS) { + const days = ms / DAY_MS; + return days % 7 === 0 + ? `${round(days / 7)} week${days === 7 ? '' : 's'}` + : `${round(days)} day${days === 1 ? '' : 's'}`; + } + const hours = ms / HOUR_MS; + return `${round(hours)} hour${hours === 1 ? '' : 's'}`; +} + +/** + * Parse the argument of a `claim` command into a deadline. + * + * Accepts an empty argument (the default window), ` hours|days|weeks`, or an + * absolute `YYYY-MM-DD` date, which is read as the end of that day UTC. Over-long + * windows are clamped rather than rejected, and the caller is told via `clamped`. + */ +function parseWindow(argument, now) { + const trimmed = (argument || '').trim().toLowerCase(); + + let until; + if (trimmed === '') { + until = now + DEFAULT_WINDOW_MS; + } else if (/^\d{4}-\d{2}-\d{2}$/.test(trimmed)) { + until = Date.parse(`${trimmed}T23:59:59Z`); + if (Number.isNaN(until)) return { error: `\`${trimmed}\` is not a real date.` }; + } else { + const match = trimmed.match(/^(\d+)\s*(hour|hours|day|days|week|weeks)$/); + if (!match) { + return { + error: `I could not read \`${trimmed}\` as a window. Use \`claim\`, ` + + '`claim 5 days` (or hours/weeks), or `claim 2026-08-01`.', + }; + } + until = now + Number(match[1]) * UNITS[match[2]]; + } + + if (until - now < MIN_WINDOW_MS) { + return { error: 'That window is already over. Pick a deadline in the future.' }; + } + const clamped = until - now > MAX_WINDOW_MS; + if (clamped) until = now + MAX_WINDOW_MS; + return { until, clamped }; +} + +/** + * Read a command out of a comment body. + * + * As elsewhere in this repository, a command is a whole line: the bot reacts to + * a line whose entire content, up to whitespace, is the command, so that a + * comment merely discussing claims does not trigger one. The last command in a + * comment wins. + */ +function parseCommand(body) { + const lines = (body || '').replace(/\r/g, '').split('\n'); + let command = null; + for (const line of lines) { + const trimmed = line.trim(); + const claim = trimmed.match(/^claim\b(.*)$/i); + if (claim) command = { name: 'claim', argument: claim[1] }; + else if (/^disclaim$/i.test(trimmed)) command = { name: 'disclaim' }; + } + return command; +} + +/** The status comment among an already-fetched list, or null if there is none. */ +function pickStatusComment(comments) { + return [...comments].reverse() + .find(comment => comment.body && comment.body.includes(MARKER_PREFIX)) || null; +} + +/** The bot's status comment for this PR, or null if it has never claimed one. */ +async function findStatusComment(github, { owner, repo, issue_number }) { + const comments = await github.paginate(github.rest.issues.listComments, { + owner, repo, issue_number, per_page: 100, + }); + return pickStatusComment(comments); +} + +/** The claim record carried by a status comment, or null if it is unreadable. */ +function readClaim(comment) { + if (!comment || !comment.body) return null; + const start = comment.body.indexOf(MARKER_PREFIX); + if (start === -1) return null; + const end = comment.body.indexOf(MARKER_SUFFIX, start); + if (end === -1) return null; + const json = comment.body.slice(start + MARKER_PREFIX.length, end); + try { + return JSON.parse(json); + } catch (error) { + return null; + } +} + +/** Render the status comment body for a claim record. */ +function renderStatus(claim) { + const marker = MARKER_PREFIX + JSON.stringify(claim) + MARKER_SUFFIX; + + if (claim.state === 'released') { + return [marker, `Review claim by @${claim.claimant} released. This PR is back in the review queue.`].join('\n'); + } + if (claim.state === 'completed') { + return [marker, `Review claim by @${claim.claimant} completed — thanks for the review.`].join('\n'); + } + if (claim.state === 'expired') { + return [ + marker, + `Review claim by @${claim.claimant} expired on ${formatUTC(claim.until)} without a review.`, + 'This PR is back in the review queue.', + ].join('\n'); + } + + const window = describeWindow(claim.until - claim.claimedAt); + const reminders = REMINDERS_HOURS + .filter(hours => hours * HOUR_MS < claim.until - claim.claimedAt) + .sort((a, b) => b - a); + + return [ + marker, + `**@${claim.claimant} has claimed this PR for review** until ${formatUTC(claim.until)} (${window}).`, + '', + reminders.length + ? `I will remind them here ${reminders.map(h => `${h}h`).join(' and ')} before that runs out.` + : 'That window is too short for a reminder, so there will not be one.', + 'If no review lands in time the claim is released automatically and this PR returns to', + 'the review queue.', + '', + 'Comment `claim` to extend, `claim 5 days` / `claim 2026-08-01` for a specific window, or', + '`disclaim` to release it early. A claim is cooperative, not a lock: it signals intent so', + 'that others can steer around it, and anyone is still free to review this PR.', + ].join('\n'); +} + +/** Create or edit the single status comment carrying the claim record. */ +async function writeStatus(github, { owner, repo, issue_number }, claim, existing) { + const body = renderStatus(claim); + if (existing) { + await github.rest.issues.updateComment({ owner, repo, comment_id: existing.id, body }); + return existing; + } + const { data } = await github.rest.issues.createComment({ owner, repo, issue_number, body }); + return data; +} + +/** + * Has the claimant looked at the PR since claiming it? A submitted review or an + * inline review comment both count; a plain issue comment deliberately does not. + */ +async function hasReviewedSince(github, { owner, repo, issue_number }, claimant, since) { + const reviews = await github.paginate(github.rest.pulls.listReviews, { + owner, repo, pull_number: issue_number, per_page: 100, + }); + if (reviews.some(review => + review.user.login === claimant && Date.parse(review.submitted_at) >= since)) return true; + + const reviewComments = await github.paginate(github.rest.pulls.listReviewComments, { + owner, repo, pull_number: issue_number, per_page: 100, + }); + return reviewComments.some(comment => + comment.user.login === claimant && Date.parse(comment.created_at) >= since); +} + +/** + * Put the claimant on the PR as both assignee and requested reviewer. + * + * Requesting a review is the half that shows up in everyone's review queue, but + * GitHub refuses it for a non-collaborator and for the PR's own author, and + * claiming deliberately needs no permissions -- so that half is best-effort. + */ +async function takeClaim(github, core, { owner, repo, issue_number }, claimant) { + await github.rest.issues.addLabels({ owner, repo, issue_number, labels: [CLAIM_LABEL] }) + .catch(error => core.warning(`#${issue_number}: could not label: ${error.message}`)); + await github.rest.issues.addAssignees({ owner, repo, issue_number, assignees: [claimant] }) + .catch(error => core.warning(`#${issue_number}: could not assign '${claimant}': ${error.message}`)); + await github.rest.pulls.requestReviewers({ owner, repo, pull_number: issue_number, reviewers: [claimant] }) + .catch(error => core.warning(`#${issue_number}: could not request review from '${claimant}': ${error.message}`)); +} + +/** + * Drop the claim label and, when a claimant is given, take them back off the PR + * as reviewer and assignee. Every step tolerates its target being gone already. + */ +async function releaseClaim(github, core, { owner, repo, issue_number }, claimant) { + await github.rest.issues.removeLabel({ owner, repo, issue_number, name: CLAIM_LABEL }) + .catch(error => core.warning(`#${issue_number}: could not remove '${CLAIM_LABEL}': ${error.message}`)); + if (!claimant) return; + await github.rest.issues.removeAssignees({ owner, repo, issue_number, assignees: [claimant] }) + .catch(error => core.warning(`#${issue_number}: could not unassign '${claimant}': ${error.message}`)); + await github.rest.pulls.removeRequestedReviewers({ owner, repo, pull_number: issue_number, reviewers: [claimant] }) + .catch(error => core.warning(`#${issue_number}: could not drop the review request for '${claimant}': ${error.message}`)); +} + +/** + * Announce something on Zulip, using the same bot credentials and message API as + * the workers in Alex-Zughaid/PhysLibBots. + * + * A missing or broken Zulip setup must never take a workflow down with it: the + * GitHub side of an expiry has already happened by the time this is called, so a + * failure here is warned about and swallowed. + */ +async function notifyZulip(core, content) { + const { ZULIP_SITE, ZULIP_BOT_EMAIL, ZULIP_BOT_API_KEY, ZULIP_STREAM, ZULIP_TOPIC } = process.env; + if (!ZULIP_SITE || !ZULIP_BOT_EMAIL || !ZULIP_BOT_API_KEY || !ZULIP_STREAM) { + core.warning('Zulip is not configured (ZULIP_SITE / ZULIP_BOT_EMAIL / ZULIP_BOT_API_KEY / ZULIP_STREAM), skipping the announcement.'); + return false; + } + + // `to` takes a stream name or a stream id, so ZULIP_STREAM can be either. + const body = new URLSearchParams({ + type: 'stream', to: ZULIP_STREAM, topic: ZULIP_TOPIC || 'PR reviews', content, + }); + const credentials = Buffer.from(`${ZULIP_BOT_EMAIL}:${ZULIP_BOT_API_KEY}`).toString('base64'); + + try { + const response = await fetch(`${ZULIP_SITE.replace(/\/$/, '')}/api/v1/messages`, { + method: 'POST', + headers: { + Authorization: `Basic ${credentials}`, + 'Content-Type': 'application/x-www-form-urlencoded', + }, + body, + }); + if (!response.ok) { + core.warning(`Zulip API error: ${response.status} ${await response.text()}`); + return false; + } + return true; + } catch (error) { + core.warning(`Could not reach Zulip: ${error.message}`); + return false; + } +} + +module.exports = { + CLAIM_LABEL, HOUR_MS, DAY_MS, REMINDERS_HOURS, + DEFAULT_WINDOW_MS, MAX_WINDOW_MS, + formatUTC, describeWindow, parseWindow, parseCommand, + pickStatusComment, findStatusComment, readClaim, renderStatus, writeStatus, + hasReviewedSince, takeClaim, releaseClaim, notifyZulip, +}; diff --git a/.github/workflows/review_claim.yml b/.github/workflows/review_claim.yml new file mode 100644 index 0000000000..2d6420cf10 --- /dev/null +++ b/.github/workflows/review_claim.yml @@ -0,0 +1,200 @@ +# 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. + +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 helpers + uses: actions/checkout@v7.0.0 + with: + sparse-checkout: .github/scripts + persist-credentials: false + - name: Claim or disclaim + uses: actions/github-script@v7 + with: + script: | + const claims = require(`${process.env.GITHUB_WORKSPACE}/.github/scripts/review-claim.js`); + const { owner, repo } = context.repo; + const issue_number = context.payload.issue.number; + const target = { owner, repo, issue_number }; + const actor = context.payload.comment.user.login; + const commentId = context.payload.comment.id; + const now = Date.now(); + + const command = claims.parseCommand(context.payload.comment.body); + if (!command) { + core.info('No claim command in this comment.'); + return; + } + + const react = content => github.rest.reactions.createForIssueComment({ + owner, repo, comment_id: commentId, content, + }).catch(error => core.warning(`Could not react: ${error.message}`)); + + const reject = async message => { + await react('confused'); + await github.rest.issues.createComment({ + owner, repo, issue_number, body: `@${actor} ${message}`, + }); + }; + + const statusComment = await claims.findStatusComment(github, target); + const current = claims.readClaim(statusComment); + const active = current && current.state === 'active' ? current : null; + + if (command.name === 'disclaim') { + if (!active) { + core.info(`#${issue_number}: nothing to disclaim.`); + await react('confused'); + return; + } + // The claimant can always let go; a maintainer can release someone + // else's claim without waiting for it to time out. + let permitted = active.claimant === actor; + if (!permitted) { + const { data: access } = await github.rest.repos.getCollaboratorPermissionLevel({ + owner, repo, username: actor, + }).catch(() => ({ data: { permission: 'none' } })); + permitted = ['admin', 'maintain', 'write'].includes(access.permission); + } + if (!permitted) { + await reject( + `this PR is claimed by @${active.claimant} until ${claims.formatUTC(active.until)}, ` + + 'and only they (or a maintainer) can release it. It will be released ' + + 'automatically if no review arrives by then.'); + return; + } + + core.info(`#${issue_number}: ${actor} released the claim held by ${active.claimant}.`); + await claims.releaseClaim(github, core, target, active.claimant); + await claims.writeStatus(github, target, + { ...active, state: 'released', releasedBy: actor }, statusComment); + await react('+1'); + return; + } + + // Someone else's live claim is not silently overwritten: the point of + // the whole mechanism is that a second reviewer finds out before + // duplicating the work. + if (active && active.claimant !== actor) { + await reject( + `this PR is already claimed by @${active.claimant} until ` + + `${claims.formatUTC(active.until)}. It will be released automatically if no ` + + 'review arrives by then, and you are still free to review it in the meantime ' + + '— a claim signals intent rather than locking anyone out.'); + return; + } + + const window = claims.parseWindow(command.argument, now); + if (window.error) { + await reject(window.error); + return; + } + + const claim = { + state: 'active', + claimant: actor, + // Extending keeps the original claim time, so the status comment + // keeps describing the window the claimant actually asked for. + claimedAt: now, + until: window.until, + }; + + await claims.takeClaim(github, core, target, actor); + await claims.writeStatus(github, target, claim, statusComment); + await react('+1'); + + if (window.clamped) { + await github.rest.issues.createComment({ + owner, repo, issue_number, + body: `@${actor} that window was longer than the ` + + `${claims.describeWindow(claims.MAX_WINDOW_MS)} maximum, so I shortened it to ` + + `${claims.formatUTC(window.until)}. Comment \`claim\` again to extend it later.`, + }); + } + core.info(`#${issue_number}: ${actor} claimed until ${new Date(window.until).toISOString()}.`); + + 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 helpers + uses: actions/checkout@v7.0.0 + with: + sparse-checkout: .github/scripts + persist-credentials: false + - name: Clear the claim once its claimant has reviewed + uses: actions/github-script@v7 + with: + script: | + const claims = require(`${process.env.GITHUB_WORKSPACE}/.github/scripts/review-claim.js`); + const { owner, repo } = context.repo; + const issue_number = context.payload.pull_request.number; + const target = { owner, repo, issue_number }; + const reviewer = context.payload.review.user.login; + + const statusComment = await claims.findStatusComment(github, target); + const current = claims.readClaim(statusComment); + if (!current || current.state !== 'active' || current.claimant !== reviewer) { + core.info(`#${issue_number}: review by ${reviewer} does not close an active claim.`); + return; + } + + core.info(`#${issue_number}: ${reviewer} reviewed, completing their claim.`); + // The label goes, but the assignee stays: they are engaged with this + // PR now, which is the opposite of the case the expiry job handles. + await claims.releaseClaim(github, core, target, null); + await claims.writeStatus(github, target, + { ...current, state: 'completed' }, statusComment); diff --git a/.github/workflows/review_claim_expiry.yml b/.github/workflows/review_claim_expiry.yml new file mode 100644 index 0000000000..559fa070a7 --- /dev/null +++ b/.github/workflows/review_claim_expiry.yml @@ -0,0 +1,158 @@ +# 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 the assignee +# and saying so -- putting the PR back into the general review queue. +# +# 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. + +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 helpers + uses: actions/checkout@v7.0.0 + with: + sparse-checkout: .github/scripts + persist-credentials: false + - name: Remind and expire + uses: actions/github-script@v7 + env: + # Same bot credentials as the workers in Alex-Zughaid/PhysLibBots. + # 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 + with: + script: | + const claims = require(`${process.env.GITHUB_WORKSPACE}/.github/scripts/review-claim.js`); + const { owner, repo } = context.repo; + const now = Date.now(); + + const issues = await github.paginate(github.rest.issues.listForRepo, { + owner, repo, state: 'open', labels: claims.CLAIM_LABEL, per_page: 100, + }); + + for (const issue of issues) { + // `listForRepo` returns issues and PRs alike; we only want PRs. + if (!issue.pull_request) continue; + const issue_number = issue.number; + const target = { owner, repo, issue_number }; + + // One fetch serves both the claim record and the reminder markers. + const comments = await github.paginate(github.rest.issues.listComments, { + owner, repo, issue_number, per_page: 100, + }); + const statusComment = claims.pickStatusComment(comments); + const claim = claims.readClaim(statusComment); + if (!claim || claim.state !== 'active') { + core.warning(`#${issue_number}: labelled '${claims.CLAIM_LABEL}' with no active claim; clearing the label.`); + await claims.releaseClaim(github, core, target, null); + continue; + } + + const hoursLeft = (claim.until - now) / claims.HOUR_MS; + + if (now < claim.until) { + // Smallest reminder that is both due and shorter than the window: + // if a scheduled run is skipped and we come back with 20h left, + // that sends the 24h reminder rather than a stale 48h one. + const due = claims.REMINDERS_HOURS.find(hours => + hours * claims.HOUR_MS < claim.until - claim.claimedAt && hoursLeft <= hours); + if (due === undefined) { + core.info(`#${issue_number}: ${claim.claimant} has ${hoursLeft.toFixed(1)}h left, no reminder due.`); + continue; + } + if (await claims.hasReviewedSince(github, target, claim.claimant, claim.claimedAt)) { + core.info(`#${issue_number}: ${claim.claimant} has already reviewed, skipping the ${due}h reminder.`); + continue; + } + + // Keyed to the deadline, so the hourly runs in between do not + // repeat a reminder and an extension earns a fresh set. + const marker = ``; + if (comments.some(comment => comment.body && comment.body.includes(marker))) { + core.info(`#${issue_number}: ${due}h reminder for ${claim.claimant} already posted.`); + continue; + } + + core.info(`#${issue_number}: posting the ${due}h reminder for ${claim.claimant}.`); + await github.rest.issues.createComment({ + owner, repo, issue_number, + body: [ + marker, + `@${claim.claimant} about ${due} hours are left on your review claim for this PR,` + + ` which runs out at ${claims.formatUTC(claim.until)}.`, + '', + 'Reviewing it before then completes the claim. Comment `claim` to give yourself', + 'more time, or `disclaim` to hand it back to the review queue.', + ].join('\n'), + }); + continue; + } + + const reviewed = await claims.hasReviewedSince(github, target, claim.claimant, claim.claimedAt); + core.info(`#${issue_number}: claim by ${claim.claimant} ran out; reviewed=${reviewed}.`); + + if (reviewed) { + // The label goes, but the assignee stays: they did the work. + await claims.releaseClaim(github, core, target, null); + await claims.writeStatus(github, target, { ...claim, state: 'completed' }, statusComment); + continue; + } + + await claims.releaseClaim(github, core, target, claim.claimant); + await claims.writeStatus(github, target, { ...claim, state: 'expired' }, statusComment); + // The status comment is edited rather than reposted, which notifies + // nobody, so the release itself gets its own @-mention. + await github.rest.issues.createComment({ + owner, repo, issue_number, + body: [ + `@${claim.claimant} your review claim on this PR ran out at ` + + `${claims.formatUTC(claim.until)} without a review, so I have removed you as a`, + 'reviewer and assignee.', + '', + 'This PR is back in the general review queue. Comment `claim` if you would still', + 'like to take it.', + ].join('\n'), + }); + + // Zulip only hears about the failures: a claim that was honoured is + // not news, and the point of announcing this one is that the PR now + // needs somebody else. GitHub logins are not Zulip names, so the + // claimant is named rather than @-mentioned. + await claims.notifyZulip(core, [ + `**Review claim expired** on [${repo}#${issue_number}](${issue.html_url}): ${issue.title}`, + '', + `\`${claim.claimant}\` claimed this review until ${claims.formatUTC(claim.until)}, 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`.', + ].join('\n')); + } diff --git a/docs/ReviewGuidelines.md b/docs/ReviewGuidelines.md index e1941f0ce9..b27f340336 100644 --- a/docs/ReviewGuidelines.md +++ b/docs/ReviewGuidelines.md @@ -84,3 +84,38 @@ 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 avoid two reviewers (human or AI) reviewing the same PR, say what you intend to review +and claim it. This is powered by the review claim workflows in `.github/workflows` and the +`review-claimed` label. + +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`; bare `claim` uses the default of 2 days. Claiming needs no + repository permissions, so the review request is best-effort -- GitHub does not let + non-collaborators be requested as reviewers. +2. **You are reminded.** The bot @-mentions you 48 hours and then 24 hours before the + deadline. A reminder that is not shorter than the window you asked for is skipped, so a + one-day claim is never warned about a day in advance. +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 saying + the PR needs somebody else. Only failures are announced -- a claim you honour, extend or + `disclaim` is nobody else's business. + +A claim is cooperative, not a hard lock: it signals intent so that others can steer around +you, and anyone remains free to review a claimed PR. What the bot will not do is silently +overwrite someone else's live claim -- a second `claim` is answered with who holds it and +until when. The claimant can always `disclaim`, and maintainers can release a claim held by +someone else without waiting for it to time out. + +The Zulip announcement uses the `ZULIP_SITE`, `ZULIP_BOT_EMAIL`, `ZULIP_BOT_API_KEY` and +`ZULIP_STREAM` repository secrets, the same bot credentials as the workers in +[PhysLibBots](https://github.com/Alex-Zughaid/PhysLibBots). If they are missing the claim +still expires on GitHub and only the announcement is skipped. From 872d7d6c137147a0659da2c1f2cef4a75acefcb9 Mon Sep 17 00:00:00 2001 From: Alex-Zughaid <117576511+Alex-Zughaid@users.noreply.github.com> Date: Wed, 2 Sep 2026 10:09:13 +0100 Subject: [PATCH 3/4] Update ReviewGuidelines.md --- docs/ReviewGuidelines.md | 26 ++++---------------------- 1 file changed, 4 insertions(+), 22 deletions(-) diff --git a/docs/ReviewGuidelines.md b/docs/ReviewGuidelines.md index b27f340336..469f25773c 100644 --- a/docs/ReviewGuidelines.md +++ b/docs/ReviewGuidelines.md @@ -87,35 +87,17 @@ understand where in the process PRs are. ## Claiming a PR for review -To avoid two reviewers (human or AI) reviewing the same PR, say what you intend to review -and claim it. This is powered by the review claim workflows in `.github/workflows` and the -`review-claimed` label. +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`; bare `claim` uses the default of 2 days. Claiming needs no - repository permissions, so the review request is best-effort -- GitHub does not let - non-collaborators be requested as reviewers. + 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. A reminder that is not shorter than the window you asked for is skipped, so a - one-day claim is never warned about a day in advance. + 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 saying - the PR needs somebody else. Only failures are announced -- a claim you honour, extend or - `disclaim` is nobody else's business. - -A claim is cooperative, not a hard lock: it signals intent so that others can steer around -you, and anyone remains free to review a claimed PR. What the bot will not do is silently -overwrite someone else's live claim -- a second `claim` is answered with who holds it and -until when. The claimant can always `disclaim`, and maintainers can release a claim held by -someone else without waiting for it to time out. - -The Zulip announcement uses the `ZULIP_SITE`, `ZULIP_BOT_EMAIL`, `ZULIP_BOT_API_KEY` and -`ZULIP_STREAM` repository secrets, the same bot credentials as the workers in -[PhysLibBots](https://github.com/Alex-Zughaid/PhysLibBots). If they are missing the claim -still expires on GitHub and only the announcement is skipped. + as reviewer and assignee, and a message goes to the `PR reviews` topic on Zulip. From dad2ba3182bb54814359f635777c43b2cdfde49d Mon Sep 17 00:00:00 2001 From: Alex-Zughaid <117576511+Alex-Zughaid@users.noreply.github.com> Date: Wed, 2 Sep 2026 16:51:34 +0100 Subject: [PATCH 4/4] refactor(ci): move the review claim logic to scripts/review_claim.py 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 --- .github/scripts/review-claim.js | 286 ---------- .github/workflows/review_claim.yml | 148 +---- .github/workflows/review_claim_expiry.yml | 133 +---- scripts/review_claim.py | 633 ++++++++++++++++++++++ 4 files changed, 666 insertions(+), 534 deletions(-) delete mode 100644 .github/scripts/review-claim.js create mode 100644 scripts/review_claim.py diff --git a/.github/scripts/review-claim.js b/.github/scripts/review-claim.js deleted file mode 100644 index aed4b47159..0000000000 --- a/.github/scripts/review-claim.js +++ /dev/null @@ -1,286 +0,0 @@ -// Shared helpers for the review claim workflows. -// -// A claim is a promise to review a PR within a window: a reviewer comments -// `claim` (optionally with a window) and the bot records that promise, reminds -// them as the deadline approaches and releases the claim if it goes stale. -// -// The whole state of a claim lives in one bot-maintained comment per PR, in a -// hidden marker holding a JSON record. That comment is edited in place rather -// than reposted, so a PR accumulates at most one claim status comment however -// many times the claim is extended, and there is nothing to keep in sync -// anywhere else. -// -// Used by `.github/workflows/review_claim.yml` (commands) and -// `.github/workflows/review_claim_expiry.yml` (reminders and expiry). - -const CLAIM_LABEL = 'review-claimed'; -const MARKER_PREFIX = ''; - -const HOUR_MS = 60 * 60 * 1000; -const DAY_MS = 24 * HOUR_MS; - -// A review claim is a short promise, so the windows are much tighter than the -// roadmap intentions this is modelled on. -const DEFAULT_WINDOW_MS = 2 * DAY_MS; -const MAX_WINDOW_MS = 14 * DAY_MS; -const MIN_WINDOW_MS = 1 * HOUR_MS; - -// Reminders are @-mentions sent this many hours before the deadline. A -// reminder is skipped when it is not shorter than the window itself, so a -// 24 hour claim is never warned about 24 hours before it ends. Ascending, so -// that the smallest applicable reminder wins if a scheduled run is skipped. -const REMINDERS_HOURS = [24, 48]; - -const UNITS = { - hour: HOUR_MS, hours: HOUR_MS, - day: DAY_MS, days: DAY_MS, - week: 7 * DAY_MS, weeks: 7 * DAY_MS, -}; - -/** Format a timestamp the way the bot's comments always spell one out. */ -const formatUTC = when => new Date(when).toISOString().replace('T', ' ').slice(0, 16) + ' UTC'; - -/** Spell a duration back to the claimant, so they can check what was understood. */ -function describeWindow(ms) { - const round = value => Number(value.toFixed(1)).toString(); - if (ms % DAY_MS === 0 && ms >= DAY_MS) { - const days = ms / DAY_MS; - return days % 7 === 0 - ? `${round(days / 7)} week${days === 7 ? '' : 's'}` - : `${round(days)} day${days === 1 ? '' : 's'}`; - } - const hours = ms / HOUR_MS; - return `${round(hours)} hour${hours === 1 ? '' : 's'}`; -} - -/** - * Parse the argument of a `claim` command into a deadline. - * - * Accepts an empty argument (the default window), ` hours|days|weeks`, or an - * absolute `YYYY-MM-DD` date, which is read as the end of that day UTC. Over-long - * windows are clamped rather than rejected, and the caller is told via `clamped`. - */ -function parseWindow(argument, now) { - const trimmed = (argument || '').trim().toLowerCase(); - - let until; - if (trimmed === '') { - until = now + DEFAULT_WINDOW_MS; - } else if (/^\d{4}-\d{2}-\d{2}$/.test(trimmed)) { - until = Date.parse(`${trimmed}T23:59:59Z`); - if (Number.isNaN(until)) return { error: `\`${trimmed}\` is not a real date.` }; - } else { - const match = trimmed.match(/^(\d+)\s*(hour|hours|day|days|week|weeks)$/); - if (!match) { - return { - error: `I could not read \`${trimmed}\` as a window. Use \`claim\`, ` + - '`claim 5 days` (or hours/weeks), or `claim 2026-08-01`.', - }; - } - until = now + Number(match[1]) * UNITS[match[2]]; - } - - if (until - now < MIN_WINDOW_MS) { - return { error: 'That window is already over. Pick a deadline in the future.' }; - } - const clamped = until - now > MAX_WINDOW_MS; - if (clamped) until = now + MAX_WINDOW_MS; - return { until, clamped }; -} - -/** - * Read a command out of a comment body. - * - * As elsewhere in this repository, a command is a whole line: the bot reacts to - * a line whose entire content, up to whitespace, is the command, so that a - * comment merely discussing claims does not trigger one. The last command in a - * comment wins. - */ -function parseCommand(body) { - const lines = (body || '').replace(/\r/g, '').split('\n'); - let command = null; - for (const line of lines) { - const trimmed = line.trim(); - const claim = trimmed.match(/^claim\b(.*)$/i); - if (claim) command = { name: 'claim', argument: claim[1] }; - else if (/^disclaim$/i.test(trimmed)) command = { name: 'disclaim' }; - } - return command; -} - -/** The status comment among an already-fetched list, or null if there is none. */ -function pickStatusComment(comments) { - return [...comments].reverse() - .find(comment => comment.body && comment.body.includes(MARKER_PREFIX)) || null; -} - -/** The bot's status comment for this PR, or null if it has never claimed one. */ -async function findStatusComment(github, { owner, repo, issue_number }) { - const comments = await github.paginate(github.rest.issues.listComments, { - owner, repo, issue_number, per_page: 100, - }); - return pickStatusComment(comments); -} - -/** The claim record carried by a status comment, or null if it is unreadable. */ -function readClaim(comment) { - if (!comment || !comment.body) return null; - const start = comment.body.indexOf(MARKER_PREFIX); - if (start === -1) return null; - const end = comment.body.indexOf(MARKER_SUFFIX, start); - if (end === -1) return null; - const json = comment.body.slice(start + MARKER_PREFIX.length, end); - try { - return JSON.parse(json); - } catch (error) { - return null; - } -} - -/** Render the status comment body for a claim record. */ -function renderStatus(claim) { - const marker = MARKER_PREFIX + JSON.stringify(claim) + MARKER_SUFFIX; - - if (claim.state === 'released') { - return [marker, `Review claim by @${claim.claimant} released. This PR is back in the review queue.`].join('\n'); - } - if (claim.state === 'completed') { - return [marker, `Review claim by @${claim.claimant} completed — thanks for the review.`].join('\n'); - } - if (claim.state === 'expired') { - return [ - marker, - `Review claim by @${claim.claimant} expired on ${formatUTC(claim.until)} without a review.`, - 'This PR is back in the review queue.', - ].join('\n'); - } - - const window = describeWindow(claim.until - claim.claimedAt); - const reminders = REMINDERS_HOURS - .filter(hours => hours * HOUR_MS < claim.until - claim.claimedAt) - .sort((a, b) => b - a); - - return [ - marker, - `**@${claim.claimant} has claimed this PR for review** until ${formatUTC(claim.until)} (${window}).`, - '', - reminders.length - ? `I will remind them here ${reminders.map(h => `${h}h`).join(' and ')} before that runs out.` - : 'That window is too short for a reminder, so there will not be one.', - 'If no review lands in time the claim is released automatically and this PR returns to', - 'the review queue.', - '', - 'Comment `claim` to extend, `claim 5 days` / `claim 2026-08-01` for a specific window, or', - '`disclaim` to release it early. A claim is cooperative, not a lock: it signals intent so', - 'that others can steer around it, and anyone is still free to review this PR.', - ].join('\n'); -} - -/** Create or edit the single status comment carrying the claim record. */ -async function writeStatus(github, { owner, repo, issue_number }, claim, existing) { - const body = renderStatus(claim); - if (existing) { - await github.rest.issues.updateComment({ owner, repo, comment_id: existing.id, body }); - return existing; - } - const { data } = await github.rest.issues.createComment({ owner, repo, issue_number, body }); - return data; -} - -/** - * Has the claimant looked at the PR since claiming it? A submitted review or an - * inline review comment both count; a plain issue comment deliberately does not. - */ -async function hasReviewedSince(github, { owner, repo, issue_number }, claimant, since) { - const reviews = await github.paginate(github.rest.pulls.listReviews, { - owner, repo, pull_number: issue_number, per_page: 100, - }); - if (reviews.some(review => - review.user.login === claimant && Date.parse(review.submitted_at) >= since)) return true; - - const reviewComments = await github.paginate(github.rest.pulls.listReviewComments, { - owner, repo, pull_number: issue_number, per_page: 100, - }); - return reviewComments.some(comment => - comment.user.login === claimant && Date.parse(comment.created_at) >= since); -} - -/** - * Put the claimant on the PR as both assignee and requested reviewer. - * - * Requesting a review is the half that shows up in everyone's review queue, but - * GitHub refuses it for a non-collaborator and for the PR's own author, and - * claiming deliberately needs no permissions -- so that half is best-effort. - */ -async function takeClaim(github, core, { owner, repo, issue_number }, claimant) { - await github.rest.issues.addLabels({ owner, repo, issue_number, labels: [CLAIM_LABEL] }) - .catch(error => core.warning(`#${issue_number}: could not label: ${error.message}`)); - await github.rest.issues.addAssignees({ owner, repo, issue_number, assignees: [claimant] }) - .catch(error => core.warning(`#${issue_number}: could not assign '${claimant}': ${error.message}`)); - await github.rest.pulls.requestReviewers({ owner, repo, pull_number: issue_number, reviewers: [claimant] }) - .catch(error => core.warning(`#${issue_number}: could not request review from '${claimant}': ${error.message}`)); -} - -/** - * Drop the claim label and, when a claimant is given, take them back off the PR - * as reviewer and assignee. Every step tolerates its target being gone already. - */ -async function releaseClaim(github, core, { owner, repo, issue_number }, claimant) { - await github.rest.issues.removeLabel({ owner, repo, issue_number, name: CLAIM_LABEL }) - .catch(error => core.warning(`#${issue_number}: could not remove '${CLAIM_LABEL}': ${error.message}`)); - if (!claimant) return; - await github.rest.issues.removeAssignees({ owner, repo, issue_number, assignees: [claimant] }) - .catch(error => core.warning(`#${issue_number}: could not unassign '${claimant}': ${error.message}`)); - await github.rest.pulls.removeRequestedReviewers({ owner, repo, pull_number: issue_number, reviewers: [claimant] }) - .catch(error => core.warning(`#${issue_number}: could not drop the review request for '${claimant}': ${error.message}`)); -} - -/** - * Announce something on Zulip, using the same bot credentials and message API as - * the workers in Alex-Zughaid/PhysLibBots. - * - * A missing or broken Zulip setup must never take a workflow down with it: the - * GitHub side of an expiry has already happened by the time this is called, so a - * failure here is warned about and swallowed. - */ -async function notifyZulip(core, content) { - const { ZULIP_SITE, ZULIP_BOT_EMAIL, ZULIP_BOT_API_KEY, ZULIP_STREAM, ZULIP_TOPIC } = process.env; - if (!ZULIP_SITE || !ZULIP_BOT_EMAIL || !ZULIP_BOT_API_KEY || !ZULIP_STREAM) { - core.warning('Zulip is not configured (ZULIP_SITE / ZULIP_BOT_EMAIL / ZULIP_BOT_API_KEY / ZULIP_STREAM), skipping the announcement.'); - return false; - } - - // `to` takes a stream name or a stream id, so ZULIP_STREAM can be either. - const body = new URLSearchParams({ - type: 'stream', to: ZULIP_STREAM, topic: ZULIP_TOPIC || 'PR reviews', content, - }); - const credentials = Buffer.from(`${ZULIP_BOT_EMAIL}:${ZULIP_BOT_API_KEY}`).toString('base64'); - - try { - const response = await fetch(`${ZULIP_SITE.replace(/\/$/, '')}/api/v1/messages`, { - method: 'POST', - headers: { - Authorization: `Basic ${credentials}`, - 'Content-Type': 'application/x-www-form-urlencoded', - }, - body, - }); - if (!response.ok) { - core.warning(`Zulip API error: ${response.status} ${await response.text()}`); - return false; - } - return true; - } catch (error) { - core.warning(`Could not reach Zulip: ${error.message}`); - return false; - } -} - -module.exports = { - CLAIM_LABEL, HOUR_MS, DAY_MS, REMINDERS_HOURS, - DEFAULT_WINDOW_MS, MAX_WINDOW_MS, - formatUTC, describeWindow, parseWindow, parseCommand, - pickStatusComment, findStatusComment, readClaim, renderStatus, writeStatus, - hasReviewedSince, takeClaim, releaseClaim, notifyZulip, -}; diff --git a/.github/workflows/review_claim.yml b/.github/workflows/review_claim.yml index 9b5d9654ea..aac585c616 100644 --- a/.github/workflows/review_claim.yml +++ b/.github/workflows/review_claim.yml @@ -19,6 +19,8 @@ # 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 @@ -31,8 +33,8 @@ on: # 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 + 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: @@ -43,6 +45,7 @@ jobs: # 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' && @@ -52,115 +55,16 @@ jobs: (contains(github.event.comment.body, 'claim') || contains(github.event.comment.body, 'Claim')) steps: - - name: Check out the claim helpers + - name: Check out the claim script uses: actions/checkout@v7.0.0 with: - sparse-checkout: .github/scripts + sparse-checkout: scripts/review_claim.py + sparse-checkout-cone-mode: false persist-credentials: false - name: Claim or disclaim - uses: actions/github-script@v7 - with: - script: | - const claims = require(`${process.env.GITHUB_WORKSPACE}/.github/scripts/review-claim.js`); - const { owner, repo } = context.repo; - const issue_number = context.payload.issue.number; - const target = { owner, repo, issue_number }; - const actor = context.payload.comment.user.login; - const commentId = context.payload.comment.id; - const now = Date.now(); - - const command = claims.parseCommand(context.payload.comment.body); - if (!command) { - core.info('No claim command in this comment.'); - return; - } - - const react = content => github.rest.reactions.createForIssueComment({ - owner, repo, comment_id: commentId, content, - }).catch(error => core.warning(`Could not react: ${error.message}`)); - - const reject = async message => { - await react('confused'); - await github.rest.issues.createComment({ - owner, repo, issue_number, body: `@${actor} ${message}`, - }); - }; - - const statusComment = await claims.findStatusComment(github, target); - const current = claims.readClaim(statusComment); - const active = current && current.state === 'active' ? current : null; - - if (command.name === 'disclaim') { - if (!active) { - core.info(`#${issue_number}: nothing to disclaim.`); - await react('confused'); - return; - } - // The claimant can always let go; a maintainer can release someone - // else's claim without waiting for it to time out. - let permitted = active.claimant === actor; - if (!permitted) { - const { data: access } = await github.rest.repos.getCollaboratorPermissionLevel({ - owner, repo, username: actor, - }).catch(() => ({ data: { permission: 'none' } })); - permitted = ['admin', 'maintain', 'write'].includes(access.permission); - } - if (!permitted) { - await reject( - `this PR is claimed by @${active.claimant} until ${claims.formatUTC(active.until)}, ` + - 'and only they (or a maintainer) can release it. It will be released ' + - 'automatically if no review arrives by then.'); - return; - } - - core.info(`#${issue_number}: ${actor} released the claim held by ${active.claimant}.`); - await claims.releaseClaim(github, core, target, active.claimant); - await claims.writeStatus(github, target, - { ...active, state: 'released', releasedBy: actor }, statusComment); - await react('+1'); - return; - } - - // Someone else's live claim is not silently overwritten: the point of - // the whole mechanism is that a second reviewer finds out before - // duplicating the work. - if (active && active.claimant !== actor) { - await reject( - `this PR is already claimed by @${active.claimant} until ` + - `${claims.formatUTC(active.until)}. It will be released automatically if no ` + - 'review arrives by then, and you are still free to review it in the meantime ' + - '— a claim signals intent rather than locking anyone out.'); - return; - } - - const window = claims.parseWindow(command.argument, now); - if (window.error) { - await reject(window.error); - return; - } - - const claim = { - state: 'active', - claimant: actor, - // Extending keeps the original claim time, so the status comment - // keeps describing the window the claimant actually asked for. - claimedAt: now, - until: window.until, - }; - - await claims.takeClaim(github, core, target, actor); - await claims.writeStatus(github, target, claim, statusComment); - await react('+1'); - - if (window.clamped) { - await github.rest.issues.createComment({ - owner, repo, issue_number, - body: `@${actor} that window was longer than the ` + - `${claims.describeWindow(claims.MAX_WINDOW_MS)} maximum, so I shortened it to ` + - `${claims.formatUTC(window.until)}. Comment \`claim\` again to extend it later.`, - }); - } - core.info(`#${issue_number}: ${actor} claimed until ${new Date(window.until).toISOString()}.`); + run: python3 scripts/review_claim.py comment + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} complete: name: Complete claim on review @@ -170,31 +74,13 @@ jobs: github.repository == 'leanprover-community/physlib' && github.event_name == 'pull_request_review' steps: - - name: Check out the claim helpers + - name: Check out the claim script uses: actions/checkout@v7.0.0 with: - sparse-checkout: .github/scripts + sparse-checkout: scripts/review_claim.py + sparse-checkout-cone-mode: false persist-credentials: false - name: Clear the claim once its claimant has reviewed - uses: actions/github-script@v7 - with: - script: | - const claims = require(`${process.env.GITHUB_WORKSPACE}/.github/scripts/review-claim.js`); - const { owner, repo } = context.repo; - const issue_number = context.payload.pull_request.number; - const target = { owner, repo, issue_number }; - const reviewer = context.payload.review.user.login; - - const statusComment = await claims.findStatusComment(github, target); - const current = claims.readClaim(statusComment); - if (!current || current.state !== 'active' || current.claimant !== reviewer) { - core.info(`#${issue_number}: review by ${reviewer} does not close an active claim.`); - return; - } - - core.info(`#${issue_number}: ${reviewer} reviewed, completing their claim.`); - // The label goes, but the assignee stays: they are engaged with this - // PR now, which is the opposite of the case the expiry job handles. - await claims.releaseClaim(github, core, target, null); - await claims.writeStatus(github, target, - { ...current, state: 'completed' }, statusComment); + run: python3 scripts/review_claim.py review + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} diff --git a/.github/workflows/review_claim_expiry.yml b/.github/workflows/review_claim_expiry.yml index c34022c6f4..d5fd314047 100644 --- a/.github/workflows/review_claim_expiry.yml +++ b/.github/workflows/review_claim_expiry.yml @@ -6,25 +6,28 @@ # * @-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 the assignee -# and saying so -- putting the PR back into the general review queue. +# 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 * * * *" + - 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 + issues: write # Only allow reading/labelling issues + pull-requests: write # Only allow PR comments/labels/assignees # All other permissions are implicitly 'none' jobs: @@ -34,125 +37,21 @@ jobs: # 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 helpers + - name: Check out the claim script uses: actions/checkout@v7.0.0 with: - sparse-checkout: .github/scripts + sparse-checkout: scripts/review_claim.py + sparse-checkout-cone-mode: false persist-credentials: false - name: Remind and expire - uses: actions/github-script@v7 + run: python3 scripts/review_claim.py expire env: - # Same bot credentials as the workers in Alex-Zughaid/PhysLibBots. - # Missing secrets downgrade to a warning rather than failing the job: - # releasing the claim on GitHub matters more than announcing it. + 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 - with: - script: | - const claims = require(`${process.env.GITHUB_WORKSPACE}/.github/scripts/review-claim.js`); - const { owner, repo } = context.repo; - const now = Date.now(); - - const issues = await github.paginate(github.rest.issues.listForRepo, { - owner, repo, state: 'open', labels: claims.CLAIM_LABEL, per_page: 100, - }); - - for (const issue of issues) { - // `listForRepo` returns issues and PRs alike; we only want PRs. - if (!issue.pull_request) continue; - const issue_number = issue.number; - const target = { owner, repo, issue_number }; - - // One fetch serves both the claim record and the reminder markers. - const comments = await github.paginate(github.rest.issues.listComments, { - owner, repo, issue_number, per_page: 100, - }); - const statusComment = claims.pickStatusComment(comments); - const claim = claims.readClaim(statusComment); - if (!claim || claim.state !== 'active') { - core.warning(`#${issue_number}: labelled '${claims.CLAIM_LABEL}' with no active claim; clearing the label.`); - await claims.releaseClaim(github, core, target, null); - continue; - } - - const hoursLeft = (claim.until - now) / claims.HOUR_MS; - - if (now < claim.until) { - // Smallest reminder that is both due and shorter than the window: - // if a scheduled run is skipped and we come back with 20h left, - // that sends the 24h reminder rather than a stale 48h one. - const due = claims.REMINDERS_HOURS.find(hours => - hours * claims.HOUR_MS < claim.until - claim.claimedAt && hoursLeft <= hours); - if (due === undefined) { - core.info(`#${issue_number}: ${claim.claimant} has ${hoursLeft.toFixed(1)}h left, no reminder due.`); - continue; - } - if (await claims.hasReviewedSince(github, target, claim.claimant, claim.claimedAt)) { - core.info(`#${issue_number}: ${claim.claimant} has already reviewed, skipping the ${due}h reminder.`); - continue; - } - - // Keyed to the deadline, so the hourly runs in between do not - // repeat a reminder and an extension earns a fresh set. - const marker = ``; - if (comments.some(comment => comment.body && comment.body.includes(marker))) { - core.info(`#${issue_number}: ${due}h reminder for ${claim.claimant} already posted.`); - continue; - } - - core.info(`#${issue_number}: posting the ${due}h reminder for ${claim.claimant}.`); - await github.rest.issues.createComment({ - owner, repo, issue_number, - body: [ - marker, - `@${claim.claimant} about ${due} hours are left on your review claim for this PR,` + - ` which runs out at ${claims.formatUTC(claim.until)}.`, - '', - 'Reviewing it before then completes the claim. Comment `claim` to give yourself', - 'more time, or `disclaim` to hand it back to the review queue.', - ].join('\n'), - }); - continue; - } - - const reviewed = await claims.hasReviewedSince(github, target, claim.claimant, claim.claimedAt); - core.info(`#${issue_number}: claim by ${claim.claimant} ran out; reviewed=${reviewed}.`); - - if (reviewed) { - // The label goes, but the assignee stays: they did the work. - await claims.releaseClaim(github, core, target, null); - await claims.writeStatus(github, target, { ...claim, state: 'completed' }, statusComment); - continue; - } - - await claims.releaseClaim(github, core, target, claim.claimant); - await claims.writeStatus(github, target, { ...claim, state: 'expired' }, statusComment); - // The status comment is edited rather than reposted, which notifies - // nobody, so the release itself gets its own @-mention. - await github.rest.issues.createComment({ - owner, repo, issue_number, - body: [ - `@${claim.claimant} your review claim on this PR ran out at ` + - `${claims.formatUTC(claim.until)} without a review, so I have removed you as a`, - 'reviewer and assignee.', - '', - 'This PR is back in the general review queue. Comment `claim` if you would still', - 'like to take it.', - ].join('\n'), - }); - - // Zulip only hears about the failures: a claim that was honoured is - // not news, and the point of announcing this one is that the PR now - // needs somebody else. GitHub logins are not Zulip names, so the - // claimant is named rather than @-mentioned. - await claims.notifyZulip(core, [ - `**Review claim expired** on [${repo}#${issue_number}](${issue.html_url}): ${issue.title}`, - '', - `\`${claim.claimant}\` claimed this review until ${claims.formatUTC(claim.until)}, 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`.', - ].join('\n')); - } diff --git a/scripts/review_claim.py b/scripts/review_claim.py new file mode 100644 index 0000000000..a470d90287 --- /dev/null +++ b/scripts/review_claim.py @@ -0,0 +1,633 @@ +#!/usr/bin/env python3 +""" +Review claims for pull requests. + +To avoid two reviewers (human or AI) reviewing the same PR, a reviewer says what +they intend to review and claims it, by commenting on the PR: + + 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 requests a review from the claimant, assigns them, 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. +A claim that runs out without a review is released -- the claimant comes off the +PR as reviewer and assignee -- and announced on Zulip, so that somebody else +picks the PR up. + +The whole state of a claim lives in that one status comment, in a hidden marker +holding a JSON record. The comment is edited in place rather than reposted, so a +PR accumulates at most one of them however often the claim is extended, and there +is nothing to keep in sync anywhere else. + +Sample usage, from the workflows in .github/workflows/review_claim*.yml: + + $ python scripts/review_claim.py comment # handle an issue_comment event + $ python scripts/review_claim.py review # handle a pull_request_review event + $ python scripts/review_claim.py expire # remind about, and expire, claims + +The first two read the event from GITHUB_EVENT_PATH. All three need GITHUB_TOKEN +and GITHUB_REPOSITORY; the Zulip announcement additionally needs ZULIP_SITE, +ZULIP_BOT_EMAIL, ZULIP_BOT_API_KEY and ZULIP_STREAM, and is skipped with a +warning when they are not set. +""" + +import base64 +import json +import os +import re +import sys +import urllib.error +import urllib.parse +import urllib.request +from datetime import datetime, timedelta, timezone + +CLAIM_LABEL = 'review-claimed' +MARKER_PREFIX = '' +CLAIM_FIELDS = ('state', 'claimant', 'claimed_at', 'until') +REMINDER_MARKER = '' + +# A review claim is a short promise, so the windows are much tighter than the +# roadmap intentions this is modelled on. +DEFAULT_WINDOW = timedelta(days=2) +MAX_WINDOW = timedelta(days=14) +MIN_WINDOW = timedelta(hours=1) + +# Reminders are @-mentions sent this many hours before the deadline. A reminder +# is skipped when it is not shorter than the window itself, so a one day claim is +# never warned about a day in advance. Ascending, so that the smallest +# applicable reminder wins if a scheduled run is skipped. +REMINDERS_HOURS = (24, 48) + +UNITS = { + 'hour': timedelta(hours=1), 'hours': timedelta(hours=1), + 'day': timedelta(days=1), 'days': timedelta(days=1), + 'week': timedelta(weeks=1), 'weeks': timedelta(weeks=1), +} + +API_ROOT = 'https://api.github.com' + + +class ClaimError(Exception): + """A command we understood the shape of but cannot carry out.""" + + +def warn(message): + """Emit a GitHub Actions warning annotation.""" + print(f'::warning::{message}') + + +def now(): + return datetime.now(timezone.utc) + + +def to_iso(when): + return when.astimezone(timezone.utc).strftime('%Y-%m-%dT%H:%M:%SZ') + + +def parse_iso(text): + """Parse an ISO 8601 timestamp, tolerating the trailing `Z` GitHub sends.""" + return datetime.fromisoformat(text.replace('Z', '+00:00')) + + +def format_utc(when): + """Format a timestamp the way the bot's comments always spell one out.""" + return when.astimezone(timezone.utc).strftime('%Y-%m-%d %H:%M UTC') + + +def describe_window(window): + """Spell a duration back to the claimant, so they can check what we understood.""" + seconds = window.total_seconds() + + def trim(value): + return str(int(value)) if value == int(value) else str(round(value, 1)) + + if seconds % 86400 == 0 and seconds >= 86400: + days = seconds / 86400 + if days % 7 == 0: + weeks = days / 7 + return f'{trim(weeks)} week' + ('' if weeks == 1 else 's') + return f'{trim(days)} day' + ('' if days == 1 else 's') + hours = seconds / 3600 + return f'{trim(hours)} hour' + ('' if hours == 1 else 's') + + +def parse_window(argument, at): + """ + Parse the argument of a `claim` command into a deadline. + + Accepts an empty argument (the default window), ` hours|days|weeks`, or an + absolute `YYYY-MM-DD` date, read as the end of that day UTC. Over-long + windows are clamped rather than rejected; the caller is told via `clamped`. + Returns a `(until, clamped)` pair, or raises `ClaimError` with a message + meant for the claimant. + """ + trimmed = (argument or '').strip().lower() + + if trimmed == '': + until = at + DEFAULT_WINDOW + elif re.fullmatch(r'\d{4}-\d{2}-\d{2}', trimmed): + try: + until = parse_iso(f'{trimmed}T23:59:59Z') + except ValueError: + raise ClaimError(f'`{trimmed}` is not a real date.') + else: + match = re.fullmatch(r'(\d+)\s*(hour|hours|day|days|week|weeks)', trimmed) + if not match: + raise ClaimError( + f'I could not read `{trimmed}` as a window. Use `claim`, ' + '`claim 5 days` (or hours/weeks), or `claim 2026-08-01`.') + until = at + int(match.group(1)) * UNITS[match.group(2)] + + if until - at < MIN_WINDOW: + raise ClaimError('That window is already over. Pick a deadline in the future.') + clamped = until - at > MAX_WINDOW + if clamped: + until = at + MAX_WINDOW + return until, clamped + + +def parse_command(body): + """ + Read a command out of a comment body. + + As elsewhere in this repository, a command is a whole line: we react to a line + whose entire content, up to whitespace, is the command, so that a comment + merely discussing claims does not trigger one. The last command in a comment + wins. Returns a `(name, argument)` pair, or None. + """ + command = None + for line in (body or '').replace('\r', '').split('\n'): + trimmed = line.strip() + match = re.match(r'claim\b(.*)$', trimmed, re.IGNORECASE) + if match: + command = ('claim', match.group(1)) + elif re.fullmatch(r'disclaim', trimmed, re.IGNORECASE): + command = ('disclaim', None) + return command + + +def read_claim(body): + """ + The claim record carried by a comment body, or None if there is none. + + A marker that is unreadable or missing a field is treated as no claim at all, + rather than trusted and crashed on: anyone can paste one of these into a + comment, and the expiry run then clears the stale label as it would for any + other PR labelled without a live claim. + """ + if not body or MARKER_PREFIX not in body: + return None + start = body.index(MARKER_PREFIX) + len(MARKER_PREFIX) + end = body.find(MARKER_SUFFIX, start) + if end == -1: + return None + try: + record = json.loads(body[start:end]) + except json.JSONDecodeError: + return None + if not isinstance(record, dict) or not all( + isinstance(record.get(field), str) for field in CLAIM_FIELDS): + return None + return record + + +def pick_status_comment(comments): + """The status comment among an already-fetched list, or None if there is none.""" + for comment in reversed(comments): + if MARKER_PREFIX in (comment.get('body') or ''): + return comment + return None + + +def render_status(claim): + """Render the status comment body for a claim record.""" + marker = MARKER_PREFIX + json.dumps(claim) + MARKER_SUFFIX + claimant = claim['claimant'] + + if claim['state'] == 'released': + return f'{marker}\nReview claim by @{claimant} released. This PR is back in the review queue.' + if claim['state'] == 'completed': + return f'{marker}\nReview claim by @{claimant} completed — thanks for the review.' + if claim['state'] == 'expired': + return '\n'.join([ + marker, + f'Review claim by @{claimant} expired on {format_utc(parse_iso(claim["until"]))} ' + 'without a review.', + 'This PR is back in the review queue.', + ]) + + until = parse_iso(claim['until']) + window = until - parse_iso(claim['claimed_at']) + reminders = [hours for hours in REMINDERS_HOURS if timedelta(hours=hours) < window] + reminders.sort(reverse=True) + if reminders: + promise = ('I will remind them here ' + + ' and '.join(f'{hours}h' for hours in reminders) + + ' before that runs out.') + else: + promise = 'That window is too short for a reminder, so there will not be one.' + + return '\n'.join([ + marker, + f'**@{claimant} has claimed this PR for review** until {format_utc(until)} ' + f'({describe_window(window)}).', + '', + promise, + 'If no review lands in time the claim is released automatically and this PR returns to', + 'the review queue.', + '', + 'Comment `claim` to extend, `claim 5 days` / `claim 2026-08-01` for a specific window, or', + '`disclaim` to release it early. A claim is cooperative, not a lock: it signals intent so', + 'that others can steer around it, and anyone is still free to review this PR.', + ]) + + +class GitHub: + """The slice of the GitHub REST API these workflows need.""" + + def __init__(self, token, repo): + self.token = token + self.repo = repo + + def request(self, method, path, data=None): + url = path if path.startswith('http') else f'{API_ROOT}/repos/{self.repo}{path}' + body = json.dumps(data).encode() if data is not None else None + request = urllib.request.Request(url, data=body, method=method) + request.add_header('Authorization', f'Bearer {self.token}') + request.add_header('Accept', 'application/vnd.github+json') + request.add_header('X-GitHub-Api-Version', '2022-11-28') + if body is not None: + request.add_header('Content-Type', 'application/json') + with urllib.request.urlopen(request) as response: + payload = response.read() + link = response.headers.get('Link', '') + return (json.loads(payload) if payload else None), link + + def get(self, path): + return self.request('GET', path)[0] + + def post(self, path, data): + return self.request('POST', path, data)[0] + + def patch(self, path, data): + return self.request('PATCH', path, data)[0] + + def delete(self, path, data=None): + return self.request('DELETE', path, data)[0] + + def paginate(self, path): + """Follow `Link: rel="next"` until the collection is exhausted.""" + separator = '&' if '?' in path else '?' + url = f'{path}{separator}per_page=100' + items = [] + while url: + page, link = self.request('GET', url) + items.extend(page or []) + match = re.search(r'<([^>]+)>;\s*rel="next"', link or '') + url = match.group(1) if match else None + return items + + def tolerate(self, description, method, path, data=None): + """ + Make a call whose failure must not stop the workflow. + + Labels, assignees and review requests are all things GitHub may refuse -- + the label may be gone already, the claimant may not be a collaborator -- + and none of those are worth failing a run over. + """ + try: + self.request(method, path, data) + return True + except urllib.error.HTTPError as error: + warn(f'{description}: {error.code} {error.reason}') + except urllib.error.URLError as error: + warn(f'{description}: {error.reason}') + return False + + +def take_claim(github, number, claimant): + """ + Put the claimant on the PR as both assignee and requested reviewer. + + Requesting a review is the half that shows up in everyone's review queue, but + GitHub refuses it for a non-collaborator and for the PR's own author, and + claiming deliberately needs no permissions -- so that half is best-effort. + """ + github.tolerate(f'#{number}: could not label', 'POST', + f'/issues/{number}/labels', {'labels': [CLAIM_LABEL]}) + github.tolerate(f'#{number}: could not assign {claimant}', 'POST', + f'/issues/{number}/assignees', {'assignees': [claimant]}) + github.tolerate(f'#{number}: could not request review from {claimant}', 'POST', + f'/pulls/{number}/requested_reviewers', {'reviewers': [claimant]}) + + +def release_claim(github, number, claimant=None): + """ + Drop the claim label and, when a claimant is given, take them back off the PR + as reviewer and assignee. Every step tolerates its target being gone already. + """ + github.tolerate(f'#{number}: could not remove {CLAIM_LABEL}', 'DELETE', + f'/issues/{number}/labels/{CLAIM_LABEL}') + if not claimant: + return + github.tolerate(f'#{number}: could not unassign {claimant}', 'DELETE', + f'/issues/{number}/assignees', {'assignees': [claimant]}) + github.tolerate(f'#{number}: could not drop the review request for {claimant}', 'DELETE', + f'/pulls/{number}/requested_reviewers', {'reviewers': [claimant]}) + + +def has_reviewed_since(github, number, claimant, since): + """ + Has the claimant looked at the PR since claiming it? A submitted review or an + inline review comment both count; a plain issue comment deliberately does not. + """ + for review in github.paginate(f'/pulls/{number}/reviews'): + if review['user']['login'] == claimant and parse_iso(review['submitted_at']) >= since: + return True + for comment in github.paginate(f'/pulls/{number}/comments'): + if comment['user']['login'] == claimant and parse_iso(comment['created_at']) >= since: + return True + return False + + +def write_status(github, number, claim, existing): + """Create or edit the single status comment carrying the claim record.""" + body = {'body': render_status(claim)} + if existing: + return github.patch(f'/issues/comments/{existing["id"]}', body) + return github.post(f'/issues/{number}/comments', body) + + +def notify_zulip(content): + """ + Announce something on Zulip, using the same bot credentials and message API as + the Physlib Zulip bots. + + A missing or broken Zulip setup must never take a workflow down with it: the + GitHub side of an expiry has already happened by the time this is called, so a + failure here is warned about and swallowed. + """ + site = os.environ.get('ZULIP_SITE') + email = os.environ.get('ZULIP_BOT_EMAIL') + key = os.environ.get('ZULIP_BOT_API_KEY') + stream = os.environ.get('ZULIP_STREAM') + if not (site and email and key and stream): + warn('Zulip is not configured (ZULIP_SITE / ZULIP_BOT_EMAIL / ZULIP_BOT_API_KEY / ' + 'ZULIP_STREAM), skipping the announcement.') + return False + + # `to` takes a stream name or a stream id, so ZULIP_STREAM can be either. + body = urllib.parse.urlencode({ + 'type': 'stream', + 'to': stream, + 'topic': os.environ.get('ZULIP_TOPIC') or 'PR reviews', + 'content': content, + }).encode() + credentials = base64.b64encode(f'{email}:{key}'.encode()).decode() + + request = urllib.request.Request(f'{site.rstrip("/")}/api/v1/messages', data=body, + method='POST') + request.add_header('Authorization', f'Basic {credentials}') + request.add_header('Content-Type', 'application/x-www-form-urlencoded') + try: + with urllib.request.urlopen(request): + return True + except urllib.error.HTTPError as error: + warn(f'Zulip API error: {error.code} {error.read().decode(errors="replace")}') + except urllib.error.URLError as error: + warn(f'Could not reach Zulip: {error.reason}') + return False + + +def may_release(github, actor, claimant): + """ + The claimant can always let go; a maintainer can release someone else's claim + without waiting for it to time out. + """ + if actor == claimant: + return True + try: + access = github.get(f'/collaborators/{actor}/permission') + except (urllib.error.HTTPError, urllib.error.URLError): + return False + return access.get('permission') in ('admin', 'maintain', 'write') + + +def handle_comment(github, event): + """Handle an `issue_comment` event: the `claim` and `disclaim` commands.""" + command = parse_command(event['comment']['body']) + if not command: + print('No claim command in this comment.') + return + name, argument = command + + number = event['issue']['number'] + actor = event['comment']['user']['login'] + comment_id = event['comment']['id'] + at = now() + + def react(content): + github.tolerate('Could not react', 'POST', + f'/issues/comments/{comment_id}/reactions', {'content': content}) + + def reject(message): + react('confused') + github.post(f'/issues/{number}/comments', {'body': f'@{actor} {message}'}) + + comments = github.paginate(f'/issues/{number}/comments') + status_comment = pick_status_comment(comments) + current = read_claim(status_comment.get('body') if status_comment else None) + active = current if current and current['state'] == 'active' else None + + if name == 'disclaim': + if not active: + print(f'#{number}: nothing to disclaim.') + react('confused') + return + if not may_release(github, actor, active['claimant']): + reject(f'this PR is claimed by @{active["claimant"]} until ' + f'{format_utc(parse_iso(active["until"]))}, and only they (or a maintainer) ' + 'can release it. It will be released automatically if no review arrives ' + 'by then.') + return + + print(f'#{number}: {actor} released the claim held by {active["claimant"]}.') + release_claim(github, number, active['claimant']) + write_status(github, number, + dict(active, state='released', released_by=actor), status_comment) + react('+1') + return + + # Someone else's live claim is not silently overwritten: the point of the whole + # mechanism is that a second reviewer finds out before duplicating the work. + if active and active['claimant'] != actor: + reject(f'this PR is already claimed by @{active["claimant"]} until ' + f'{format_utc(parse_iso(active["until"]))}. It will be released automatically ' + 'if no review arrives by then, and you are still free to review it in the ' + 'meantime — a claim signals intent rather than locking anyone out.') + return + + try: + until, clamped = parse_window(argument, at) + except ClaimError as error: + reject(str(error)) + return + + # Extending records a fresh claim time, so the status comment keeps describing + # the window the claimant actually asked for. + claim = { + 'state': 'active', + 'claimant': actor, + 'claimed_at': to_iso(at), + 'until': to_iso(until), + } + take_claim(github, number, actor) + write_status(github, number, claim, status_comment) + react('+1') + + if clamped: + github.post(f'/issues/{number}/comments', {'body': + f'@{actor} that window was longer than the {describe_window(MAX_WINDOW)} ' + f'maximum, so I shortened it to {format_utc(until)}. Comment `claim` again ' + 'to extend it later.'}) + print(f'#{number}: {actor} claimed until {to_iso(until)}.') + + +def handle_review(github, event): + """Handle a `pull_request_review` event: a review completes its claim.""" + number = event['pull_request']['number'] + reviewer = event['review']['user']['login'] + + comments = github.paginate(f'/issues/{number}/comments') + status_comment = pick_status_comment(comments) + current = read_claim(status_comment.get('body') if status_comment else None) + if not current or current['state'] != 'active' or current['claimant'] != reviewer: + print(f'#{number}: review by {reviewer} does not close an active claim.') + return + + print(f'#{number}: {reviewer} reviewed, completing their claim.') + # The label goes, but the assignee stays: they are engaged with this PR now, + # which is the opposite of the case the expiry run handles. + release_claim(github, number) + write_status(github, number, dict(current, state='completed'), status_comment) + + +def expire(github): + """Remind about, and release, claims on every open PR carrying the label.""" + issues = github.paginate(f'/issues?state=open&labels={CLAIM_LABEL}') + at = now() + + for issue in issues: + # The issues endpoint returns issues and PRs alike; we only want PRs. + if 'pull_request' not in issue: + continue + number = issue['number'] + + # One fetch serves both the claim record and the reminder markers. + comments = github.paginate(f'/issues/{number}/comments') + status_comment = pick_status_comment(comments) + claim = read_claim(status_comment.get('body') if status_comment else None) + if not claim or claim['state'] != 'active': + warn(f'#{number}: labelled {CLAIM_LABEL} with no active claim; clearing the label.') + release_claim(github, number) + continue + + claimant = claim['claimant'] + claimed_at = parse_iso(claim['claimed_at']) + until = parse_iso(claim['until']) + hours_left = (until - at).total_seconds() / 3600 + + if at < until: + # Smallest reminder that is both due and shorter than the window: if a + # scheduled run is skipped and we come back with 20h left, that sends + # the 24h reminder rather than a stale 48h one. + due = next((hours for hours in REMINDERS_HOURS + if timedelta(hours=hours) < until - claimed_at and hours_left <= hours), + None) + if due is None: + print(f'#{number}: {claimant} has {hours_left:.1f}h left, no reminder due.') + continue + if has_reviewed_since(github, number, claimant, claimed_at): + print(f'#{number}: {claimant} has already reviewed, ' + f'skipping the {due}h reminder.') + continue + + # Keyed to the deadline, so the hourly runs in between do not repeat a + # reminder and an extension earns a fresh set. + marker = REMINDER_MARKER.format(until=claim['until'], hours=due) + if any(marker in (comment.get('body') or '') for comment in comments): + print(f'#{number}: {due}h reminder for {claimant} already posted.') + continue + + print(f'#{number}: posting the {due}h reminder for {claimant}.') + github.post(f'/issues/{number}/comments', {'body': '\n'.join([ + marker, + f'@{claimant} about {due} hours are left on your review claim for this PR, ' + f'which runs out at {format_utc(until)}.', + '', + 'Reviewing it before then completes the claim. Comment `claim` to give yourself', + 'more time, or `disclaim` to hand it back to the review queue.', + ])}) + continue + + reviewed = has_reviewed_since(github, number, claimant, claimed_at) + print(f'#{number}: claim by {claimant} ran out; reviewed={reviewed}.') + + if reviewed: + # The label goes, but the assignee stays: they did the work. + release_claim(github, number) + write_status(github, number, dict(claim, state='completed'), status_comment) + continue + + release_claim(github, number, claimant) + write_status(github, number, dict(claim, state='expired'), status_comment) + # The status comment is edited rather than reposted, which notifies nobody, + # so the release itself gets its own @-mention. + github.post(f'/issues/{number}/comments', {'body': '\n'.join([ + f'@{claimant} your review claim on this PR ran out at {format_utc(until)} ' + 'without a review, so I have removed you as a reviewer and assignee.', + '', + 'This PR is back in the general review queue. Comment `claim` if you would still', + 'like to take it.', + ])}) + + # Zulip only hears about the failures: a claim that was honoured is not + # news, and the point of announcing this one is that the PR now needs + # somebody else. GitHub logins are not Zulip names, so the claimant is + # named rather than @-mentioned. + repo_name = github.repo.split('/')[-1] + notify_zulip('\n'.join([ + f'**Review claim expired** on [{repo_name}#{number}]({issue["html_url"]}): ' + f'{issue["title"]}', + '', + f'`{claimant}` claimed this review until {format_utc(until)}, 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`.', + ])) + + +def main(argv): + if len(argv) != 2 or argv[1] not in ('comment', 'review', 'expire'): + print(f'usage: {argv[0]} comment|review|expire', file=sys.stderr) + return 2 + + github = GitHub(os.environ['GITHUB_TOKEN'], os.environ['GITHUB_REPOSITORY']) + if argv[1] == 'expire': + expire(github) + return 0 + + with open(os.environ['GITHUB_EVENT_PATH'], encoding='utf-8') as handle: + event = json.load(handle) + if argv[1] == 'comment': + handle_comment(github, event) + else: + handle_review(github, event) + return 0 + + +if __name__ == '__main__': + sys.exit(main(sys.argv))