Settle rule: recognise all 28 Mathlib maintainers; keep every tag in a conflict rebuild

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`).
@@ -241,14 +242,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.
 

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}}

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"]}
-    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")
+    # 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.
+    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
@@ -175,27 +176,27 @@ 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",
         "--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)
-    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):

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)
 
@@ -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

bot/settle.py

@@ -15,19 +15,34 @@
 """
 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/<login>`).
+# 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. 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)
 BOTS = {"github-actions[bot]"}
 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 +103,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)
@@ -172,10 +187,12 @@ 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
+    # 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)
@@ -211,7 +228,7 @@ 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", ""))
     for c in gh_list(repo, f"issues/{pr}/comments"):
@@ -239,7 +256,7 @@ 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)]
         if mver:
             if any(s in OBJECT for s in mver):
                 return "recycle", ex, "maintainer rejected/revised"
@@ -270,7 +287,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 +309,9 @@ 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. "
             f"Reviews recorded from: {who}. **Ready for a maintainer's review.**"
             + (f" {len(recycle)} recycled to the next batch." if recycle else "")
             + " <!-- wikilean-bot-ready -->")

bot/test_poll.py

@@ -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,11 @@ 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.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