From eb9fe24b2f4e8114e80f5e794f60992f4e8d47a1 Mon Sep 17 00:00:00 2001 From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com> Date: Tue, 13 Oct 2026 17:24:51 -0400 Subject: [PATCH 1/7] bot: settle gate counts real reviewers The gate counted the PR author (the operator's own account) as one of its >=2 reviewers and treated any OWNER/MEMBER/COLLABORATOR association as a maintainer, so batch 7 opened on the author plus a Mathlib reviewer. - the author never counts toward the gate (their per-tag verdicts still do) - 'maintainer' is only the explicit MAINTAINERS list (the Mathlib maintainers team, 28 logins); the association and org probe are gone - a maintainer's reaction no longer overrides the author's written objection - the ready comment (settle.ready_header) states the rule applied and how many green tags rest on the author's approval alone Tests: bot/test_settle_gate.py. --- bot/README.md | 16 ++-- bot/harvest_corrections.py | 5 +- bot/poll.py | 3 +- bot/settle.py | 103 +++++++++++------------- bot/test_poll.py | 71 ++++------------- bot/test_settle_gate.py | 158 +++++++++++++++++++++++++++++++++++++ scripts/ci-python.sh | 1 + 7 files changed, 238 insertions(+), 119 deletions(-) create mode 100644 bot/test_settle_gate.py diff --git a/bot/README.md b/bot/README.md index 5856be67d..61992d529 100644 --- a/bot/README.md +++ b/bot/README.md @@ -10,10 +10,10 @@ next batch only after the current one merges. Each run does two phases: 1. **Settle** the current PR (`settle.py`, deterministic): - - **Gate:** โ‰ฅ2 distinct people with a recorded verdict on the PR, **counting the - PR author**, at least one of them a "maintainer": `jcommelin`, `faenuccio`, or - anyone GitHub lists as an owner, member or collaborator of mathlib4 (which - includes Mathlib reviewers). No minimum PR age is checked. + - **Gate:** โ‰ฅ2 distinct human reviewers on the PR besides its author, + including โ‰ฅ1 Mathlib maintainer from the explicit list in `settle.py` + (`MAINTAINERS`). GitHub's author association does not count: it also marks + Mathlib reviewers, and misses maintainers whose org membership is private. - When the gate is open, classify each tag and **split** the PR down to its green tags (`split.py`, force-push), then post a ready-to-merge comment. - Any Mathlib maintainer merges the now-all-green PR (`bors merge`, or delegates @@ -26,9 +26,13 @@ Each run does two phases: ## Per-tag rule (`settle.py`) - A bare **note/comment = "defer to the other reviewer"** โ†’ ignored. -- A **maintainer's explicit approve/reject/revise/flag trumps** everything. +- A **maintainer's explicit approve/reject/revise/flag trumps** everything, except + that a maintainer's ๐Ÿ‘ reaction never overrides the PR author's written objection. - Otherwise: any **reject/revise/flag โ†’ recycle**; else **โ‰ฅ1 approve โ†’ green**; - else (no review) โ†’ recycle. + else (no review) โ†’ recycle. The author's own verdicts count per tag, but never + toward the gate. +- The ready comment says how many green tags a reviewer other than the author + approved, and how many rest on the author's approval with no reviewer objection. So one approval suffices per tag (silence = agreement), but any unresolved objection recycles, and a maintainer overrides. Recording model: the detailed diff --git a/bot/harvest_corrections.py b/bot/harvest_corrections.py index 7df894f77..d79de2ae1 100644 --- a/bot/harvest_corrections.py +++ b/bot/harvest_corrections.py @@ -181,15 +181,14 @@ def harvest(pr, repo=REPO): records = [] for c in settle.gh_list(repo, f"issues/{pr}/comments"): login = (c.get("user") or {}).get("login", "") - assoc = c.get("author_association") body = c.get("body", "") or "" if login in settle.BOTS: continue if "## WikiLean review" not in body and not re.search(r"##\s*WikiLean review", body): continue - # Maintainer if org-role association OR on the allowlist. - is_maint = (assoc in settle.ORG_ROLES) or (login in settle.MAINTAINERS) + # Maintainer only if on settle's explicit list (not GitHub's association). + is_maint = login in settle.MAINTAINERS if is_maint: maint.add(login) diff --git a/bot/poll.py b/bot/poll.py index ee3e86d3e..1e2f08fc3 100644 --- a/bot/poll.py +++ b/bot/poll.py @@ -4,7 +4,8 @@ Each tick looks at the current batch PR's GitHub state and acts on it: - MERGED -> open the next batch (open_batch.py) - OPEN + settle gate met -> trim to greens + triage/queue the rest - (>=2 reviewers incl >=1 maintainer) + post the reviewer table + ready comment + (>=2 reviewers besides the author, + post the reviewer table + ready comment + incl >=1 listed maintainer) - CLOSED, not merged -> halt: exit non-zero for a human - otherwise -> wait (nothing to do) A failed GitHub read in decide()/tick() (bad token, error body, empty answer) exits diff --git a/bot/settle.py b/bot/settle.py index 9baacecb4..ea0307e3d 100644 --- a/bot/settle.py +++ b/bot/settle.py @@ -5,24 +5,30 @@ split. No mutations. Importable (`classify(pr)`) and runnable (prints a report). Rule (see bot/README.md): - - Gate: >=2 distinct people with a recorded review on the PR, the PR author - included, >=1 of them a "maintainer": MAINTAINERS, an OWNER/MEMBER/COLLABORATOR - association on the PR, or a public org member who reacted. No PR age is checked. + - Gate: >=2 distinct human reviewers on the PR besides its author, including + >=1 Mathlib maintainer from MAINTAINERS. - A bare note/comment = "defer to the other reviewer" -> ignored. - - A maintainer's explicit approve/reject/revise/flag (a ๐Ÿ‘/๐Ÿ‘Ž reaction included) TRUMPS. - - Else: any reject/revise/flag -> recycle; else >=1 approve (the author's own - included) -> green; else recycle. + - A maintainer's explicit approve/reject/revise/flag TRUMPS, except that a + maintainer's reaction never overrides the PR author's written objection. + - Else: any reject/revise/flag -> recycle; else >=1 approve -> green; else recycle. + The author's own verdicts count here, per tag, but never toward the gate. """ import json, subprocess, re, sys, datetime as dt -# Allowlist seed (always treated as maintainer). Needed for maintainers whose -# leanprover-community org membership is PRIVATE: their author_association -# shows CONTRIBUTOR and the members probe 404s, so without the seed their -# verdicts lose the maintainer trump โ€” batch 6 bug: faenuccio's post-settle -# rejects were trumped by an earlier approve and never re-trimmed the PR. -MAINTAINERS = {"jcommelin", "faenuccio"} -# GitHub author_association values that mark a Mathlib maintainer/reviewer. -ORG_ROLES = {"OWNER", "MEMBER", "COLLABORATOR"} +# The ONLY source of "maintainer": the "Mathlib maintainers" team in +# leanprover-community/leanprover-community.github.io data/teams.yaml (commit +# 5b8381a4, 2026-09-13), names mapped to the GitHub logins `gh api users/` +# confirms. GitHub's author_association is not used: COLLABORATOR also covers +# Mathlib reviewers, and a maintainer whose org membership is private shows +# CONTRIBUTOR (batch 6: faenuccio's rejects were ignored that way). Update this +# list when the team changes. +MAINTAINERS = frozenset({ + "adamtopaz", "ADedecker", "adomani", "b-mehta", "bryangingechen", "digama0", + "dupuisf", "eric-wieser", "faenuccio", "fpvandoorn", "grunweg", "hrmacbeth", + "j-loreaux", "jcommelin", "joelriou", "kbuzzard", "kim-em", "kmill", + "mattrobball", "ocfnash", "PatrickMassot", "RemyDegenne", "riccardobrasca", + "robertylewis", "sgouezel", "TwoFX", "urkud", "Vierkantor", +}) OBJECT = ("reject", "revise", "flag") # hard objections (a note is NOT one) BOTS = {"github-actions[bot]"} REACTION_VERDICT = {"+1": "approve", "-1": "reject"} # ๐Ÿ‘ = approve, ๐Ÿ‘Ž = reject (REST content names) @@ -84,23 +90,6 @@ def gh_reactions(repo, comment_id): return gh_list(repo, f"pulls/comments/{comment_id}/reactions") -_ORG_MEMBER = {} -def is_org_member(repo, login): - """Is `login` a PUBLIC member of the repo's org? Reaction objects carry no - author_association, so this is how a react-only reviewer is recognised as a - maintainer (private members 404 โ€” they fall back to the MAINTAINERS seed). - Cached per run so N reactions by one maintainer cost one API call.""" - org = repo.split("/")[0] - k = (org, login) - if k not in _ORG_MEMBER: - args = ["api", f"orgs/{org}/members/{login}", "--silent"] - r = subprocess.run(["gh", *args], capture_output=True, text=True) - if r.returncode != 0 and "HTTP 404" not in (r.stderr or ""): - raise GhError(gh_failure(args, r)) - _ORG_MEMBER[k] = (r.returncode == 0) # 204 -> 0 (member), 404 -> not a public member - return _ORG_MEMBER[k] - - def is_merged(pr, repo="leanprover-community/mathlib4"): """True if the PR merged. Mathlib merges via BORS, which closes the PR (state 'closed', merged=false) and prefixes the title '[Merged by Bors] - โ€ฆ' โ€” @@ -172,26 +161,25 @@ def classify(pr, repo="leanprover-community/mathlib4"): # explicit[(qid, login)] = (status, ts); notes[(qid, login)] = text explicit, notes, reviewers = {}, {}, set() - # Maintainers/reviewers: anyone whose GitHub author_association on the PR is an - # org role, seeded by the explicit allowlist. Their verdict trumps, and the - # settle gate needs >=1 of them. - maint = set(MAINTAINERS) - def record_assoc(login, assoc): - if login and login not in BOTS and assoc in ORG_ROLES: - maint.add(login) - def note_explicit(qid, login, status, ts, text=""): + # (qid, login) pairs whose latest verdict is a reaction, not a written comment. + by_reaction = set() + # The PR author is the operator (the bot opens PRs under the operator's account): + # their verdicts count per tag, but they are never one of the gate's reviewers. + author = (meta.get("user") or {}).get("login", "") + maint = MAINTAINERS + def note_explicit(qid, login, status, ts, text="", reaction=False): if not login or login in BOTS: return reviewers.add(login) k = (qid, login) if k not in explicit or ts > explicit[k][1]: explicit[k] = (status, ts) + (by_reaction.add if reaction else by_reaction.discard)(k) if text: notes[k] = text for c in gh_list(repo, f"pulls/{pr}/comments"): u = (c.get("user") or {}).get("login", "") - record_assoc(u, c.get("author_association")) b = c.get("body", "") or "" m = re.search(r"wikilean-review:(Q\d+)", b) if m: @@ -211,12 +199,9 @@ def note_explicit(qid, login, status, ts, text=""): ru = (r.get("user") or {}).get("login", "") if not v or not ru or ru in BOTS: continue - if ru not in maint and is_org_member(repo, ru): - maint.add(ru) # a maintainer's reaction trumps, like a maintainer comment - note_explicit(qid, ru, v, r.get("created_at", "")) + note_explicit(qid, ru, v, r.get("created_at", ""), reaction=True) for c in gh_list(repo, f"issues/{pr}/comments"): u = (c.get("user") or {}).get("login", "") - record_assoc(u, c.get("author_association")) b = c.get("body", "") or "" if u in BOTS: continue @@ -227,7 +212,6 @@ def note_explicit(qid, login, status, ts, text=""): pr_state = {} for r in gh_list(repo, f"pulls/{pr}/reviews"): u = (r.get("user") or {}).get("login", "") - record_assoc(u, r.get("author_association")) if not u or u in BOTS: continue ts = r.get("submitted_at", "") or "" @@ -239,7 +223,10 @@ def note_explicit(qid, login, status, ts, text=""): def decide(qid): ex = {u: stt for (q, u), (stt, _) in explicit.items() if q == qid} real = {u: stt for u, stt in ex.items() if stt != "(note)"} - mver = [stt for u, stt in real.items() if u in maint] + # A reaction never overrides the operator's written objection. + author_objects = real.get(author) in OBJECT and (qid, author) not in by_reaction + mver = [stt for u, stt in real.items() + if u in maint and not (author_objects and (qid, u) in by_reaction)] if mver: if any(s in OBJECT for s in mver): return "recycle", ex, "maintainer rejected/revised" @@ -258,11 +245,14 @@ def decide(qid): green, recycle = [], [] for q in tags: verdict, ex, why = decide(q) + real = {u: stt for u, stt in ex.items() if stt != "(note)"} + approvers = {u for u, stt in real.items() if stt == "approve"} | (blanket - real.keys()) rec = { "qid": q, "file": decl_line.get(q, (None, None))[0], "verdicts": ex, "reason": why, + "approved_by_reviewer": bool(approvers - {author}), "notes": [ {"login": u, "status": ex[u], "text": notes.get((q, u), "")} for u in ex if notes.get((q, u)) @@ -270,10 +260,12 @@ def decide(qid): } (green if verdict == "green" else recycle).append(rec) + reviewers.discard(author) maint_reviewers = sorted(reviewers & maint) gate_ok = len(reviewers) >= 2 and bool(maint_reviewers) return { "pr": pr, "repo": repo, "head_sha": head_sha, "age_h": round(age_h, 1), + "author": author, "reviewers": sorted(reviewers), "blanket_approvers": sorted(blanket), "maintainer_reviewers": maint_reviewers, "gate": gate_ok, @@ -283,16 +275,17 @@ def decide(qid): def ready_header(cls): - """The settle comment's first line, stating the rule classify() applied. It names - reviewers in code font, without @, so it adds no mentions of its own (the tag - table below it already lists reviewers).""" + """The settle comment's first line. It states what the gate checked and how many + green tags rest on the author's approval alone. It names maintainers without @, so + it adds no mentions of its own (the tag table below it lists reviewers).""" green, recycle = cls["green"], cls["recycle"] - who = ", ".join(f"`{u}`" for u in cls["reviewers"]) or "none" - return (f"This PR was trimmed to the **{len(green)}** `@[wikidata]` tags with at least one approval ๐ŸŸข " - f"and no unresolved objection. Under this bot's rule one approval per tag is enough, and it can " - f"be the PR author's own or a single ๐Ÿ‘ reaction; a verdict from a Mathlib maintainer or from " - f"anyone GitHub lists as a mathlib4 owner, member or collaborator overrides the others. " - f"Reviews recorded from: {who}. **Ready for a maintainer's review.**" + by_reviewer = sum(1 for g in green if g["approved_by_reviewer"]) + maint = ", ".join(f"`{m}`" for m in cls["maintainer_reviewers"]) or "none" + return (f"This PR was trimmed to the **{len(green)}** `@[wikidata]` tags with an approval and no " + f"unresolved objection: {by_reviewer} approved by a reviewer other than the PR author, " + f"{len(green) - by_reviewer} approved by the author with no objection from reviewers. " + f"Reviewed by {len(cls['reviewers'])} people besides the author (maintainers: {maint}) " + f"โ€” **ready for a maintainer to merge**." + (f" {len(recycle)} recycled to the next batch." if recycle else "") + " ") diff --git a/bot/test_poll.py b/bot/test_poll.py index dbe34a800..2a55ad5c6 100644 --- a/bot/test_poll.py +++ b/bot/test_poll.py @@ -38,7 +38,7 @@ def pull(state="open", title="doc: add wikidata attributes (batch 7)", merged=False): return {"number": PR, "state": state, "merged": merged, "merged_at": None, - "title": title, "created_at": "2026-08-10T11:00:00Z", + "title": title, "created_at": "2026-08-10T11:00:00Z", "user": {"login": "Deicyde"}, "head": {"sha": "c" * 40}} @@ -67,7 +67,7 @@ class FakeGh: def __init__(self, *, pr_json=None, state="OPEN", mergeable=("MERGEABLE",), master=MASTER, diff=DIFF, reviews=(), comments=(), issue_comments=(), - checks=(0, CHECKS_GREEN, ""), edits=None, fail=None): + checks=(0, CHECKS_GREEN, ""), edits=None, reactions=None, fail=None): self.pr_json = pr_json if pr_json is not None else pull() self.state = state self.mergeable = list(mergeable) @@ -78,6 +78,7 @@ def __init__(self, *, pr_json=None, state="OPEN", mergeable=("MERGEABLE",), self.issue_comments = list(issue_comments) self.checks = checks self.edits = edits or {} + self.reactions = reactions or {} self.fail = fail self.calls = [] @@ -118,8 +119,8 @@ def route(self, cmd): return 0, lines(self.comments), "" if path == f"repos/{REPO}/issues/{PR}/comments": return 0, lines(self.issue_comments), "" - if path.startswith("orgs/"): - return 1, "", "gh: Not Found (HTTP 404)\n" + if path.startswith(f"repos/{REPO}/pulls/comments/") and path.endswith("/reactions"): + return 0, lines(self.reactions.get(int(path.split("/")[-2]), [])), "" raise AssertionError(f"unrouted gh call: {cmd}") @@ -163,7 +164,6 @@ def setUp(self): quiet = contextlib.redirect_stdout(io.StringIO()) # poll narrates every step quiet.__enter__() self.addCleanup(quiet.__exit__, None, None, None) - settle._ORG_MEMBER.clear() def write_state(self, **state): base = {"current_pr": PR, "batch_num": 7, "branch": "wikilean/wikidata-batch-7"} @@ -199,34 +199,34 @@ def test_closed_not_merged_halts_instead_of_waiting(self): def test_open_unsettled_gate_not_met_waits(self): self.write_state() - self.assertEqual(self.run_with(FakeGh(reviews=approvals("Deicyde")), poll.decide), "wait") + self.assertEqual(self.run_with(FakeGh(reviews=approvals("SnirBroshi")), poll.decide), "wait") def test_open_unsettled_gate_met_acts(self): self.write_state() - fake = FakeGh(reviews=approvals("Deicyde") + approvals("jcommelin")) + fake = FakeGh(reviews=approvals("SnirBroshi") + approvals("jcommelin")) self.assertEqual(self.run_with(fake, poll.decide), "act") def test_open_settled_clean_waits(self): self.write_state(settled_pr=PR, conflict_sha=CONFLICT_SHA) - fake = FakeGh(reviews=approvals("Deicyde") + approvals("jcommelin")) + fake = FakeGh(reviews=approvals("SnirBroshi") + approvals("jcommelin")) self.assertEqual(self.run_with(fake, poll.decide), "wait") def test_settled_conflicting_acts(self): self.write_state(settled_pr=PR, conflict_sha=CONFLICT_SHA) fake = FakeGh(mergeable=("CONFLICTING",), - reviews=approvals("Deicyde") + approvals("jcommelin")) + reviews=approvals("SnirBroshi") + approvals("jcommelin")) self.assertEqual(self.run_with(fake, poll.decide), "act") def test_settled_conflicting_already_rebuilt_on_this_master_waits(self): self.write_state(settled_pr=PR, conflict_sha=MASTER) fake = FakeGh(mergeable=("CONFLICTING",), - reviews=approvals("Deicyde") + approvals("jcommelin")) + reviews=approvals("SnirBroshi") + approvals("jcommelin")) self.assertEqual(self.run_with(fake, poll.decide), "wait") def test_unknown_mergeable_is_reread_until_github_answers(self): self.write_state(settled_pr=PR, conflict_sha=CONFLICT_SHA) fake = FakeGh(mergeable=("UNKNOWN", "UNKNOWN", "CONFLICTING"), - reviews=approvals("Deicyde") + approvals("jcommelin")) + reviews=approvals("SnirBroshi") + approvals("jcommelin")) self.assertEqual(self.run_with(fake, poll.decide), "act") reads = [c for c in fake.calls if "mergeable" in c] self.assertEqual(len(reads), 3) @@ -234,14 +234,14 @@ def test_unknown_mergeable_is_reread_until_github_answers(self): def test_persistently_unknown_mergeable_halts(self): self.write_state(settled_pr=PR, conflict_sha=CONFLICT_SHA) fake = FakeGh(mergeable=("UNKNOWN",), - reviews=approvals("Deicyde") + approvals("jcommelin")) + reviews=approvals("SnirBroshi") + approvals("jcommelin")) with self.assertRaisesRegex(poll.Halt, "UNKNOWN"): self.run_with(fake, poll.decide) def test_settled_ci_cache_flake_acts(self): self.write_state(settled_pr=PR, conflict_sha=CONFLICT_SHA) flake = "ci / Build\tpass\t10m\tu\t\nci / Post-Build Step\tfail\t1m\tu\t\n" - fake = FakeGh(reviews=approvals("Deicyde") + approvals("jcommelin"), checks=(1, flake, "")) + fake = FakeGh(reviews=approvals("SnirBroshi") + approvals("jcommelin"), checks=(1, flake, "")) self.assertEqual(self.run_with(fake, poll.decide), "act") def test_auth_failure_raises_with_a_rotation_hint(self): @@ -259,9 +259,8 @@ def test_auth_failure_on_any_later_call_raises(self): self.write_state(settled_pr=PR, conflict_sha=CONFLICT_SHA) for broken in ("pr view", "reviews", "mergeable", "commits/master", "pr checks", "pr diff"): with self.subTest(broken=broken): - settle._ORG_MEMBER.clear() fake = FakeGh(mergeable=("CONFLICTING",) if broken == "commits/master" else ("MERGEABLE",), - reviews=approvals("Deicyde") + approvals("jcommelin"), + reviews=approvals("SnirBroshi") + approvals("jcommelin"), fail=lambda c, b=broken: auth_failure(c) if b in " ".join(c) else None) with self.assertRaises(settle.GhError): self.run_with(fake, poll.decide) @@ -310,7 +309,7 @@ def test_closed_not_merged_halts(self): def test_settled_conflicting_rebuilds(self): self.write_state(settled_pr=PR, conflict_sha=CONFLICT_SHA) fake = FakeGh(mergeable=("UNKNOWN", "CONFLICTING"), - reviews=approvals("Deicyde") + approvals("jcommelin")) + reviews=approvals("SnirBroshi") + approvals("jcommelin")) out = io.StringIO() with contextlib.redirect_stdout(out): self.run_with(fake, poll.tick, Path("/unused"), True) @@ -331,7 +330,7 @@ def test_conflict_rebuild_without_the_approved_file_halts(self): def test_failed_ci_retrigger_fails_the_tick_and_keeps_the_retry(self): self.write_state(settled_pr=PR, conflict_sha=CONFLICT_SHA) flake = "ci / Build\tpass\t10m\tu\t\nci / Post-Build Step\tfail\t1m\tu\t\n" - fake = FakeGh(reviews=approvals("Deicyde") + approvals("jcommelin"), checks=(1, flake, ""), + fake = FakeGh(reviews=approvals("SnirBroshi") + approvals("jcommelin"), checks=(1, flake, ""), edits={"reopen": (1, "", "HTTP 401: Bad credentials\n")}) with mock.patch.object(poll.split, "freshen_branch_and_push", return_value=False): with self.assertRaises(SystemExit): @@ -378,51 +377,15 @@ def test_reactions_failure_is_not_swallowed(self): with self.assertRaises(settle.GhError): self.run_with(FakeGh(fail=auth_failure), settle.gh_reactions, REPO, 1) - def test_org_membership_distinguishes_not_found_from_failure(self): - member = lambda c: (0, "", "") if c[1] == "api" and c[2].startswith("orgs/") else None - self.assertTrue(self.run_with(FakeGh(fail=member), settle.is_org_member, REPO, "someone")) - settle._ORG_MEMBER.clear() - self.assertFalse(self.run_with(FakeGh(), settle.is_org_member, REPO, "someone")) - settle._ORG_MEMBER.clear() - with self.assertRaises(settle.GhError): - self.run_with(FakeGh(fail=auth_failure), settle.is_org_member, REPO, "someone") - def test_classify_rejects_an_empty_diff(self): with self.assertRaisesRegex(settle.GhError, "empty"): self.run_with(FakeGh(diff=""), settle.classify, PR, REPO) def test_classify_reads_tags_from_the_diff(self): - result = self.run_with(FakeGh(reviews=approvals("Deicyde")), settle.classify, PR, REPO) + result = self.run_with(FakeGh(reviews=approvals("SnirBroshi")), settle.classify, PR, REPO) self.assertEqual(result["tags"], ["Q36161", "Q474715"]) -class ReadyHeaderTest(PollFixture): - CLS = {"pr": PR, "reviewers": ["Deicyde", "SnirBroshi"], "maintainer_reviewers": ["SnirBroshi"], - "gate": True, "tags": ["Q1", "Q2", "Q3"], "green": [{"qid": "Q1"}, {"qid": "Q2"}], - "recycle": [{"qid": "Q3"}]} - - def test_header_states_the_rule_classify_applies(self): - h = settle.ready_header(self.CLS) - self.assertIn("**2** `@[wikidata]` tags with at least one approval", h) - self.assertIn("the PR author's own or a single ๐Ÿ‘ reaction", h) - self.assertIn("Reviews recorded from: `Deicyde`, `SnirBroshi`.", h) - self.assertIn("1 recycled to the next batch.", h) - self.assertNotIn("@SnirBroshi", h) # names, not pings - self.assertNotIn("โ‰ฅ2 reviewers", h) - self.assertTrue(h.endswith("")) - - def test_settle_posts_that_header(self): - self.write_state() - commands = [] - with mock.patch.object(poll, "sh", side_effect=lambda cmd, **kw: commands.append(cmd)), \ - mock.patch.object(poll, "CANDS", self.here / "state" / "pool_candidates.json"), \ - mock.patch.object(poll.pool, "candidates", return_value=[]), \ - mock.patch("pr_table.sync_body_count"): - poll.do_settle(PR, "wikilean/wikidata-batch-7", Path("/unused"), self.CLS, dry=False) - table = next(c for c in commands if str(c[1]).endswith("pr_table.py")) - self.assertEqual(table[table.index("--header") + 1], settle.ready_header(self.CLS)) - - class DecideCommandLineTest(unittest.TestCase): """`poll.py --decide` as CI runs it, with a fake gh executable on PATH.""" diff --git a/bot/test_settle_gate.py b/bot/test_settle_gate.py new file mode 100644 index 000000000..80155942c --- /dev/null +++ b/bot/test_settle_gate.py @@ -0,0 +1,158 @@ +#!/usr/bin/env python3 +"""Who counts in the settle gate: the PR author never does, only the explicit +maintainer list is 'maintainer', a reaction never overrides the author's written +objection, and the public header states the rule that was applied.""" +from __future__ import annotations + +import json +import unittest +from pathlib import Path +from unittest import mock + +import poll +import settle +from test_poll import PR, REPO, FakeGh, PollFixture + +AUTHOR = "Deicyde" + + +def review(login, state="APPROVED", assoc="CONTRIBUTOR", at="2026-08-11T00:00:00Z"): + return {"user": {"login": login}, "author_association": assoc, "state": state, "submitted_at": at} + + +def crossref_comment(cid, qid, plus=0, minus=0): + """The bot's per-tag inline comment that reviewers react to.""" + return {"id": cid, "user": {"login": AUTHOR}, "author_association": "CONTRIBUTOR", + "body": f"Cross-reference for {qid} ", + "created_at": "2026-08-10T11:20:00Z", "reactions": {"+1": plus, "-1": minus}} + + +def reaction(login, content="+1", at="2026-08-10T12:00:00Z"): + return {"content": content, "user": {"login": login}, "created_at": at} + + +def written_verdict(login, qid, status, at="2026-08-12T00:00:00Z", assoc="CONTRIBUTOR"): + """An inline WikiLean review comment carrying an explicit verdict.""" + return {"id": 900, "user": {"login": login}, "author_association": assoc, + "body": f" ({status})\n> {status} this tag", "created_at": at} + + +def pasted_review(login, verdicts, at="2026-08-24T00:00:00Z"): + """The '## WikiLean review' issue comment the operator pastes from the site.""" + lines = ["## WikiLean review", ""] + for qid, status in verdicts.items(): + lines += [f"- **[{qid}]** tag", f" - status: **{status}**", f" - {status} by the operator"] + return {"user": {"login": login}, "author_association": "CONTRIBUTOR", + "body": "\n".join(lines), "created_at": at} + + +class GateTest(PollFixture): + def classify(self, **kwargs): + return self.run_with(FakeGh(**kwargs), settle.classify, PR, REPO) + + def test_the_author_is_never_a_gate_reviewer(self): + r = self.classify(reviews=[review(AUTHOR, "COMMENTED"), review("jcommelin")], + issue_comments=[pasted_review(AUTHOR, {"Q36161": "approve"})]) + self.assertEqual(r["author"], AUTHOR) + self.assertEqual(r["reviewers"], ["jcommelin"]) + self.assertFalse(r["gate"]) + self.assertFalse(r["gate_reasons"]["two_reviewers"]) + + r = self.classify(reviews=[review(AUTHOR, "COMMENTED"), review("jcommelin"), review("SnirBroshi")]) + self.assertTrue(r["gate"]) + self.assertEqual(r["reviewers"], ["SnirBroshi", "jcommelin"]) + + def test_the_author_s_objection_still_recycles_a_tag(self): + r = self.classify(reviews=[review("jcommelin"), review("SnirBroshi")], + issue_comments=[pasted_review(AUTHOR, {"Q36161": "reject"})]) + self.assertEqual([g["qid"] for g in r["recycle"]], ["Q36161"]) + + def test_github_association_does_not_make_a_maintainer(self): + r = self.classify(reviews=[review("SnirBroshi", assoc="COLLABORATOR"), + review("someone", assoc="MEMBER")]) + self.assertEqual(r["maintainer_reviewers"], []) + self.assertFalse(r["gate"]) + + def test_a_listed_maintainer_counts_whatever_the_association(self): + r = self.classify(reviews=[review("faenuccio", assoc="CONTRIBUTOR"), review("SnirBroshi")]) + self.assertEqual(r["maintainer_reviewers"], ["faenuccio"]) + self.assertTrue(r["gate"]) + + def test_a_maintainer_reaction_does_not_override_the_author_s_written_reject(self): + r = self.classify( + reviews=[review("SnirBroshi", "COMMENTED")], + comments=[crossref_comment(101, "Q36161", plus=1)], + reactions={101: [reaction("jcommelin")]}, + issue_comments=[pasted_review(AUTHOR, {"Q36161": "reject"})]) + q = next(t for t in r["green"] + r["recycle"] if t["qid"] == "Q36161") + self.assertIn(q, r["recycle"]) + self.assertEqual(q["reason"], "objection (reject/revise)") + + def test_a_maintainer_reaction_still_approves_when_the_author_did_not_object(self): + r = self.classify(comments=[crossref_comment(101, "Q36161", plus=1)], + reactions={101: [reaction("jcommelin")]}) + q = next(t for t in r["green"] if t["qid"] == "Q36161") + self.assertEqual(q["reason"], "maintainer approved") + self.assertTrue(q["approved_by_reviewer"]) + + def test_a_maintainer_s_written_approve_still_trumps_the_author(self): + r = self.classify(comments=[written_verdict("jcommelin", "Q36161", "approve")], + issue_comments=[pasted_review(AUTHOR, {"Q36161": "reject"})]) + self.assertIn("Q36161", [g["qid"] for g in r["green"]]) + + def test_pr_42608_shape(self): + # The author rejected Set and PartialOrder in writing; a reviewer (not a + # maintainer) thumbed both up. The old gate opened on author + reviewer and + # kept both tags green. + r = self.classify( + reviews=[review(AUTHOR, "COMMENTED", assoc="CONTRIBUTOR"), + review("SnirBroshi", "COMMENTED", assoc="COLLABORATOR")], + comments=[crossref_comment(101, "Q36161", plus=1), crossref_comment(102, "Q474715", plus=1)], + reactions={101: [reaction("SnirBroshi")], 102: [reaction("SnirBroshi")]}, + issue_comments=[pasted_review(AUTHOR, {"Q36161": "reject", "Q474715": "reject"})]) + self.assertEqual(r["reviewers"], ["SnirBroshi"]) + self.assertEqual(r["maintainer_reviewers"], []) + self.assertFalse(r["gate"]) + self.assertEqual(sorted(t["qid"] for t in r["recycle"]), ["Q36161", "Q474715"]) + + def test_approved_by_reviewer_ignores_the_author_s_own_approval(self): + r = self.classify(reviews=[review("SnirBroshi", "COMMENTED"), review("jcommelin", "COMMENTED")], + issue_comments=[pasted_review(AUTHOR, {"Q36161": "approve", "Q474715": "approve"})], + comments=[written_verdict("SnirBroshi", "Q474715", "approve")]) + by_qid = {g["qid"]: g for g in r["green"]} + self.assertFalse(by_qid["Q36161"]["approved_by_reviewer"]) + self.assertTrue(by_qid["Q474715"]["approved_by_reviewer"]) + + +class HeaderTest(PollFixture): + CLS = {"pr": PR, "author": AUTHOR, "reviewers": ["SnirBroshi", "jcommelin"], + "maintainer_reviewers": ["jcommelin"], "gate": True, "tags": ["Q1", "Q2", "Q3"], + "green": [{"qid": "Q1", "approved_by_reviewer": True}, + {"qid": "Q2", "approved_by_reviewer": False}], + "recycle": [{"qid": "Q3"}]} + + def test_header_states_the_rule_that_was_applied(self): + h = settle.ready_header(self.CLS) + self.assertIn("**2** `@[wikidata]` tags", h) + self.assertIn("1 approved by a reviewer other than the PR author", h) + self.assertIn("1 approved by the author with no objection from reviewers", h) + self.assertIn("Reviewed by 2 people besides the author (maintainers: `jcommelin`)", h) + self.assertIn("1 recycled to the next batch.", h) + self.assertNotIn("@jcommelin", h) # names, not pings + self.assertNotIn("โ‰ฅ2 reviewers", h) + self.assertTrue(h.endswith("")) + + def test_settle_posts_that_header(self): + self.write_state(settled_pr=None) + commands = [] + with mock.patch.object(poll, "sh", side_effect=lambda cmd, **kw: commands.append(cmd)), \ + mock.patch.object(poll, "CANDS", self.here / "state" / "pool_candidates.json"), \ + mock.patch.object(poll.pool, "candidates", return_value=[]), \ + mock.patch("pr_table.sync_body_count"): + poll.do_settle(PR, "wikilean/wikidata-batch-7", Path("/unused"), self.CLS, dry=False) + table = next(c for c in commands if str(c[1]).endswith("pr_table.py")) + self.assertEqual(table[table.index("--header") + 1], settle.ready_header(self.CLS)) + + +if __name__ == "__main__": + unittest.main() diff --git a/scripts/ci-python.sh b/scripts/ci-python.sh index b74089cd0..be3c83ac5 100755 --- a/scripts/ci-python.sh +++ b/scripts/ci-python.sh @@ -118,5 +118,6 @@ run_check "Frontier suitability policy tests" "$PYTHON_BIN" brain/test_frontier_ run_check "Frontier generated-page contract" "$PYTHON_BIN" site/test_frontier_page.py run_check "Bot poller fail-closed tests" "$PYTHON_BIN" bot/test_poll.py run_check "Bot state branch tests" "$PYTHON_BIN" bot/test_state_branch.py +run_check "Bot settle gate tests" "$PYTHON_BIN" bot/test_settle_gate.py printf '\nCI Python summary: %s commands passed; all required offline scenarios ran.\n' "$CHECKS_PASSED" From 2d1e67f736c7a12098b16538ad80093396cc6566 Mon Sep 17 00:00:00 2001 From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com> Date: Tue, 13 Oct 2026 17:46:47 -0400 Subject: [PATCH 2/7] bot: settle gate review fixes: written verdicts, rebuild set, author, login case - track each login's latest written verdict apart from reactions, so a same-meaning reaction cannot cancel the author's written objection or a maintainer's written approve - a conflict rebuild re-applies every tag on the PR, not the green set: with the gate closed nothing triages a recycled tag, so it must not vanish in a force-push - a PR with no author login fails closed instead of counting the author - maintainer logins match case-insensitively (settle.is_maintainer), also in pr_table and harvest_corrections; drop harvest's unused set --- bot/README.md | 2 +- bot/harvest_corrections.py | 5 +--- bot/poll.py | 13 ++++----- bot/pr_table.py | 2 +- bot/settle.py | 36 +++++++++++++++++++------ bot/test_poll.py | 2 +- bot/test_settle_gate.py | 54 +++++++++++++++++++++++++++++++++++++- 7 files changed, 92 insertions(+), 22 deletions(-) diff --git a/bot/README.md b/bot/README.md index 61992d529..ed0b4776b 100644 --- a/bot/README.md +++ b/bot/README.md @@ -246,7 +246,7 @@ Steps: moved since its last rebuild (`conflict_sha` in `bot_state.json`), the next tick rebuilds the branch from fresh master, re-applies the green tags (no build; Mathlib CI compiles), force-pushes, and refreshes the tag table and PR body. The - log says `RESOLVE-CONFLICT #N: rebuild off fresh master with K green tags`. + log says `RESOLVE-CONFLICT #N: rebuild off fresh master with the K tags it carries`. - It records the master it rebuilt onto before pushing, so it tries at most once per master commit. Master moves many times a day, so a failed rebuild is retried on a later tick; to retry now, dispatch the workflow. diff --git a/bot/harvest_corrections.py b/bot/harvest_corrections.py index d79de2ae1..a7a3fef5a 100644 --- a/bot/harvest_corrections.py +++ b/bot/harvest_corrections.py @@ -177,7 +177,6 @@ def classify_failure_mode(note, suggested_qid, suggested_decl, orig_decl): def harvest(pr, repo=REPO): """Return a list of correction records for the PR (no I/O).""" - maint = set(settle.MAINTAINERS) records = [] for c in settle.gh_list(repo, f"issues/{pr}/comments"): login = (c.get("user") or {}).get("login", "") @@ -188,9 +187,7 @@ def harvest(pr, repo=REPO): continue # Maintainer only if on settle's explicit list (not GitHub's association). - is_maint = login in settle.MAINTAINERS - if is_maint: - maint.add(login) + is_maint = settle.is_maintainer(login) per_qid = settle.parse_pasted(body) # {qid: {status, note}} line_meta = parse_line_meta(body) # {qid: {label, file}} diff --git a/bot/poll.py b/bot/poll.py index 1e2f08fc3..8e75662f4 100644 --- a/bot/poll.py +++ b/bot/poll.py @@ -143,7 +143,7 @@ def master_tip(): def resolve_conflicts(pr, branch, mathlib, dry): """Auto-resolve a settled PR that CONFLICTS with master: RE-DERIVE the branch off - FRESH master and re-apply its green tags, then force-push. @[wikidata] tags are + FRESH master and re-apply the tags it carries, then force-push. @[wikidata] tags are purely ADDITIVE, so rebuilding on master is conflict-proof โ€” text-merging master in (freshen_master) is what kept hitting unresolvable conflicts on doc-attr PRs.""" cls = settle.classify(pr, REPO) @@ -158,13 +158,14 @@ def resolve_conflicts(pr, branch, mathlib, dry): f"cannot rebuild without decl/file per green tag; reconstruct it by " f"hand from the PR diff on the bot-state branch, then re-tick.") approved = json.loads(apath.read_text()) - # The green set = tags CURRENTLY on the PR (post-trim the recycled are already gone, - # so classify(pr).recycle is empty โ€” reconstruct from classify.green, not approved - # minus recycled, which would wrongly re-add the trimmed tags). decl/file from approved. - green_qids = {g["qid"] for g in cls["green"]} + # Rebuild exactly the tags CURRENTLY on the PR (classify's tags, read from its diff), + # not approved minus recycled, which would re-add trimmed tags, and not the green set: + # trimming belongs to the settle (triage, requeue, table), and a tag that recycles + # without the gate being met must not silently vanish here. decl/file from approved. + green_qids = set(cls["tags"]) green = {"branch": branch, "title": approved.get("title", "doc: add wikidata attributes"), "tags": [t for t in approved["tags"] if t["qid"] in green_qids]} - print(f" RESOLVE-CONFLICT #{pr}: rebuild off fresh master with {len(green['tags'])} green tags") + print(f" RESOLVE-CONFLICT #{pr}: rebuild off fresh master with the {len(green['tags'])} tags it carries") if dry: return sh(["git", "-C", str(mathlib), "fetch", "origin", branch], check=True) # --force-with-lease base diff --git a/bot/pr_table.py b/bot/pr_table.py index a0aca9ef5..55c3b2d50 100644 --- a/bot/pr_table.py +++ b/bot/pr_table.py @@ -22,7 +22,7 @@ def reviews_cell(verdicts): return "โ€”" parts = [] for login, status in verdicts.items(): - mark = "\\*" if login in settle.MAINTAINERS else "" # maintainer marked with * + mark = "\\*" if settle.is_maintainer(login) else "" # maintainer marked with * parts.append(f"{EMO.get(status, 'ยท')} @{login}{mark}") return " ยท ".join(parts) diff --git a/bot/settle.py b/bot/settle.py index ea0307e3d..005fd06be 100644 --- a/bot/settle.py +++ b/bot/settle.py @@ -29,6 +29,12 @@ "mattrobball", "ocfnash", "PatrickMassot", "RemyDegenne", "riccardobrasca", "robertylewis", "sgouezel", "TwoFX", "urkud", "Vierkantor", }) +_MAINTAINERS_LC = frozenset(m.lower() for m in MAINTAINERS) + + +def is_maintainer(login): + """GitHub logins are case-insensitive.""" + return bool(login) and login.lower() in _MAINTAINERS_LC OBJECT = ("reject", "revise", "flag") # hard objections (a note is NOT one) BOTS = {"github-actions[bot]"} REACTION_VERDICT = {"+1": "approve", "-1": "reject"} # ๐Ÿ‘ = approve, ๐Ÿ‘Ž = reject (REST content names) @@ -161,17 +167,21 @@ def classify(pr, repo="leanprover-community/mathlib4"): # explicit[(qid, login)] = (status, ts); notes[(qid, login)] = text explicit, notes, reviewers = {}, {}, set() - # (qid, login) pairs whose latest verdict is a reaction, not a written comment. - by_reaction = set() + # (qid, login) pairs whose latest verdict is a reaction, not a written comment; + # written[(qid, login)] = (status, ts) of their latest WRITTEN verdict. + by_reaction, written = set(), {} # The PR author is the operator (the bot opens PRs under the operator's account): # their verdicts count per tag, but they are never one of the gate's reviewers. author = (meta.get("user") or {}).get("login", "") - maint = MAINTAINERS + if not author: + raise GhError(f"pulls/{pr}: no author login; cannot exclude the author from the gate") def note_explicit(qid, login, status, ts, text="", reaction=False): if not login or login in BOTS: return reviewers.add(login) k = (qid, login) + if not reaction and (k not in written or ts > written[k][1]): + written[k] = (status, ts) if k not in explicit or ts > explicit[k][1]: explicit[k] = (status, ts) (by_reaction.add if reaction else by_reaction.discard)(k) @@ -223,10 +233,20 @@ def note_explicit(qid, login, status, ts, text="", reaction=False): def decide(qid): ex = {u: stt for (q, u), (stt, _) in explicit.items() if q == qid} real = {u: stt for u, stt in ex.items() if stt != "(note)"} - # A reaction never overrides the operator's written objection. - author_objects = real.get(author) in OBJECT and (qid, author) not in by_reaction - mver = [stt for u, stt in real.items() - if u in maint and not (author_objects and (qid, u) in by_reaction)] + # A reaction never overrides the operator's written objection: while the author + # objects (latest verdict) and has objected in writing, a maintainer counts only + # through their latest written verdict. + author_objects = (real.get(author) in OBJECT + and written.get((qid, author), ("",))[0] in OBJECT) + mver = [] + for u, stt in real.items(): + if not is_maintainer(u): + continue + if author_objects and (qid, u) in by_reaction: + stt = written.get((qid, u), ("(note)",))[0] + if stt == "(note)": + continue + mver.append(stt) if mver: if any(s in OBJECT for s in mver): return "recycle", ex, "maintainer rejected/revised" @@ -261,7 +281,7 @@ def decide(qid): (green if verdict == "green" else recycle).append(rec) reviewers.discard(author) - maint_reviewers = sorted(reviewers & maint) + maint_reviewers = sorted(u for u in reviewers if is_maintainer(u)) gate_ok = len(reviewers) >= 2 and bool(maint_reviewers) return { "pr": pr, "repo": repo, "head_sha": head_sha, "age_h": round(age_h, 1), diff --git a/bot/test_poll.py b/bot/test_poll.py index 2a55ad5c6..2bf51cc22 100644 --- a/bot/test_poll.py +++ b/bot/test_poll.py @@ -313,7 +313,7 @@ def test_settled_conflicting_rebuilds(self): out = io.StringIO() with contextlib.redirect_stdout(out): self.run_with(fake, poll.tick, Path("/unused"), True) - self.assertIn("RESOLVE-CONFLICT #42608: rebuild off fresh master with 2 green tags", out.getvalue()) + self.assertIn("RESOLVE-CONFLICT #42608: rebuild off fresh master with the 2 tags it carries", out.getvalue()) def test_auth_failure_raises(self): self.write_state(settled_pr=PR) diff --git a/bot/test_settle_gate.py b/bot/test_settle_gate.py index 80155942c..24759a485 100644 --- a/bot/test_settle_gate.py +++ b/bot/test_settle_gate.py @@ -4,6 +4,8 @@ objection, and the public header states the rule that was applied.""" from __future__ import annotations +import contextlib +import io import json import unittest from pathlib import Path @@ -11,7 +13,7 @@ import poll import settle -from test_poll import PR, REPO, FakeGh, PollFixture +from test_poll import CONFLICT_SHA, PR, REPO, FakeGh, PollFixture, pull AUTHOR = "Deicyde" @@ -100,6 +102,43 @@ def test_a_maintainer_s_written_approve_still_trumps_the_author(self): issue_comments=[pasted_review(AUTHOR, {"Q36161": "reject"})]) self.assertIn("Q36161", [g["qid"] for g in r["green"]]) + def test_the_author_s_reaction_after_a_written_reject_keeps_the_objection(self): + r = self.classify( + comments=[crossref_comment(101, "Q36161", plus=1, minus=1)], + reactions={101: [reaction("jcommelin", "+1", "2026-08-25T00:00:00Z"), + reaction(AUTHOR, "-1", "2026-08-26T00:00:00Z")]}, + issue_comments=[pasted_review(AUTHOR, {"Q36161": "reject"}, at="2026-08-24T00:00:00Z")]) + self.assertIn("Q36161", [t["qid"] for t in r["recycle"]]) + + def test_a_maintainer_s_reaction_after_their_written_approve_keeps_the_trump(self): + r = self.classify( + comments=[written_verdict("jcommelin", "Q36161", "approve", at="2026-08-12T00:00:00Z"), + crossref_comment(101, "Q36161", plus=1)], + reactions={101: [reaction("jcommelin", "+1", "2026-08-30T00:00:00Z")]}, + issue_comments=[pasted_review(AUTHOR, {"Q36161": "reject"})]) + q = next(t for t in r["green"] if t["qid"] == "Q36161") + self.assertEqual(q["reason"], "maintainer approved") + + def test_the_author_retracting_by_reaction_lifts_the_objection(self): + r = self.classify( + comments=[crossref_comment(101, "Q36161", plus=2)], + reactions={101: [reaction("jcommelin", "+1", "2026-08-25T00:00:00Z"), + reaction(AUTHOR, "+1", "2026-08-26T00:00:00Z")]}, + issue_comments=[pasted_review(AUTHOR, {"Q36161": "reject"}, at="2026-08-24T00:00:00Z")]) + self.assertIn("Q36161", [t["qid"] for t in r["green"]]) + + def test_maintainer_logins_match_case_insensitively(self): + r = self.classify(reviews=[review("JCommelin"), review("SnirBroshi")]) + self.assertEqual(r["maintainer_reviewers"], ["JCommelin"]) + self.assertTrue(settle.is_maintainer("remydegenne")) + self.assertFalse(settle.is_maintainer("")) + + def test_a_pr_without_an_author_fails_closed(self): + pr_json = pull() + del pr_json["user"] + with self.assertRaisesRegex(settle.GhError, "no author login"): + self.classify(pr_json=pr_json, reviews=[review("jcommelin"), review("SnirBroshi")]) + def test_pr_42608_shape(self): # The author rejected Set and PartialOrder in writing; a reviewer (not a # maintainer) thumbed both up. The old gate opened on author + reviewer and @@ -124,6 +163,19 @@ def test_approved_by_reviewer_ignores_the_author_s_own_approval(self): self.assertTrue(by_qid["Q474715"]["approved_by_reviewer"]) +class ConflictRebuildTest(PollFixture): + def test_a_rebuild_keeps_every_tag_on_the_pr(self): + # Under the new rule the author's written reject recycles Q36161, but the gate is + # closed, so no settle trims it; the conflict rebuild must not drop it either. + self.write_state(settled_pr=PR, conflict_sha=CONFLICT_SHA) + fake = FakeGh(mergeable=("CONFLICTING",), reviews=[review("SnirBroshi", "COMMENTED")], + issue_comments=[pasted_review(AUTHOR, {"Q36161": "reject"})]) + out = io.StringIO() + with contextlib.redirect_stdout(out): + self.run_with(fake, poll.tick, Path("/unused"), True) + self.assertIn("rebuild off fresh master with the 2 tags it carries", out.getvalue()) + + class HeaderTest(PollFixture): CLS = {"pr": PR, "author": AUTHOR, "reviewers": ["SnirBroshi", "jcommelin"], "maintainer_reviewers": ["jcommelin"], "gate": True, "tags": ["Q1", "Q2", "Q3"], From 3f74cf1af75cd4613cd1048e1febe47b02afdb20 Mon Sep 17 00:00:00 2001 From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com> Date: Wed, 14 Oct 2026 23:51:41 -0400 Subject: [PATCH 3/7] bot: the author's reject stands unless a listed maintainer writes later MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Main's per-tag rule let any "maintainer" verdict trump, whenever given, and "maintainer" included every mathlib4 owner/member/collaborator. On mathlib4#42608 a Mathlib reviewer's ๐Ÿ‘ (association COLLABORATOR), older than the PR author's written reject, kept Set (Q36161) and PartialOrder (Q474715) green. Maintainers whose org membership is private (16 of the 28) read as CONTRIBUTOR and 404 on the members probe; of those, only faenuccio was recognised, through the old two-login list. - MAINTAINERS is now the 28 logins of the Mathlib maintainers team (teams.yaml at 5b8381a4), added to the association and org-probe check rather than replacing it. is_maintainer() matches them case-insensitively, in settle, pr_table's maintainer mark and harvest_corrections. - decide(): if the PR author's latest verdict on a tag is a reject/revise/flag, only a listed maintainer whose latest verdict on the tag is one they wrote after it can trump. An earlier verdict, a reaction alone or an association-only maintainer no longer overrides it, so the objection recycles the tag. - ready_header names "a Mathlib maintainer listed in the bot" instead of jcommelin and faenuccio, and says only a listed maintainer's later written verdict overrides the author's reject/revise/flag. - resolve_conflicts re-applies every tag on the PR, not the green set: with the gate closed nothing triages a recycled tag, so a rebuild must not drop it. Trimming stays with the settle. The stale "green tags" wording in poll.py and the README follows. The gate is unchanged. The list, is_maintainer() and the rebuild of every tag come from this branch's earlier draft. The tests in bot/test_settle_gate.py are adapted from its fixtures: the draft's regression (a maintainer's written approve, the author's reject, then the maintainer's ๐Ÿ‘Ž went green), a replay of #42608's verdicts, and the cases that tell main and this rule apart. Co-Authored-By: Claude Opus 5.5 --- bot/README.md | 16 ++- bot/harvest_corrections.py | 7 +- bot/poll.py | 23 ++-- bot/pr_table.py | 2 +- bot/settle.py | 75 +++++++++---- bot/test_poll.py | 17 ++- bot/test_settle_gate.py | 218 +++++++++++++++++++++++++++++++++++++ scripts/ci-python.sh | 1 + 8 files changed, 311 insertions(+), 48 deletions(-) create mode 100644 bot/test_settle_gate.py diff --git a/bot/README.md b/bot/README.md index 9af3abb82..5dfb39ec7 100644 --- a/bot/README.md +++ b/bot/README.md @@ -11,9 +11,10 @@ Each run does two phases: 1. **Settle** the current PR (`settle.py`, deterministic): - **Gate:** โ‰ฅ2 distinct people with a recorded verdict on the PR, **counting the - PR author**, at least one of them a "maintainer": `jcommelin`, `faenuccio`, or - anyone GitHub lists as an owner, member or collaborator of mathlib4 (which - includes Mathlib reviewers). No minimum PR age is checked. + PR author**, at least one of them a "maintainer": a Mathlib maintainer listed + in `settle.py` (`MAINTAINERS`), or anyone GitHub lists as an owner, member or + collaborator of mathlib4 (which includes Mathlib reviewers). No minimum PR age + is checked. - When the gate is open, classify each tag and **split** the PR down to its green tags (`split.py`, force-push), then post the tag table under a header stating the rule applied and "Ready for a maintainer's review" (`settle.ready_header`). @@ -28,6 +29,8 @@ Each run does two phases: - A bare **note/comment = "defer to the other reviewer"** โ†’ ignored. - A **maintainer's explicit approve/reject/revise/flag trumps** everything. +- Except: the **PR author's reject/revise/flag** stands unless a maintainer listed + in `MAINTAINERS` writes a verdict on that tag after it (a ๐Ÿ‘/๐Ÿ‘Ž alone does not). - Otherwise: any **reject/revise/flag โ†’ recycle**; else **โ‰ฅ1 approve โ†’ green**; else (no review) โ†’ recycle. @@ -241,14 +244,15 @@ Steps: - What the bot does: when the settled PR is `CONFLICTING` and Mathlib master has moved since its last rebuild (`conflict_sha` in `bot_state.json`), the next tick - rebuilds the branch from fresh master, re-applies the green tags (no build; + rebuilds the branch from fresh master, re-applies every tag it carries (no build; Mathlib CI compiles), force-pushes, and refreshes the tag table and PR body. The - log says `RESOLVE-CONFLICT #N: rebuild off fresh master with K green tags`. + log says `RESOLVE-CONFLICT #N: rebuild off fresh master with the K tags it carries`. + Trimming recycled tags stays with the settle. - It records the master it rebuilt onto before pushing, so it tries at most once per master commit. Master moves many times a day, so a failed rebuild is retried on a later tick; to retry now, dispatch the workflow. - The run fails with `batchN_approved.json MISSING (adopted batch?)` โ†’ the rebuild needs the decl - and file of every green tag. Reconstruct `bot/state/batchN_approved.json` from + and file of every tag on the PR. Reconstruct `bot/state/batchN_approved.json` from the PR diff on `bot-state`, then dispatch. - After a clean rebuild, read the new diff before asking anyone to review it. diff --git a/bot/harvest_corrections.py b/bot/harvest_corrections.py index 7df894f77..078d5cdb7 100644 --- a/bot/harvest_corrections.py +++ b/bot/harvest_corrections.py @@ -177,7 +177,6 @@ def classify_failure_mode(note, suggested_qid, suggested_decl, orig_decl): def harvest(pr, repo=REPO): """Return a list of correction records for the PR (no I/O).""" - maint = set(settle.MAINTAINERS) records = [] for c in settle.gh_list(repo, f"issues/{pr}/comments"): login = (c.get("user") or {}).get("login", "") @@ -188,10 +187,8 @@ def harvest(pr, repo=REPO): if "## WikiLean review" not in body and not re.search(r"##\s*WikiLean review", body): continue - # Maintainer if org-role association OR on the allowlist. - is_maint = (assoc in settle.ORG_ROLES) or (login in settle.MAINTAINERS) - if is_maint: - maint.add(login) + # Maintainer if org-role association OR on settle's list (case-insensitive). + is_maint = (assoc in settle.ORG_ROLES) or settle.is_maintainer(login) per_qid = settle.parse_pasted(body) # {qid: {status, note}} line_meta = parse_line_meta(body) # {qid: {label, file}} diff --git a/bot/poll.py b/bot/poll.py index c23b698d8..cc298e1c6 100644 --- a/bot/poll.py +++ b/bot/poll.py @@ -142,7 +142,7 @@ def master_tip(): def resolve_conflicts(pr, branch, mathlib, dry): """Auto-resolve a settled PR that CONFLICTS with master: RE-DERIVE the branch off - FRESH master and re-apply its green tags, then force-push. @[wikidata] tags are + FRESH master and re-apply the tags it carries, then force-push. @[wikidata] tags are purely ADDITIVE, so rebuilding on master is conflict-proof โ€” text-merging master in (freshen_master) is what kept hitting unresolvable conflicts on doc-attr PRs.""" cls = settle.classify(pr, REPO) @@ -151,19 +151,20 @@ def resolve_conflicts(pr, branch, mathlib, dry): if not apath.exists(): # An ADOPTED batch (open_batch adopt guard) heals bot_state but cannot # conjure the approved file another runner assembled. Without it we can't - # map green qids back to decl/file, so we cannot rebuild โ€” halt (a red run) + # map the PR's qids back to decl/file, so we cannot rebuild โ€” halt (a red run) # for a human; a green 'wait' here would hide the stall. raise Halt(f"RESOLVE-CONFLICT #{pr}: {apath.name} MISSING (adopted batch?) โ€” " - f"cannot rebuild without decl/file per green tag; reconstruct it by " + f"cannot rebuild without decl/file per tag; reconstruct it by " f"hand from the PR diff on the bot-state branch, then re-tick.") approved = json.loads(apath.read_text()) - # The green set = tags CURRENTLY on the PR (post-trim the recycled are already gone, - # so classify(pr).recycle is empty โ€” reconstruct from classify.green, not approved - # minus recycled, which would wrongly re-add the trimmed tags). decl/file from approved. - green_qids = {g["qid"] for g in cls["green"]} + # Rebuild exactly the tags CURRENTLY on the PR (classify's tags, read from its diff), + # not approved minus recycled, which would re-add trimmed tags, and not the green set: + # trimming belongs to the settle (triage, requeue, table), and a tag that recycles + # while the gate is closed must not silently vanish here. decl/file from approved. + green_qids = set(cls["tags"]) green = {"branch": branch, "title": approved.get("title", "doc: add wikidata attributes"), "tags": [t for t in approved["tags"] if t["qid"] in green_qids]} - print(f" RESOLVE-CONFLICT #{pr}: rebuild off fresh master with {len(green['tags'])} green tags") + print(f" RESOLVE-CONFLICT #{pr}: rebuild off fresh master with the {len(green['tags'])} tags it carries") if dry: return sh(["git", "-C", str(mathlib), "fetch", "origin", branch], check=True) # --force-with-lease base @@ -189,9 +190,9 @@ def resolve_conflicts(pr, branch, mathlib, dry): sh([sys.executable, str(HERE / "open_batch_pr.py"), "--approved", str(gpath), "--mathlib", str(mathlib), "--repo", REPO, "--base", "master", "--apply", "--check", "--reapply"], check=True) # NO --build โ€” CI compile-checks - # The force-push shrank the diff to the green set; this path otherwise never re-runs - # pr_table, so the table comment AND the body count would both go stale. Refresh the - # trimmed table, then sync the body to the KNOWN green count (passed explicitly, so no + # The force-push rewrote the branch; this path otherwise never re-runs pr_table, so + # the table comment AND the body count would both go stale. Refresh the table, then + # sync the body to the KNOWN tag count (passed explicitly, so no # `gh pr diff` and no GitHub diff-recompute lag right after the force-push). import pr_table sh([sys.executable, str(HERE / "pr_table.py"), str(pr), "--repo", REPO, "--post", "--no-body-sync"], check=False) diff --git a/bot/pr_table.py b/bot/pr_table.py index a0aca9ef5..55c3b2d50 100644 --- a/bot/pr_table.py +++ b/bot/pr_table.py @@ -22,7 +22,7 @@ def reviews_cell(verdicts): return "โ€”" parts = [] for login, status in verdicts.items(): - mark = "\\*" if login in settle.MAINTAINERS else "" # maintainer marked with * + mark = "\\*" if settle.is_maintainer(login) else "" # maintainer marked with * parts.append(f"{EMO.get(status, 'ยท')} @{login}{mark}") return " ยท ".join(parts) diff --git a/bot/settle.py b/bot/settle.py index 06cf94e41..685eb46f5 100644 --- a/bot/settle.py +++ b/bot/settle.py @@ -9,18 +9,31 @@ included, >=1 of them a "maintainer": MAINTAINERS, an OWNER/MEMBER/COLLABORATOR association on the PR, or a public org member who reacted. No PR age is checked. - A bare note/comment = "defer to the other reviewer" -> ignored. - - A maintainer's explicit approve/reject/revise/flag (a ๐Ÿ‘/๐Ÿ‘Ž reaction included) TRUMPS. + - A maintainer's explicit approve/reject/revise/flag (a ๐Ÿ‘/๐Ÿ‘Ž reaction included) TRUMPS, + except that the PR author's latest reject/revise/flag on a tag stands unless a + LISTED maintainer (MAINTAINERS) wrote a verdict on that tag after it (a reaction + alone never overrides it). - Else: any reject/revise/flag -> recycle; else >=1 approve (the author's own included) -> green; else recycle. """ import json, subprocess, re, sys, datetime as dt -# Allowlist seed (always treated as maintainer). Needed for maintainers whose -# leanprover-community org membership is PRIVATE: their author_association -# shows CONTRIBUTOR and the members probe 404s, so without the seed their -# verdicts lose the maintainer trump โ€” batch 6 bug: faenuccio's post-settle -# rejects were trumped by an earlier approve and never re-trimmed the PR. -MAINTAINERS = {"jcommelin", "faenuccio"} +# Always treated as maintainer: the "Mathlib maintainers" team in +# leanprover-community/leanprover-community.github.io data/teams.yaml (commit +# 5b8381a4, 2026-09-13), as GitHub logins (each checked with `gh api users/`). +# Needed for maintainers whose org membership is PRIVATE: their author_association +# shows CONTRIBUTOR and the members probe 404s, so without the list their verdicts +# lose the maintainer trump โ€” batch 6 bug: faenuccio's post-settle rejects were +# trumped by an earlier approve and never re-trimmed the PR. Only a listed +# maintainer overrides the PR author's objection. Update it when the team changes. +MAINTAINERS = frozenset({ + "adamtopaz", "ADedecker", "adomani", "b-mehta", "bryangingechen", "digama0", + "dupuisf", "eric-wieser", "faenuccio", "fpvandoorn", "grunweg", "hrmacbeth", + "j-loreaux", "jcommelin", "joelriou", "kbuzzard", "kim-em", "kmill", + "mattrobball", "ocfnash", "PatrickMassot", "RemyDegenne", "riccardobrasca", + "robertylewis", "sgouezel", "TwoFX", "urkud", "Vierkantor", +}) +_MAINTAINERS_LC = frozenset(m.lower() for m in MAINTAINERS) # GitHub author_association values that mark a Mathlib maintainer/reviewer. ORG_ROLES = {"OWNER", "MEMBER", "COLLABORATOR"} OBJECT = ("reject", "revise", "flag") # hard objections (a note is NOT one) @@ -28,6 +41,11 @@ REACTION_VERDICT = {"+1": "approve", "-1": "reject"} # ๐Ÿ‘ = approve, ๐Ÿ‘Ž = reject (REST content names) +def is_maintainer(login): + """Is `login` on MAINTAINERS? GitHub logins are case-insensitive.""" + return bool(login) and login.lower() in _MAINTAINERS_LC + + class GhError(RuntimeError): """A gh call failed or answered with nothing usable. Never read it as 'wait': an expired token once kept the poller green and blind for three weeks.""" @@ -88,7 +106,7 @@ def gh_reactions(repo, comment_id): def is_org_member(repo, login): """Is `login` a PUBLIC member of the repo's org? Reaction objects carry no author_association, so this is how a react-only reviewer is recognised as a - maintainer (private members 404 โ€” they fall back to the MAINTAINERS seed). + maintainer (private members 404 โ€” they fall back to the MAINTAINERS list). Cached per run so N reactions by one maintainer cost one API call.""" org = repo.split("/")[0] k = (org, login) @@ -153,6 +171,7 @@ def classify(pr, repo="leanprover-community/mathlib4"): created = dt.datetime.fromisoformat(meta["created_at"].replace("Z", "+00:00")) age_h = (dt.datetime.now(dt.timezone.utc) - created).total_seconds() / 3600 head_sha = meta["head"]["sha"] + author = (meta.get("user") or {}).get("login", "") diff = gh_run(["pr", "diff", str(pr), "--repo", repo]) if not diff.strip(): @@ -170,20 +189,25 @@ def classify(pr, repo="leanprover-community/mathlib4"): decl_line[m.group(1)] = (f, idx) tags = list(dict.fromkeys(tags)) - # explicit[(qid, login)] = (status, ts); notes[(qid, login)] = text - explicit, notes, reviewers = {}, {}, set() - # Maintainers/reviewers: anyone whose GitHub author_association on the PR is an - # org role, seeded by the explicit allowlist. Their verdict trumps, and the + # explicit[(qid, login)] = (status, ts); notes[(qid, login)] = text; + # written[(qid, login)] = (status, ts) of their latest verdict that is not a reaction + explicit, written, notes, reviewers = {}, {}, {}, set() + # Maintainers/reviewers: everyone on MAINTAINERS, plus anyone whose GitHub + # author_association on the PR is an org role. Their verdict trumps, and the # settle gate needs >=1 of them. - maint = set(MAINTAINERS) + maint = set() + def is_maint(login): + return is_maintainer(login) or login in maint def record_assoc(login, assoc): if login and login not in BOTS and assoc in ORG_ROLES: maint.add(login) - def note_explicit(qid, login, status, ts, text=""): + def note_explicit(qid, login, status, ts, text="", reaction=False): if not login or login in BOTS: return reviewers.add(login) k = (qid, login) + if not reaction and (k not in written or ts > written[k][1]): + written[k] = (status, ts) if k not in explicit or ts > explicit[k][1]: explicit[k] = (status, ts) if text: @@ -211,9 +235,9 @@ def note_explicit(qid, login, status, ts, text=""): ru = (r.get("user") or {}).get("login", "") if not v or not ru or ru in BOTS: continue - if ru not in maint and is_org_member(repo, ru): + if not is_maint(ru) and is_org_member(repo, ru): maint.add(ru) # a maintainer's reaction trumps, like a maintainer comment - note_explicit(qid, ru, v, r.get("created_at", "")) + note_explicit(qid, ru, v, r.get("created_at", ""), reaction=True) for c in gh_list(repo, f"issues/{pr}/comments"): u = (c.get("user") or {}).get("login", "") record_assoc(u, c.get("author_association")) @@ -239,7 +263,16 @@ def note_explicit(qid, login, status, ts, text=""): def decide(qid): ex = {u: stt for (q, u), (stt, _) in explicit.items() if q == qid} real = {u: stt for u, stt in ex.items() if stt != "(note)"} - mver = [stt for u, stt in real.items() if u in maint] + mver = [stt for u, stt in real.items() if is_maint(u)] + # The PR author's latest reject/revise/flag stands unless a LISTED maintainer + # wrote a verdict on the tag after it and still holds it. An earlier verdict, a + # reaction alone, or an association-only maintainer no longer overrides it. + a = explicit.get((qid, author)) + if a and a[0] in OBJECT: + def wrote_later(u): + w = written.get((qid, u)) + return w is not None and w[0] == real[u] and w[1] > a[1] + mver = [real[u] for u in real if is_maintainer(u) and wrote_later(u)] if mver: if any(s in OBJECT for s in mver): return "recycle", ex, "maintainer rejected/revised" @@ -270,7 +303,7 @@ def decide(qid): } (green if verdict == "green" else recycle).append(rec) - maint_reviewers = sorted(reviewers & maint) + maint_reviewers = sorted(u for u in reviewers if is_maint(u)) gate_ok = len(reviewers) >= 2 and bool(maint_reviewers) return { "pr": pr, "repo": repo, "head_sha": head_sha, "age_h": round(age_h, 1), @@ -292,8 +325,10 @@ def ready_header(cls): f"and no reject/revise/flag recorded by this bot that a maintainer's verdict did not override " f"(GitHub \"Request changes\" reviews and free-text comments are not counted). Under this bot's " f"rule one approval per tag is enough, and it can be the PR author's own or a single ๐Ÿ‘ reaction. " - f"Only a per-tag verdict or ๐Ÿ‘/๐Ÿ‘Ž from `jcommelin`, `faenuccio` or someone GitHub shows the bot " - f"as a mathlib4 owner, member or collaborator overrides the others; a GitHub PR approval never does. " + f"Only a per-tag verdict or ๐Ÿ‘/๐Ÿ‘Ž from a Mathlib maintainer listed in the bot or someone GitHub " + f"shows the bot as a mathlib4 owner, member or collaborator overrides the others; a GitHub PR " + f"approval never does. The PR author's own reject/revise/flag on a tag is overridden only by a " + f"written verdict a listed maintainer gives on that tag after it. " f"Reviews recorded from: {who}. **Ready for a maintainer's review.**" + (f" {len(recycle)} recycled to the next batch." if recycle else "") + " ") diff --git a/bot/test_poll.py b/bot/test_poll.py index 8de3bcd5c..ca8c4ee18 100644 --- a/bot/test_poll.py +++ b/bot/test_poll.py @@ -38,7 +38,7 @@ def pull(state="open", title="doc: add wikidata attributes (batch 7)", merged=False): return {"number": PR, "state": state, "merged": merged, "merged_at": None, - "title": title, "created_at": "2026-08-10T11:00:00Z", + "title": title, "created_at": "2026-08-10T11:00:00Z", "user": {"login": "Deicyde"}, "head": {"sha": "c" * 40}} @@ -67,7 +67,7 @@ class FakeGh: def __init__(self, *, pr_json=None, state="OPEN", mergeable=("MERGEABLE",), master=MASTER, diff=DIFF, reviews=(), comments=(), issue_comments=(), - checks=(0, CHECKS_GREEN, ""), edits=None, fail=None): + checks=(0, CHECKS_GREEN, ""), edits=None, reactions=None, fail=None): self.pr_json = pr_json if pr_json is not None else pull() self.state = state self.mergeable = list(mergeable) @@ -78,6 +78,7 @@ def __init__(self, *, pr_json=None, state="OPEN", mergeable=("MERGEABLE",), self.issue_comments = list(issue_comments) self.checks = checks self.edits = edits or {} + self.reactions = reactions or {} # {crossref comment id: [reaction, ...]} self.fail = fail self.calls = [] @@ -118,6 +119,8 @@ def route(self, cmd): return 0, lines(self.comments), "" if path == f"repos/{REPO}/issues/{PR}/comments": return 0, lines(self.issue_comments), "" + if path.startswith(f"repos/{REPO}/pulls/comments/") and path.endswith("/reactions"): + return 0, lines(self.reactions.get(int(path.split("/")[-2]), [])), "" if path.startswith("orgs/"): return 1, "", "gh: Not Found (HTTP 404)\n" raise AssertionError(f"unrouted gh call: {cmd}") @@ -314,7 +317,7 @@ def test_settled_conflicting_rebuilds(self): out = io.StringIO() with contextlib.redirect_stdout(out): self.run_with(fake, poll.tick, Path("/unused"), True) - self.assertIn("RESOLVE-CONFLICT #42608: rebuild off fresh master with 2 green tags", out.getvalue()) + self.assertIn("RESOLVE-CONFLICT #42608: rebuild off fresh master with the 2 tags it carries", out.getvalue()) def test_auth_failure_raises(self): self.write_state(settled_pr=PR) @@ -407,9 +410,13 @@ def test_header_states_the_rule_classify_applies(self): self.assertIn("no reject/revise/flag recorded by this bot that a maintainer's verdict did not override", h) self.assertIn('GitHub "Request changes" reviews and free-text comments are not counted', h) self.assertIn("the PR author's own or a single ๐Ÿ‘ reaction", h) - self.assertIn("Only a per-tag verdict or ๐Ÿ‘/๐Ÿ‘Ž from `jcommelin`, `faenuccio` or someone GitHub shows " - "the bot as a mathlib4 owner, member or collaborator overrides the others", h) + self.assertIn("Only a per-tag verdict or ๐Ÿ‘/๐Ÿ‘Ž from a Mathlib maintainer listed in the bot or someone " + "GitHub shows the bot as a mathlib4 owner, member or collaborator overrides the others", h) self.assertIn("a GitHub PR approval never does", h) + self.assertIn("The PR author's own reject/revise/flag on a tag is overridden only by a written verdict " + "a listed maintainer gives on that tag after it.", h) + self.assertNotIn("jcommelin", h) # the list is in the bot, not the header + self.assertNotIn("faenuccio", h) self.assertIn("Reviews recorded from: `Deicyde`, `SnirBroshi`.", h) self.assertIn("1 recycled to the next batch.", h) self.assertNotRegex(h, r"@\w") # names, not pings diff --git a/bot/test_settle_gate.py b/bot/test_settle_gate.py new file mode 100644 index 000000000..7ad1d6344 --- /dev/null +++ b/bot/test_settle_gate.py @@ -0,0 +1,218 @@ +#!/usr/bin/env python3 +"""Per-tag rule in settle.classify(): the PR author's latest reject/revise/flag +stands unless a LISTED maintainer (settle.MAINTAINERS) wrote a verdict on that +tag after it, and every listed maintainer counts as one whatever GitHub's +author_association says. The gate itself is unchanged.""" +from __future__ import annotations + +import contextlib +import io +import unittest +from pathlib import Path + +import poll +import settle +from test_poll import CONFLICT_SHA, PR, REPO, FakeGh, PollFixture + +AUTHOR = "Deicyde" +EARLY = "2026-08-10T12:00:00Z" # a reviewer's reaction, before the author's verdicts +APPROVE_AT = "2026-08-12T00:00:00Z" # a maintainer's written approve, before the author's reject +REJECT_AT = "2026-08-24T00:00:00Z" # the author's written reject +AFTER = "2026-08-25T00:00:00Z" +LATER = "2026-08-30T00:00:00Z" + + +def review(login, state="COMMENTED", assoc="CONTRIBUTOR", at="2026-08-11T00:00:00Z"): + return {"user": {"login": login}, "author_association": assoc, "state": state, "submitted_at": at} + + +def crossref_comment(cid, qid, plus=0, minus=0): + """The bot's per-tag inline comment that reviewers react to.""" + return {"id": cid, "user": {"login": AUTHOR}, "author_association": "CONTRIBUTOR", + "body": f"Cross-reference for {qid} ", + "created_at": "2026-08-10T11:20:00Z", "reactions": {"+1": plus, "-1": minus}} + + +def reaction(login, content="+1", at=EARLY): + return {"content": content, "user": {"login": login}, "created_at": at} + + +def written_verdict(login, qid, status, at=AFTER, assoc="CONTRIBUTOR"): + """An inline WikiLean review comment carrying an explicit verdict.""" + return {"id": 900, "user": {"login": login}, "author_association": assoc, + "body": f" ({status})\n> {status} this tag", "created_at": at} + + +def pasted_review(login, verdicts, at=REJECT_AT): + """The '## WikiLean review' issue comment the operator pastes from the site.""" + lines = ["## WikiLean review", ""] + for qid, status in verdicts.items(): + lines += [f"- **[{qid}]** tag", f" - status: **{status}**", f" - {status} by the operator"] + return {"user": {"login": login}, "author_association": "CONTRIBUTOR", + "body": "\n".join(lines), "created_at": at} + + +AUTHOR_REJECTS_SET = pasted_review(AUTHOR, {"Q36161": "reject"}) + + +class PerTagRuleTest(PollFixture): + def classify(self, **kwargs): + return self.run_with(FakeGh(**kwargs), settle.classify, PR, REPO) + + def verdict(self, r, qid="Q36161"): + tag = next(t for t in r["green"] + r["recycle"] if t["qid"] == qid) + return ("green" if tag in r["green"] else "recycle"), tag["reason"] + + def test_a_maintainer_s_thumbs_down_after_the_author_s_reject_is_not_green(self): + # Written approve, then the author's written reject, then the maintainer's ๐Ÿ‘Ž: + # both now reject, so the tag recycles, with or without a blanket approval. + for blanket in ([], [review("SnirBroshi", "APPROVED")]): + with self.subTest(blanket=bool(blanket)): + r = self.classify( + reviews=blanket, + comments=[written_verdict("jcommelin", "Q36161", "approve", at=APPROVE_AT), + crossref_comment(101, "Q36161", minus=1)], + reactions={101: [reaction("jcommelin", "-1", LATER)]}, + issue_comments=[AUTHOR_REJECTS_SET]) + self.assertEqual(self.verdict(r)[0], "recycle") + + def test_a_collaborator_s_thumbs_up_before_the_author_s_reject_recycles(self): + r = self.classify(reviews=[review("SnirBroshi", assoc="COLLABORATOR")], + comments=[crossref_comment(101, "Q36161", plus=1)], + reactions={101: [reaction("SnirBroshi")]}, + issue_comments=[AUTHOR_REJECTS_SET]) + self.assertEqual(self.verdict(r), ("recycle", "objection (reject/revise)")) + + def test_a_listed_maintainer_s_thumbs_up_before_the_author_s_reject_recycles(self): + r = self.classify(comments=[crossref_comment(101, "Q36161", plus=1)], + reactions={101: [reaction("jcommelin")]}, + issue_comments=[AUTHOR_REJECTS_SET]) + self.assertEqual(self.verdict(r), ("recycle", "objection (reject/revise)")) + + def test_a_listed_maintainer_s_reaction_alone_never_overrides_the_author(self): + fake = FakeGh(comments=[crossref_comment(101, "Q36161", plus=1)], + reactions={101: [reaction("jcommelin", "+1", LATER)]}, + issue_comments=[AUTHOR_REJECTS_SET]) + r = self.run_with(fake, settle.classify, PR, REPO) + self.assertEqual(self.verdict(r), ("recycle", "objection (reject/revise)")) + self.assertFalse([c for c in fake.calls if c[1] == "api" and c[2].startswith("orgs/")]) + + def test_a_maintainer_s_earlier_written_approve_loses_to_the_author_s_later_reject(self): + r = self.classify(comments=[written_verdict("jcommelin", "Q36161", "approve", at=APPROVE_AT)], + issue_comments=[AUTHOR_REJECTS_SET]) + self.assertEqual(self.verdict(r), ("recycle", "objection (reject/revise)")) + + def test_a_listed_maintainer_s_written_approve_after_the_author_s_reject_is_green(self): + for login in ("jcommelin", "JCommelin", "grunweg"): # grunweg's membership is private + with self.subTest(login=login): + r = self.classify(comments=[written_verdict(login, "Q36161", "approve")], + issue_comments=[AUTHOR_REJECTS_SET]) + self.assertEqual(self.verdict(r), ("green", "maintainer approved")) + + def test_a_same_meaning_reaction_after_that_written_approve_keeps_it_green(self): + r = self.classify(comments=[written_verdict("jcommelin", "Q36161", "approve"), + crossref_comment(101, "Q36161", plus=1)], + reactions={101: [reaction("jcommelin", "+1", LATER)]}, + issue_comments=[AUTHOR_REJECTS_SET]) + self.assertEqual(self.verdict(r), ("green", "maintainer approved")) + + def test_a_thumbs_down_after_that_written_approve_recycles(self): + r = self.classify(comments=[written_verdict("jcommelin", "Q36161", "approve"), + crossref_comment(101, "Q36161", minus=1)], + reactions={101: [reaction("jcommelin", "-1", LATER)]}, + issue_comments=[AUTHOR_REJECTS_SET]) + self.assertEqual(self.verdict(r)[0], "recycle") + + def test_an_association_only_maintainer_does_not_override_the_author(self): + r = self.classify(reviews=[review("SnirBroshi", assoc="COLLABORATOR")], + comments=[written_verdict("SnirBroshi", "Q36161", "approve", at=LATER, + assoc="COLLABORATOR")], + issue_comments=[AUTHOR_REJECTS_SET]) + self.assertEqual(self.verdict(r), ("recycle", "objection (reject/revise)")) + + def test_the_author_retracting_lifts_the_objection(self): + r = self.classify(comments=[crossref_comment(101, "Q36161", plus=1)], + reactions={101: [reaction(AUTHOR, "+1", LATER)]}, + issue_comments=[AUTHOR_REJECTS_SET]) + self.assertEqual(self.verdict(r), ("green", "approved (>=1 review, no objection)")) + + def test_a_private_listed_maintainer_s_reject_beats_a_collaborator_s_thumbs_up(self): + # grunweg's org membership is private, so GitHub shows CONTRIBUTOR and the + # members probe 404s; only the list makes the reject a maintainer's. + r = self.classify(reviews=[review("SnirBroshi", assoc="COLLABORATOR")], + comments=[crossref_comment(101, "Q36161", plus=1), + written_verdict("grunweg", "Q36161", "reject")], + reactions={101: [reaction("SnirBroshi")]}) + self.assertEqual(self.verdict(r), ("recycle", "maintainer rejected/revised")) + self.assertEqual(r["maintainer_reviewers"], ["SnirBroshi", "grunweg"]) + + def test_a_collaborator_s_thumbs_up_still_overrides_a_non_author_s_reject(self): + # Unchanged: an association-only maintainer trumps everyone but the PR author, + # and the gate still opens on the author plus that collaborator. + r = self.classify(reviews=[review("SnirBroshi", assoc="COLLABORATOR")], + comments=[crossref_comment(101, "Q36161", plus=1), + written_verdict("someone", "Q36161", "reject")], + reactions={101: [reaction("SnirBroshi")]}, + issue_comments=[pasted_review(AUTHOR, {"Q474715": "approve"})]) + self.assertEqual(self.verdict(r), ("green", "maintainer approved")) + r = self.classify(reviews=[review("SnirBroshi", assoc="COLLABORATOR")], + comments=[crossref_comment(101, "Q36161", plus=1)], + reactions={101: [reaction("SnirBroshi")]}, + issue_comments=[pasted_review(AUTHOR, {"Q474715": "approve"})]) + self.assertEqual(r["reviewers"], [AUTHOR, "SnirBroshi"]) + self.assertTrue(r["gate"]) + + def test_listed_maintainers_count_whatever_the_association(self): + r = self.classify(reviews=[review("GrunWeg", "APPROVED")], + issue_comments=[pasted_review(AUTHOR, {"Q36161": "approve"})]) + self.assertEqual(r["maintainer_reviewers"], ["GrunWeg"]) + self.assertTrue(r["gate"]) + self.assertEqual(len(settle.MAINTAINERS), 28) + self.assertTrue(settle.is_maintainer("remydegenne")) + self.assertFalse(settle.is_maintainer("SnirBroshi")) + self.assertFalse(settle.is_maintainer("")) + + +DIFF_42608 = "".join(f"+++ b/Mathlib/F{i}.lean\n+@[wikidata {q}]\n" for i, q in enumerate( + ["Q166154", "Q994399", "Q124247109", "Q24743362", "Q332791", "Q36161", "Q474715", + "Q1474074", "Q1070472"])) + + +class Pr42608ReplayTest(PollFixture): + def test_set_and_partial_order_recycle_and_the_rest_stay_green(self): + # mathlib4#42608's verdict shape: a Mathlib reviewer (association COLLABORATOR) + # approved three tags (as ๐Ÿ‘ here) before the author's pasted WikiLean review, + # which approved seven and rejected Set and PartialOrder. + approved = ["Q166154", "Q994399", "Q124247109", "Q24743362", "Q332791", "Q1474074", "Q1070472"] + thumbs = {"Q24743362": 101, "Q36161": 102, "Q474715": 103} + r = self.run_with(FakeGh( + diff=DIFF_42608, + reviews=[review("SnirBroshi", assoc="COLLABORATOR")], + comments=[crossref_comment(cid, q, plus=1) for q, cid in thumbs.items()], + reactions={cid: [reaction("SnirBroshi")] for cid in thumbs.values()}, + issue_comments=[pasted_review(AUTHOR, {**{q: "approve" for q in approved}, + "Q36161": "reject", "Q474715": "reject"})]), + settle.classify, PR, REPO) + self.assertTrue(r["gate"]) # the gate is unchanged: author + a collaborator + self.assertEqual([g["qid"] for g in r["green"]], approved) + self.assertEqual([(t["qid"], t["reason"]) for t in r["recycle"]], + [("Q36161", "objection (reject/revise)"), ("Q474715", "objection (reject/revise)")]) + h = settle.ready_header(r) + self.assertIn("**7** `@[wikidata]` tags", h) + self.assertIn("2 recycled to the next batch.", h) + + +class ConflictRebuildTest(PollFixture): + def test_a_rebuild_keeps_every_tag_on_the_pr(self): + # With the gate closed nothing trims or triages a recycled tag, so the conflict + # rebuild must re-apply it rather than drop it. + self.write_state(settled_pr=PR, conflict_sha=CONFLICT_SHA) + fake = FakeGh(mergeable=("CONFLICTING",), issue_comments=[AUTHOR_REJECTS_SET]) + out = io.StringIO() + with contextlib.redirect_stdout(out): + self.run_with(fake, poll.tick, Path("/unused"), True) + self.assertIn("rebuild off fresh master with the 2 tags it carries", out.getvalue()) + + +if __name__ == "__main__": + unittest.main() diff --git a/scripts/ci-python.sh b/scripts/ci-python.sh index d0ccdc632..d7500e6d1 100755 --- a/scripts/ci-python.sh +++ b/scripts/ci-python.sh @@ -119,6 +119,7 @@ run_check "Brain nightly shell tests" "$PYTHON_BIN" site/ops/test_brain_nightly. run_check "Frontier suitability policy tests" "$PYTHON_BIN" brain/test_frontier_suitability.py run_check "Frontier generated-page contract" "$PYTHON_BIN" site/test_frontier_page.py run_check "Bot poller fail-closed tests" "$PYTHON_BIN" bot/test_poll.py +run_check "Bot settle per-tag rule tests" "$PYTHON_BIN" bot/test_settle_gate.py run_check "Bot state branch tests" "$PYTHON_BIN" bot/test_state_branch.py printf '\nCI Python summary: %s commands passed; all required offline scenarios ran.\n' "$CHECKS_PASSED" From 7e4a7681eecfc6f7bfaa9448bf83a41945cca92c Mon Sep 17 00:00:00 2001 From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com> Date: Thu, 15 Oct 2026 00:20:25 -0400 Subject: [PATCH 4/7] bot: keep every maintainer's objection when the author objects MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The previous commit replaced the maintainer verdicts on a tag with only the listed maintainers who wrote after the author's objection. That also threw away every other maintainer's live objection: a listed maintainer's ๐Ÿ‘Ž, a reject written before the author's, or a collaborator's ๐Ÿ‘Ž. With the author's reject added, such a tag could go green where it recycles without it, the same kind of lost ๐Ÿ‘Ž that sank the earlier draft. Only the approvals that may override the author are narrowed now; every maintainer's objection still counts, the author's own included when GitHub shows them an org role. With the same maintainers, the exception can no longer green a tag that main's rule recycles. Co-Authored-By: Claude Opus 5.5 --- bot/settle.py | 6 +++++- bot/test_settle_gate.py | 33 +++++++++++++++++++++++++++++++++ 2 files changed, 38 insertions(+), 1 deletion(-) diff --git a/bot/settle.py b/bot/settle.py index 685eb46f5..45e10babb 100644 --- a/bot/settle.py +++ b/bot/settle.py @@ -267,12 +267,16 @@ def decide(qid): # The PR author's latest reject/revise/flag stands unless a LISTED maintainer # wrote a verdict on the tag after it and still holds it. An earlier verdict, a # reaction alone, or an association-only maintainer no longer overrides it. + # Only the approvals that can override it are narrowed: every maintainer's + # objection still counts, so no tag goes green that the same maintainers would + # recycle without this exception. a = explicit.get((qid, author)) if a and a[0] in OBJECT: def wrote_later(u): w = written.get((qid, u)) return w is not None and w[0] == real[u] and w[1] > a[1] - mver = [real[u] for u in real if is_maintainer(u) and wrote_later(u)] + mver = [s for u, s in real.items() + if (is_maint(u) and s in OBJECT) or (is_maintainer(u) and wrote_later(u))] if mver: if any(s in OBJECT for s in mver): return "recycle", ex, "maintainer rejected/revised" diff --git a/bot/test_settle_gate.py b/bot/test_settle_gate.py index 7ad1d6344..0fc1720a6 100644 --- a/bot/test_settle_gate.py +++ b/bot/test_settle_gate.py @@ -123,6 +123,39 @@ def test_a_thumbs_down_after_that_written_approve_recycles(self): issue_comments=[AUTHOR_REJECTS_SET]) self.assertEqual(self.verdict(r)[0], "recycle") + def test_the_author_s_reject_never_drops_another_maintainer_s_objection(self): + # A listed maintainer's written approve comes after the author's reject, but + # another maintainer objects too: a listed one by ๐Ÿ‘Ž, a listed MEMBER in writing + # before the author, or a collaborator by ๐Ÿ‘Ž. Each recycles, as it does when the + # author never rejected. + approve_after = written_verdict("jcommelin", "Q36161", "approve") + shapes = { + "listed ๐Ÿ‘Ž later": dict( + comments=[approve_after, crossref_comment(101, "Q36161", minus=1)], + reactions={101: [reaction("kbuzzard", "-1", LATER)]}), + "listed written reject earlier": dict( + comments=[written_verdict("sgouezel", "Q36161", "reject", at=APPROVE_AT, + assoc="MEMBER"), approve_after]), + "collaborator ๐Ÿ‘Ž later": dict( + reviews=[review("SnirBroshi", assoc="COLLABORATOR")], + comments=[approve_after, crossref_comment(101, "Q36161", minus=1)], + reactions={101: [reaction("SnirBroshi", "-1", LATER)]}), + } + for name, shape in shapes.items(): + for author_rejects in (False, True): + with self.subTest(shape=name, author_rejects=author_rejects): + r = self.classify(**shape, + issue_comments=[AUTHOR_REJECTS_SET] if author_rejects else []) + self.assertEqual(self.verdict(r), ("recycle", "maintainer rejected/revised")) + + def test_an_author_with_an_org_role_keeps_a_maintainer_s_objection(self): + # Unchanged: if GitHub shows the author as a collaborator, their reject is a + # maintainer's, and not even a listed maintainer's later written approve lifts it. + r = self.classify(reviews=[review(AUTHOR, assoc="COLLABORATOR")], + comments=[written_verdict("jcommelin", "Q36161", "approve")], + issue_comments=[AUTHOR_REJECTS_SET]) + self.assertEqual(self.verdict(r), ("recycle", "maintainer rejected/revised")) + def test_an_association_only_maintainer_does_not_override_the_author(self): r = self.classify(reviews=[review("SnirBroshi", assoc="COLLABORATOR")], comments=[written_verdict("SnirBroshi", "Q36161", "approve", at=LATER, From f4f1b639fcc4602ec8d62f32ffbb8cf1b4b04dfd Mon Sep 17 00:00:00 2001 From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com> Date: Thu, 15 Oct 2026 00:20:25 -0400 Subject: [PATCH 5/7] bot: name resolve_conflicts' tag set for what it holds Since the rebuild re-applies every tag on the PR, green_qids and green no longer hold the green set. Rename them to pr_qids and carried (and green_files to carried_files) so the code reads like its comments. The reapply_green.json state file keeps its name. Co-Authored-By: Claude Opus 5.5 --- bot/poll.py | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/bot/poll.py b/bot/poll.py index cc298e1c6..7259249ef 100644 --- a/bot/poll.py +++ b/bot/poll.py @@ -161,10 +161,10 @@ def resolve_conflicts(pr, branch, mathlib, dry): # not approved minus recycled, which would re-add trimmed tags, and not the green set: # trimming belongs to the settle (triage, requeue, table), and a tag that recycles # while the gate is closed must not silently vanish here. decl/file from approved. - green_qids = set(cls["tags"]) - green = {"branch": branch, "title": approved.get("title", "doc: add wikidata attributes"), - "tags": [t for t in approved["tags"] if t["qid"] in green_qids]} - print(f" RESOLVE-CONFLICT #{pr}: rebuild off fresh master with the {len(green['tags'])} tags it carries") + pr_qids = set(cls["tags"]) + carried = {"branch": branch, "title": approved.get("title", "doc: add wikidata attributes"), + "tags": [t for t in approved["tags"] if t["qid"] in pr_qids]} + print(f" RESOLVE-CONFLICT #{pr}: rebuild off fresh master with the {len(carried['tags'])} tags it carries") if dry: return sh(["git", "-C", str(mathlib), "fetch", "origin", branch], check=True) # --force-with-lease base @@ -176,16 +176,16 @@ def resolve_conflicts(pr, branch, mathlib, dry): # foundational modules (it ran 80m+ on #40861 before timing out). The original build # already proved which files need the CrossRefAttribute import; re-add exactly those # and let mathlib CI do the compile check. - green_files = {t["file"] for t in green["tags"]} + carried_files = {t["file"] for t in carried["tags"]} gr = subprocess.run(["git", "-C", str(mathlib), "grep", "-l", "Mathlib.Tactic.CrossRefAttribute", f"origin/{branch}", "--", "Mathlib"], capture_output=True, text=True).stdout.split() - green["import_files"] = sorted({f.split(":", 1)[1] for f in gr if ":" in f} & green_files) + carried["import_files"] = sorted({f.split(":", 1)[1] for f in gr if ":" in f} & carried_files) # Record the master we rebuild ONTO *before* the fallible push, so a failed rebuild # doesn't re-loop every tick at the same master โ€” it retries only when master advances. stt = json.loads(STATE.read_text()); stt["conflict_sha"] = rebuilt; stt.pop("retriggered_pr", None) STATE.write_text(json.dumps(stt, indent=1)) gpath = HERE / "state" / "reapply_green.json" - gpath.write_text(json.dumps(green, indent=1)) + gpath.write_text(json.dumps(carried, indent=1)) sh(["git", "-C", str(mathlib), "checkout", "-B", branch, "FETCH_HEAD"], check=True) sh([sys.executable, str(HERE / "open_batch_pr.py"), "--approved", str(gpath), "--mathlib", str(mathlib), "--repo", REPO, "--base", "master", @@ -196,7 +196,7 @@ def resolve_conflicts(pr, branch, mathlib, dry): # `gh pr diff` and no GitHub diff-recompute lag right after the force-push). import pr_table sh([sys.executable, str(HERE / "pr_table.py"), str(pr), "--repo", REPO, "--post", "--no-body-sync"], check=False) - pr_table.sync_body_count(pr, REPO, n=len(green["tags"])) + pr_table.sync_body_count(pr, REPO, n=len(carried["tags"])) def do_open(mathlib, dry): From dd23e9e6129d9fbef12c02ad4050db34d5ecf3bb Mon Sep 17 00:00:00 2001 From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com> Date: Sat, 17 Oct 2026 16:40:04 -0400 Subject: [PATCH 6/7] bot/test_settle_gate.py: test the guard that a maintainer still holds their later written verdict A listed maintainer writes reject after the author's reject, then reacts thumbs-up. Their latest verdict is the thumbs-up, but no written approve backs it, so it must not override the author's objection. With the w[0] == real[u] check in wrote_later removed, this input turned green and all 17 existing tests still passed; this test fails then. --- bot/test_settle_gate.py | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/bot/test_settle_gate.py b/bot/test_settle_gate.py index 0fc1720a6..768f716c5 100644 --- a/bot/test_settle_gate.py +++ b/bot/test_settle_gate.py @@ -123,6 +123,16 @@ def test_a_thumbs_down_after_that_written_approve_recycles(self): issue_comments=[AUTHOR_REJECTS_SET]) self.assertEqual(self.verdict(r)[0], "recycle") + def test_a_thumbs_up_that_contradicts_the_maintainer_s_later_written_verdict_recycles(self): + # The override needs the listed maintainer's written verdict after the author's + # reject to be the one they still hold. Here they wrote reject, then reacted ๐Ÿ‘: + # the ๐Ÿ‘ is their latest verdict, but no written approve backs it. + r = self.classify(comments=[written_verdict("kbuzzard", "Q36161", "reject"), + crossref_comment(101, "Q36161", plus=1)], + reactions={101: [reaction("kbuzzard", "+1", LATER)]}, + issue_comments=[AUTHOR_REJECTS_SET]) + self.assertEqual(self.verdict(r), ("recycle", "objection (reject/revise)")) + def test_the_author_s_reject_never_drops_another_maintainer_s_objection(self): # A listed maintainer's written approve comes after the author's reject, but # another maintainer objects too: a listed one by ๐Ÿ‘Ž, a listed MEMBER in writing From 32c4436d6386f014bd8729c0f1169b28d2cbf5fb Mon Sep 17 00:00:00 2001 From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com> Date: Sat, 17 Oct 2026 17:04:50 -0400 Subject: [PATCH 7/7] bot: no author privilege in the settle rule The PR author's reject no longer stands against maintainers. As on main, a maintainer's verdict beats it whenever and however it was given: a reaction or a written verdict, earlier or later, from a listed maintainer or one recognised by association. The carve-out goes, and with it the written-verdict bookkeeping it used, the ready header's sentence and the README line. The gate is unchanged: the author still counts as one of the two reviewers. Kept: the 28-login MAINTAINERS list (case-insensitive) and the conflict rebuild that keeps every tag on the PR. The carve-out tests now assert the opposite: a collaborator's earlier thumbs-up, a listed maintainer's later thumbs-up, a listed maintainer's earlier written approve and a collaborator's later written approve each beat the author's reject. The guard test goes with the guard. The mathlib4#42608 replay keeps all nine tags green. Also corrects pr_table.sync_body_count's docstring: the rebuild no longer shrinks the diff. --- bot/README.md | 2 - bot/pr_table.py | 4 +- bot/settle.py | 37 +++------- bot/test_poll.py | 4 +- bot/test_settle_gate.py | 149 ++++++++++++++++------------------------ 5 files changed, 70 insertions(+), 126 deletions(-) diff --git a/bot/README.md b/bot/README.md index 5dfb39ec7..95f07718b 100644 --- a/bot/README.md +++ b/bot/README.md @@ -29,8 +29,6 @@ Each run does two phases: - A bare **note/comment = "defer to the other reviewer"** โ†’ ignored. - A **maintainer's explicit approve/reject/revise/flag trumps** everything. -- Except: the **PR author's reject/revise/flag** stands unless a maintainer listed - in `MAINTAINERS` writes a verdict on that tag after it (a ๐Ÿ‘/๐Ÿ‘Ž alone does not). - Otherwise: any **reject/revise/flag โ†’ recycle**; else **โ‰ฅ1 approve โ†’ green**; else (no review) โ†’ recycle. diff --git a/bot/pr_table.py b/bot/pr_table.py index 55c3b2d50..37585b8fb 100644 --- a/bot/pr_table.py +++ b/bot/pr_table.py @@ -88,8 +88,8 @@ def post(pr, repo, body): def sync_body_count(pr, repo, n=None): """Keep the PR body's 'adds a batch of N `@[wikidata]` attributes' line in sync with the tags ACTUALLY in the PR's current diff. That line is written once at open; the - settle-trim (split.py) and the conflict-rebuild (poll.resolve_conflicts) both shrink - the diff but never touch the body, so without this it overstates after a trim. + settle-trim (split.py) shrinks the diff and the conflict-rebuild (poll.resolve_conflicts) + re-derives it, but neither touches the body, so without this it overstates after a trim. n defaults to a fresh count of @[wikidata] attribute occurrences in `gh pr diff`: anchored to `@[` so a QID mentioned in added prose isn't counted, and via findall so a diff --git a/bot/settle.py b/bot/settle.py index 45e10babb..336a4b62b 100644 --- a/bot/settle.py +++ b/bot/settle.py @@ -9,10 +9,7 @@ included, >=1 of them a "maintainer": MAINTAINERS, an OWNER/MEMBER/COLLABORATOR association on the PR, or a public org member who reacted. No PR age is checked. - A bare note/comment = "defer to the other reviewer" -> ignored. - - A maintainer's explicit approve/reject/revise/flag (a ๐Ÿ‘/๐Ÿ‘Ž reaction included) TRUMPS, - except that the PR author's latest reject/revise/flag on a tag stands unless a - LISTED maintainer (MAINTAINERS) wrote a verdict on that tag after it (a reaction - alone never overrides it). + - A maintainer's explicit approve/reject/revise/flag (a ๐Ÿ‘/๐Ÿ‘Ž reaction included) TRUMPS. - Else: any reject/revise/flag -> recycle; else >=1 approve (the author's own included) -> green; else recycle. """ @@ -24,8 +21,8 @@ # Needed for maintainers whose org membership is PRIVATE: their author_association # shows CONTRIBUTOR and the members probe 404s, so without the list their verdicts # lose the maintainer trump โ€” batch 6 bug: faenuccio's post-settle rejects were -# trumped by an earlier approve and never re-trimmed the PR. Only a listed -# maintainer overrides the PR author's objection. Update it when the team changes. +# trumped by an earlier approve and never re-trimmed the PR. Update it when the +# team changes. MAINTAINERS = frozenset({ "adamtopaz", "ADedecker", "adomani", "b-mehta", "bryangingechen", "digama0", "dupuisf", "eric-wieser", "faenuccio", "fpvandoorn", "grunweg", "hrmacbeth", @@ -171,7 +168,6 @@ def classify(pr, repo="leanprover-community/mathlib4"): created = dt.datetime.fromisoformat(meta["created_at"].replace("Z", "+00:00")) age_h = (dt.datetime.now(dt.timezone.utc) - created).total_seconds() / 3600 head_sha = meta["head"]["sha"] - author = (meta.get("user") or {}).get("login", "") diff = gh_run(["pr", "diff", str(pr), "--repo", repo]) if not diff.strip(): @@ -189,9 +185,8 @@ def classify(pr, repo="leanprover-community/mathlib4"): decl_line[m.group(1)] = (f, idx) tags = list(dict.fromkeys(tags)) - # explicit[(qid, login)] = (status, ts); notes[(qid, login)] = text; - # written[(qid, login)] = (status, ts) of their latest verdict that is not a reaction - explicit, written, notes, reviewers = {}, {}, {}, set() + # explicit[(qid, login)] = (status, ts); notes[(qid, login)] = text + explicit, notes, reviewers = {}, {}, set() # Maintainers/reviewers: everyone on MAINTAINERS, plus anyone whose GitHub # author_association on the PR is an org role. Their verdict trumps, and the # settle gate needs >=1 of them. @@ -201,13 +196,11 @@ def is_maint(login): def record_assoc(login, assoc): if login and login not in BOTS and assoc in ORG_ROLES: maint.add(login) - def note_explicit(qid, login, status, ts, text="", reaction=False): + def note_explicit(qid, login, status, ts, text=""): if not login or login in BOTS: return reviewers.add(login) k = (qid, login) - if not reaction and (k not in written or ts > written[k][1]): - written[k] = (status, ts) if k not in explicit or ts > explicit[k][1]: explicit[k] = (status, ts) if text: @@ -237,7 +230,7 @@ def note_explicit(qid, login, status, ts, text="", reaction=False): continue if not is_maint(ru) and is_org_member(repo, ru): maint.add(ru) # a maintainer's reaction trumps, like a maintainer comment - note_explicit(qid, ru, v, r.get("created_at", ""), reaction=True) + note_explicit(qid, ru, v, r.get("created_at", "")) for c in gh_list(repo, f"issues/{pr}/comments"): u = (c.get("user") or {}).get("login", "") record_assoc(u, c.get("author_association")) @@ -264,19 +257,6 @@ def decide(qid): ex = {u: stt for (q, u), (stt, _) in explicit.items() if q == qid} real = {u: stt for u, stt in ex.items() if stt != "(note)"} mver = [stt for u, stt in real.items() if is_maint(u)] - # The PR author's latest reject/revise/flag stands unless a LISTED maintainer - # wrote a verdict on the tag after it and still holds it. An earlier verdict, a - # reaction alone, or an association-only maintainer no longer overrides it. - # Only the approvals that can override it are narrowed: every maintainer's - # objection still counts, so no tag goes green that the same maintainers would - # recycle without this exception. - a = explicit.get((qid, author)) - if a and a[0] in OBJECT: - def wrote_later(u): - w = written.get((qid, u)) - return w is not None and w[0] == real[u] and w[1] > a[1] - mver = [s for u, s in real.items() - if (is_maint(u) and s in OBJECT) or (is_maintainer(u) and wrote_later(u))] if mver: if any(s in OBJECT for s in mver): return "recycle", ex, "maintainer rejected/revised" @@ -331,8 +311,7 @@ def ready_header(cls): f"rule one approval per tag is enough, and it can be the PR author's own or a single ๐Ÿ‘ reaction. " f"Only a per-tag verdict or ๐Ÿ‘/๐Ÿ‘Ž from a Mathlib maintainer listed in the bot or someone GitHub " f"shows the bot as a mathlib4 owner, member or collaborator overrides the others; a GitHub PR " - f"approval never does. The PR author's own reject/revise/flag on a tag is overridden only by a " - f"written verdict a listed maintainer gives on that tag after it. " + f"approval never does. " f"Reviews recorded from: {who}. **Ready for a maintainer's review.**" + (f" {len(recycle)} recycled to the next batch." if recycle else "") + " ") diff --git a/bot/test_poll.py b/bot/test_poll.py index ca8c4ee18..4df99e834 100644 --- a/bot/test_poll.py +++ b/bot/test_poll.py @@ -38,7 +38,7 @@ def pull(state="open", title="doc: add wikidata attributes (batch 7)", merged=False): return {"number": PR, "state": state, "merged": merged, "merged_at": None, - "title": title, "created_at": "2026-08-10T11:00:00Z", "user": {"login": "Deicyde"}, + "title": title, "created_at": "2026-08-10T11:00:00Z", "head": {"sha": "c" * 40}} @@ -413,8 +413,6 @@ def test_header_states_the_rule_classify_applies(self): self.assertIn("Only a per-tag verdict or ๐Ÿ‘/๐Ÿ‘Ž from a Mathlib maintainer listed in the bot or someone " "GitHub shows the bot as a mathlib4 owner, member or collaborator overrides the others", h) self.assertIn("a GitHub PR approval never does", h) - self.assertIn("The PR author's own reject/revise/flag on a tag is overridden only by a written verdict " - "a listed maintainer gives on that tag after it.", h) self.assertNotIn("jcommelin", h) # the list is in the bot, not the header self.assertNotIn("faenuccio", h) self.assertIn("Reviews recorded from: `Deicyde`, `SnirBroshi`.", h) diff --git a/bot/test_settle_gate.py b/bot/test_settle_gate.py index 768f716c5..87ceee752 100644 --- a/bot/test_settle_gate.py +++ b/bot/test_settle_gate.py @@ -1,8 +1,8 @@ #!/usr/bin/env python3 -"""Per-tag rule in settle.classify(): the PR author's latest reject/revise/flag -stands unless a LISTED maintainer (settle.MAINTAINERS) wrote a verdict on that -tag after it, and every listed maintainer counts as one whatever GitHub's -author_association says. The gate itself is unchanged.""" +"""Per-tag rule in settle.classify(): every listed maintainer (settle.MAINTAINERS) +counts as one whatever GitHub's author_association says, and the PR author gets no +more say than any other reviewer: a maintainer's verdict beats theirs whenever and +however it was given. The gate itself is unchanged.""" from __future__ import annotations import contextlib @@ -63,9 +63,41 @@ def verdict(self, r, qid="Q36161"): tag = next(t for t in r["green"] + r["recycle"] if t["qid"] == qid) return ("green" if tag in r["green"] else "recycle"), tag["reason"] - def test_a_maintainer_s_thumbs_down_after_the_author_s_reject_is_not_green(self): + def test_a_maintainer_s_approve_beats_the_author_s_reject(self): + # The author is reviewed like anyone else: a maintainer's approve wins whether + # it came before or after the author's reject, as a ๐Ÿ‘ or written, and whether + # the maintainer is listed or recognised by association. + collaborator = [review("SnirBroshi", assoc="COLLABORATOR")] + shapes = { + "collaborator ๐Ÿ‘ earlier": dict( + reviews=collaborator, comments=[crossref_comment(101, "Q36161", plus=1)], + reactions={101: [reaction("SnirBroshi")]}), + "listed ๐Ÿ‘ later": dict( + comments=[crossref_comment(101, "Q36161", plus=1)], + reactions={101: [reaction("jcommelin", "+1", LATER)]}), + "listed written approve earlier": dict( + comments=[written_verdict("jcommelin", "Q36161", "approve", at=APPROVE_AT)]), + "collaborator written approve later": dict( + reviews=collaborator, + comments=[written_verdict("SnirBroshi", "Q36161", "approve", at=LATER, + assoc="COLLABORATOR")]), + } + for name, shape in shapes.items(): + with self.subTest(shape=name): + r = self.classify(**shape, issue_comments=[AUTHOR_REJECTS_SET]) + self.assertEqual(self.verdict(r), ("green", "maintainer approved")) + + def test_a_listed_maintainer_s_reaction_needs_no_org_probe(self): + fake = FakeGh(comments=[crossref_comment(101, "Q36161", plus=1)], + reactions={101: [reaction("jcommelin", "+1", LATER)]}, + issue_comments=[AUTHOR_REJECTS_SET]) + r = self.run_with(fake, settle.classify, PR, REPO) + self.assertEqual(self.verdict(r), ("green", "maintainer approved")) + self.assertFalse([c for c in fake.calls if c[1] == "api" and c[2].startswith("orgs/")]) + + def test_a_maintainer_s_later_thumbs_down_replaces_their_written_approve(self): # Written approve, then the author's written reject, then the maintainer's ๐Ÿ‘Ž: - # both now reject, so the tag recycles, with or without a blanket approval. + # the maintainer now rejects, so the tag recycles, with or without a blanket approval. for blanket in ([], [review("SnirBroshi", "APPROVED")]): with self.subTest(blanket=bool(blanket)): r = self.classify( @@ -74,70 +106,18 @@ def test_a_maintainer_s_thumbs_down_after_the_author_s_reject_is_not_green(self) crossref_comment(101, "Q36161", minus=1)], reactions={101: [reaction("jcommelin", "-1", LATER)]}, issue_comments=[AUTHOR_REJECTS_SET]) - self.assertEqual(self.verdict(r)[0], "recycle") - - def test_a_collaborator_s_thumbs_up_before_the_author_s_reject_recycles(self): - r = self.classify(reviews=[review("SnirBroshi", assoc="COLLABORATOR")], - comments=[crossref_comment(101, "Q36161", plus=1)], - reactions={101: [reaction("SnirBroshi")]}, - issue_comments=[AUTHOR_REJECTS_SET]) - self.assertEqual(self.verdict(r), ("recycle", "objection (reject/revise)")) - - def test_a_listed_maintainer_s_thumbs_up_before_the_author_s_reject_recycles(self): - r = self.classify(comments=[crossref_comment(101, "Q36161", plus=1)], - reactions={101: [reaction("jcommelin")]}, - issue_comments=[AUTHOR_REJECTS_SET]) - self.assertEqual(self.verdict(r), ("recycle", "objection (reject/revise)")) + self.assertEqual(self.verdict(r), ("recycle", "maintainer rejected/revised")) - def test_a_listed_maintainer_s_reaction_alone_never_overrides_the_author(self): - fake = FakeGh(comments=[crossref_comment(101, "Q36161", plus=1)], - reactions={101: [reaction("jcommelin", "+1", LATER)]}, - issue_comments=[AUTHOR_REJECTS_SET]) - r = self.run_with(fake, settle.classify, PR, REPO) - self.assertEqual(self.verdict(r), ("recycle", "objection (reject/revise)")) - self.assertFalse([c for c in fake.calls if c[1] == "api" and c[2].startswith("orgs/")]) - - def test_a_maintainer_s_earlier_written_approve_loses_to_the_author_s_later_reject(self): - r = self.classify(comments=[written_verdict("jcommelin", "Q36161", "approve", at=APPROVE_AT)], - issue_comments=[AUTHOR_REJECTS_SET]) - self.assertEqual(self.verdict(r), ("recycle", "objection (reject/revise)")) - - def test_a_listed_maintainer_s_written_approve_after_the_author_s_reject_is_green(self): + def test_listed_maintainers_match_whatever_the_login_case_or_membership(self): for login in ("jcommelin", "JCommelin", "grunweg"): # grunweg's membership is private with self.subTest(login=login): r = self.classify(comments=[written_verdict(login, "Q36161", "approve")], issue_comments=[AUTHOR_REJECTS_SET]) self.assertEqual(self.verdict(r), ("green", "maintainer approved")) - def test_a_same_meaning_reaction_after_that_written_approve_keeps_it_green(self): - r = self.classify(comments=[written_verdict("jcommelin", "Q36161", "approve"), - crossref_comment(101, "Q36161", plus=1)], - reactions={101: [reaction("jcommelin", "+1", LATER)]}, - issue_comments=[AUTHOR_REJECTS_SET]) - self.assertEqual(self.verdict(r), ("green", "maintainer approved")) - - def test_a_thumbs_down_after_that_written_approve_recycles(self): - r = self.classify(comments=[written_verdict("jcommelin", "Q36161", "approve"), - crossref_comment(101, "Q36161", minus=1)], - reactions={101: [reaction("jcommelin", "-1", LATER)]}, - issue_comments=[AUTHOR_REJECTS_SET]) - self.assertEqual(self.verdict(r)[0], "recycle") - - def test_a_thumbs_up_that_contradicts_the_maintainer_s_later_written_verdict_recycles(self): - # The override needs the listed maintainer's written verdict after the author's - # reject to be the one they still hold. Here they wrote reject, then reacted ๐Ÿ‘: - # the ๐Ÿ‘ is their latest verdict, but no written approve backs it. - r = self.classify(comments=[written_verdict("kbuzzard", "Q36161", "reject"), - crossref_comment(101, "Q36161", plus=1)], - reactions={101: [reaction("kbuzzard", "+1", LATER)]}, - issue_comments=[AUTHOR_REJECTS_SET]) - self.assertEqual(self.verdict(r), ("recycle", "objection (reject/revise)")) - - def test_the_author_s_reject_never_drops_another_maintainer_s_objection(self): - # A listed maintainer's written approve comes after the author's reject, but - # another maintainer objects too: a listed one by ๐Ÿ‘Ž, a listed MEMBER in writing - # before the author, or a collaborator by ๐Ÿ‘Ž. Each recycles, as it does when the - # author never rejected. + def test_any_maintainer_s_objection_recycles_whatever_the_author_says(self): + # A listed maintainer's written approve, but another maintainer objects: a listed + # one by ๐Ÿ‘Ž, a listed MEMBER in writing earlier, or a collaborator by ๐Ÿ‘Ž. approve_after = written_verdict("jcommelin", "Q36161", "approve") shapes = { "listed ๐Ÿ‘Ž later": dict( @@ -158,27 +138,14 @@ def test_the_author_s_reject_never_drops_another_maintainer_s_objection(self): issue_comments=[AUTHOR_REJECTS_SET] if author_rejects else []) self.assertEqual(self.verdict(r), ("recycle", "maintainer rejected/revised")) - def test_an_author_with_an_org_role_keeps_a_maintainer_s_objection(self): - # Unchanged: if GitHub shows the author as a collaborator, their reject is a - # maintainer's, and not even a listed maintainer's later written approve lifts it. + def test_an_author_with_an_org_role_is_a_maintainer_like_anyone_else(self): + # If GitHub shows the author as a collaborator, their reject is a maintainer's, + # and one maintainer's objection recycles the tag whoever approves it. r = self.classify(reviews=[review(AUTHOR, assoc="COLLABORATOR")], comments=[written_verdict("jcommelin", "Q36161", "approve")], issue_comments=[AUTHOR_REJECTS_SET]) self.assertEqual(self.verdict(r), ("recycle", "maintainer rejected/revised")) - def test_an_association_only_maintainer_does_not_override_the_author(self): - r = self.classify(reviews=[review("SnirBroshi", assoc="COLLABORATOR")], - comments=[written_verdict("SnirBroshi", "Q36161", "approve", at=LATER, - assoc="COLLABORATOR")], - issue_comments=[AUTHOR_REJECTS_SET]) - self.assertEqual(self.verdict(r), ("recycle", "objection (reject/revise)")) - - def test_the_author_retracting_lifts_the_objection(self): - r = self.classify(comments=[crossref_comment(101, "Q36161", plus=1)], - reactions={101: [reaction(AUTHOR, "+1", LATER)]}, - issue_comments=[AUTHOR_REJECTS_SET]) - self.assertEqual(self.verdict(r), ("green", "approved (>=1 review, no objection)")) - def test_a_private_listed_maintainer_s_reject_beats_a_collaborator_s_thumbs_up(self): # grunweg's org membership is private, so GitHub shows CONTRIBUTOR and the # members probe 404s; only the list makes the reject a maintainer's. @@ -189,9 +156,9 @@ def test_a_private_listed_maintainer_s_reject_beats_a_collaborator_s_thumbs_up(s self.assertEqual(self.verdict(r), ("recycle", "maintainer rejected/revised")) self.assertEqual(r["maintainer_reviewers"], ["SnirBroshi", "grunweg"]) - def test_a_collaborator_s_thumbs_up_still_overrides_a_non_author_s_reject(self): - # Unchanged: an association-only maintainer trumps everyone but the PR author, - # and the gate still opens on the author plus that collaborator. + def test_a_collaborator_s_thumbs_up_overrides_a_reject_and_opens_the_gate_with_the_author(self): + # Unchanged: an association-only maintainer trumps every non-maintainer, and the + # gate still opens on the author plus that collaborator. r = self.classify(reviews=[review("SnirBroshi", assoc="COLLABORATOR")], comments=[crossref_comment(101, "Q36161", plus=1), written_verdict("someone", "Q36161", "reject")], @@ -222,11 +189,14 @@ def test_listed_maintainers_count_whatever_the_association(self): class Pr42608ReplayTest(PollFixture): - def test_set_and_partial_order_recycle_and_the_rest_stay_green(self): + def test_every_tag_stays_green(self): # mathlib4#42608's verdict shape: a Mathlib reviewer (association COLLABORATOR) # approved three tags (as ๐Ÿ‘ here) before the author's pasted WikiLean review, - # which approved seven and rejected Set and PartialOrder. - approved = ["Q166154", "Q994399", "Q124247109", "Q24743362", "Q332791", "Q1474074", "Q1070472"] + # which approved seven and rejected Set and PartialOrder. The reviewer's ๐Ÿ‘ is a + # maintainer's verdict, so it beats the author's rejects. + tags = ["Q166154", "Q994399", "Q124247109", "Q24743362", "Q332791", "Q36161", "Q474715", + "Q1474074", "Q1070472"] + approved = [q for q in tags if q not in ("Q36161", "Q474715")] thumbs = {"Q24743362": 101, "Q36161": 102, "Q474715": 103} r = self.run_with(FakeGh( diff=DIFF_42608, @@ -237,12 +207,11 @@ def test_set_and_partial_order_recycle_and_the_rest_stay_green(self): "Q36161": "reject", "Q474715": "reject"})]), settle.classify, PR, REPO) self.assertTrue(r["gate"]) # the gate is unchanged: author + a collaborator - self.assertEqual([g["qid"] for g in r["green"]], approved) - self.assertEqual([(t["qid"], t["reason"]) for t in r["recycle"]], - [("Q36161", "objection (reject/revise)"), ("Q474715", "objection (reject/revise)")]) + self.assertEqual([g["qid"] for g in r["green"]], tags) + self.assertEqual(r["recycle"], []) h = settle.ready_header(r) - self.assertIn("**7** `@[wikidata]` tags", h) - self.assertIn("2 recycled to the next batch.", h) + self.assertIn("**9** `@[wikidata]` tags", h) + self.assertNotIn("recycled", h) class ConflictRebuildTest(PollFixture):