[Deicyde]

Draft. The policy question is settled: the PR author gets no special privileges. Their verdict counts like any other reviewer's, and a maintainer's verdict beats it, as on main. What's left is the full maintainer list and a conflict-rebuild fix. The per-tag rule and the gate are unchanged.

Problem

On main, two defects in bot/settle.py and bot/poll.py:

• Most maintainers are not recognised. 16 of the 28 Mathlib maintainers keep their org membership private. GitHub shows them as CONTRIBUTOR and the members probe returns 404. Main's list seeds only jcommelin and faenuccio, so faenuccio is the only one of those 16 that counts. A private maintainer's reject loses to a collaborator's 👍.
• A conflict rebuild drops recycled tags. resolve_conflicts rebuilt from classify().green. A tag that recycles while the gate is closed was dropped in the force-push, with no triage and no trim comment.

Change

• MAINTAINERS is now the Mathlib maintainers team.
  • 28 logins from data/teams.yaml in leanprover-community/leanprover-community.github.io at 5b8381a4, each checked with gh api users/<login>.
  • The list is added to the association and org-probe check; it does not replace it.
  • settle.is_maintainer() matches logins case-insensitively. settle.py, pr_table.py's maintainer mark and harvest_corrections.py's is_maintainer flag all use it.
• A conflict rebuild keeps every tag on the PR. It re-applies every tag in the diff (set(cls["tags"])), and trimming stays with the settle. The "green tags" wording in poll.py and bot/README.md, and the rebuild's variable names, now match.
• The ready header (settle.ready_header, posted on mathlib4) names "a Mathlib maintainer listed in the bot" instead of `jcommelin`, `faenuccio`. It still @-mentions no one.
• Docs: bot/README.md's gate description points to the list instead of naming two logins.

Unchanged:

• The per-tag rule. A maintainer's verdict trumps, whether it is written or a 👍/👎 and whenever it was given. Otherwise any reject/revise/flag recycles the tag, and at least one approve makes it green.
• The gate. At least 2 people with a recorded verdict, the author included, at least 1 of them a maintainer.
• No author special case. On #42608, a Mathlib reviewer (association COLLABORATOR) 👍'd Set and PartialOrder, and that beats the author's later written rejects, so both stay green.

Effect on mathlib4#42608

Checked read-only with this branch's settle.py: the gate reads open (Deicyde and SnirBroshi), 9 of 9 tags are green and nothing recycles, the same as main. #40682, the batch Mathlib merged, reads 19 of 19 green.

#42608 is already settled and still conflicting. The first acting tick once the poller is back is therefore a conflict rebuild, on main and on this branch alike:

• resolve_conflicts force-pushes all 9 tags onto fresh master.
• It reposts the tag table without --header (bot/poll.py:198), so pr_table.py's default first line replaces the ready header.

Nothing deploys on merge. The change takes effect on the first poller tick once the poller is back, which needs #48's bootstrap_state dispatch and the token rotation.

How tested

bot/test_settle_gate.py (11 tests, stubbed gh, fixtures shared with bot/test_poll.py) is wired into scripts/ci-python.sh:

Scenario	Result
A maintainer's approve against the author's reject: a collaborator's earlier 👍, a listed maintainer's later 👍, a listed maintainer's earlier written approve, a collaborator's later written approve	green
A listed maintainer's reaction	no org-membership probe
A maintainer's written approve, then the author's reject, then the maintainer's 👎	recycled, with or without a blanket approval
A listed maintainer's written approve, in a different login case or with private membership	green
A listed maintainer's approve plus another maintainer's objection (a listed maintainer's 👎, a listed member's earlier written reject, or a collaborator's 👎), with or without the author's reject	recycled
An author GitHub shows as a collaborator rejects, and a listed maintainer approves	recycled: one maintainer's objection, as for anyone
A private-membership listed maintainer's reject against a collaborator's 👍	recycled (main: green)
A collaborator's 👍 against a non-maintainer's reject	green, and the gate opens with the author plus that collaborator
Listed maintainers count whatever the association; 28 logins; case-insensitive	pinned
Replay of #42608's verdicts	gate open, 9 green, nothing recycled
Conflict rebuild with the gate closed	both tags kept on the PR

• bot/test_poll.py: FakeGh serves reactions. The header and rebuild-log assertions follow the new wording.
• python3 bot/settle.py 42608 and python3 bot/settle.py 40682 (read-only) give the results under "Effect on mathlib4#42608".
• CI run 39069431818 at 32c4436: bot/test_settle_gate.py ran 11 tests and bot/test_poll.py 43, all passing, and required is green. They were not run locally because of machine load.

Risks

• The maintainer list is a snapshot. Update MAINTAINERS when the team changes. An unlisted maintainer still counts if GitHub shows them as a mathlib4 owner, member or collaborator.
• The first acting tick on #42608 is public: a force-pushed conflict rebuild that replaces the ready header with the default line. Main does the same.
• A later bare note lifts an earlier objection. Latest-wins applies to every reviewer, as on main.

History

• First draft: a stricter rule. The PR author never counted toward the gate, only MAINTAINERS counted as maintainer, and the association check and org probe were removed. Declined.
• Next rework: the PR author's reject stood unless a listed maintainer wrote a verdict on the tag after it.
• 32c4436: that carve-out is dropped, because the PR author gets no special privileges.

The commits before 32c4436 describe those earlier rules, so squash-merge this PR or rewrite the merge message. The maintainer list, is_maintainer(), the rebuild of every tag and the test fixtures carry over from the earlier versions.

🤖 Generated with Claude Code

[Deicyde]

Ready after the maintainer's rule choice and three small fixes; still a draft (re-reviewed at f4f1b639). The code is correct: the 28 listed logins sit on top of association detection, the gate is unchanged, and the first review's thumbs-down bug is fixed. First, rewrite "Effect on mathlib4#42608": tick 1 pushes a fast-forward trim commit and updates the ready header, and tick 2 force-pushes the conflict rebuild, whose table repost drops that header (bot/poll.py:198). Second, add the option "the author's reject is final"; across all 7 batches it differs from the carve-out only on #40682's Q213363. Add a Risks bullet as well: re-pasting a Copy review re-dates old rejects and can revoke a maintainer's later written override. Third, add a test for the w[0] == real[u] guard at bot/settle.py:277, whose removal no current test catches. Decision for the maintainer: the carve-out as built (recommended, a close call) or "final". Under either rule, the first tick trims Set and PartialOrder from #42608 unless they are re-approved first. Merge before the bootstrap_state dispatch and the MATHLIB_FORK_PAT rotation; release-neutral.

Posted by the WikiLean PR swarm (lead); updated 2026-10-17.

[Deicyde]

Status review (2026-10-14): ⏸ Hold (draft); one confirmed regression

The author exclusion, the explicit maintainer list, the rebuild-all-tags change and the header all hold up. The exception this PR adds has a bug, which needs fixing before the six policy decisions in the body matter.

Fix

• A maintainer's 👎 can become a green. In bot/settle.py:245, when the author has objected in writing, a maintainer's latest reaction is swapped for their older written verdict, even when that reaction is a 👎 that agrees with the author. Example: the maintainer writes approve, the author writes reject, then the maintainer reacts 👎. The result is mver=['approve'], so the tag goes GREEN as "maintainer approved", and the public header on mathlib4 counts it as an approved tag with no unresolved objection (as reviewer-approved if another reviewer has given a blanket GitHub approval). Substitute the written verdict only when the dropped reaction is not an objection, and add the opposite-meaning test.

Nits

• The PR body says #42608's ready comment "stays as it is". The pending conflict rebuild (poll.py:199, pr_table.py --post --no-body-sync with no --header) rewrites that comment's header on the first working tick, so decision 6's hand edit is mostly unnecessary.
• Stale "green tags" wording. bot/README.md:247 and the comments at poll.py:158 and :194 still say the conflict rebuild re-applies "the green tags" or "the green set". It now re-applies every tag on the PR.

Order: #48, then #51, then this PR; retarget the base as each lands. It conflicts with #61 in scripts/ci-python.sh; keep both run_check lines. It takes effect on the first poller tick after it reaches main, and only once #48's token rotation is done.

---

_{🤖 Automated status pass by Claude Code over all 18 open PRs (#46–#63), posted for the repo owner. An independent verifier re-checked each finding. All 18 heads were also merged and tested together in a scratch tree; the only test failure that comes from combining them is #47 × #55 (three other pairs had mechanical text conflicts). Reviewed head: 2d1e67f7.}

[Deicyde]

Recommendation: merge; take it out of draft first (at 32c4436d, CI green). Per the maintainer's decision of no author privilege, 32c4436d drops the author carve-out with its header sentence, README line, docstring and tests, including the guard test. The per-tag rule and the gate are main's again. What stays: the 28 listed Mathlib maintainers, matched case-insensitively, and the conflict rebuild that keeps every tag on the PR. The pr_table.py docstring now matches that rebuild. On mathlib4#42608 the gate reads open and all 9 tags green, as on main, so this no longer has to land before the poller restarts; merge it before the next batch PR settles, so the listed maintainers count. Optional: squash-merge, so the declined stricter-gate commits stay out of main's history. Release-neutral.

Posted by the WikiLean PR swarm (lead); updated 2026-10-17.

[Deicyde]

Updated verdict at 32c4436d: ready once it leaves draft. The owner decided the PR author gets no special privileges, so 32c4436d drops the author carve-out. A maintainer's verdict beats the author's again, as on main. The gate is unchanged.

• The guard test, the re-paste side effect and the force-push timing in my earlier verdict (below) applied only to the carve-out. With it gone, none of them applies.
• On the current branch, #42608 reads gate open with 9 of 9 green, the same as main. Its first acting tick is main's conflict rebuild.
• CI is green (run 39069431818). bot/test_settle_gate.py ran 11 tests and bot/test_poll.py 43.
• Still to do: squash-merge, or rewrite the merge message. The commits before 32c4436d describe rules that were dropped.
• The pr_table.py docstring is fixed.

Earlier verdict at f4f1b63 (carve-out design)

Verdict: the code is sound, and the decision is yours. 7e4a7681 closes the 👎 bug: no sequence I tried greens a tag that a maintainer currently objects to. I tried reactions, written verdicts, two maintainers, ties (the comparison is a strict >), notes, blanket approvals and differences in login case. The code implements choices (a) to (c) as the body describes. The branch merges cleanly with current main, and bot/test_settle_gate.py already has a run_check line, so the new coverage check passes. I reviewed by reading; machine load kept me from running the tests.

• Add one test before merge. No test covers the "still holds it" guard (w[0] == real[u], bot/settle.py:277). The case: the author rejects a tag, a listed maintainer writes (reject) on it later, then 👍s the crossref comment. Under choice (a) the tag recycles. With the guard deleted it goes green as "maintainer approved", and none of the 17 tests has that shape. Update: dd23e9e6 adds this test (a written reject at 08-25, then a 👍 at 08-30, expects recycle), and it would catch the guard's removal.
• A new side effect for you to weigh: re-pasting a review revokes a maintainer's override.
  • The review tool's Copy re-emits every stored decision and never clears one. Only Submit drops what it posted (wiki/src/review.ts:1967-2016, 2096).
  • Settle dates a pasted verdict by the comment's created_at.
  • So: you reject Set, then a listed maintainer writes an approve (green). Later you paste a review of another tag from the same browser. Set's reject comes back with a newer timestamp, so Set recycles, and on a settled PR the re-settle trims it.
  • On main a maintainer's approve wins whenever it was given, so this behavior is new.
• The body's "Effect on mathlib4#42608" is wrong about the force-push.
  • The first tick does not force-push. The re-settle runs split.py, whose upstream merge aborts on #42608's conflict (mergeable_state: dirty today), and then pushes a fast-forward commit (split.py:167-209).
  • The next tick takes resolve_conflicts. That force-pushes and reposts the table without --header (poll.py:198), so the new ready header lasts one tick before pr_table.py's default first line replaces it.
  • The force-push in the Risks section belongs to that second tick.
• Merge method: squash, or rewrite the message. Main uses merge commits, and the pre-rework commits (eb9fe24b, 2d1e67f7) describe the declined stricter rule, for example "the author never counts toward the gate".
• Minor:
  • bot/pr_table.py:89-92 still says the conflict rebuild shrinks the diff.
  • The README rule (lines 32-33) doesn't say the override must still be held, or that nothing overrides an author with an org role.
  • Editing a pasted review keeps the comment's original created_at, as on main.

[Deicyde]

Re-review on main (eaa5950b): follow-up needed (tests only). The code is right; no revert.

The merged code implements the owner's policy exactly. No author lookup remains in settle.py, poll.py, pr_table.py, harvest_corrections.py or daily_bot.py, so any maintainer's latest verdict beats the author's, whenever and however it was given. The gate still counts the author. The 28 MAINTAINERS logins match teams.yaml at 5b8381a4, which is still the latest commit there. Read-only replays on main still give #42608 9/9 green with the gate open, and #40682 19/19 green. 22 adversarial inputs found no author advantage.

• Follow-up: the tests can't catch author privilege coming back.
  • My rework (32c4436d) removed "user": {"login": "Deicyde"} from the shared pull() fixture (bot/test_poll.py:39-42), so the fake PR has no author.
  • Replaying the declined carve-out against main's fixture fails 0 assertions. With user restored it fails 6, and main's code still passes.
  • Two other forms of author privilege pass either way, because no test has these inputs:
    • the author's approve beating a non-maintainer's reject;
    • the author standing in for the maintainer in the gate.
  • Fix: restore user in pull(), and add "author approves + non-maintainer rejects → recycle" and "author + non-maintainer, no maintainer → gate closed".
• Noted, not fixable without rewriting main: this merged as a plain merge commit, so the declined drafts' commits sit in main's history describing rules the code no longer has (for example b0a5788a, "the author never counts toward the gate").
• Plausible, all predating this PR, your call:
  • A bare note counts toward the gate (settle.py:202 adds note-only reviewers), and a maintainer's later bare note erases their own earlier verdict.
  • The table's * marks only listed logins, not association-recognised maintainers. SnirBroshi decides two #42608 tags without a star; cls["maintainer_reviewers"] would fix that.
  • A later COMMENTED review, such as a thread reply, cancels that person's blanket approval.