[Deicyde]

Stacked on #48 (base claude/poller-fail-closed) so the two don't collide in bot/poll.py, bot/test_poll.py and scripts/ci-python.sh. Once #48 merges, retarget to main. This PR changes wording only: the settle rule itself is untouched.

Problem

When the settle gate opens, the bot posts a "ready" comment on the upstream mathlib4 PR saying the kept tags were "approved 🟢 by ≥2 reviewers (incl. a maintainer) — ready to merge" (bot/poll.py:82-85, bot/daily_bot.py:86-89). That is not the rule bot/settle.py applies:

• The PR author counts as a reviewer. The bot opens PRs under the operator's own account, and that account is one of the "≥2".
• Collaborators count as maintainers. "Maintainer" includes anyone with an OWNER/MEMBER/COLLABORATOR association on mathlib4, which covers Mathlib reviewers, as well as the two seeded maintainers.
• One approval keeps a tag. It can be the author's own or a single 👍 reaction, and a "maintainer" verdict overrides objections.

On leanprover-community/mathlib4#42608 this text went out over 9 tags, 6 of them approved only by the author.

Change

• New settle.ready_header(cls) builds the comment's first line from the rule as implemented:
  • a kept tag has at least one approval and no reject/revise/flag recorded by this bot that a maintainer's verdict did not override; GitHub "Request changes" reviews and free-text comments are not counted
  • one approval per tag suffices, and it can be the author's own or a single 👍 reaction
  • only a per-tag verdict or 👍/👎 from jcommelin, faenuccio or a user GitHub shows the bot as a mathlib4 owner/member/collaborator overrides the others; a GitHub PR approval never does
  • it lists the logins whose reviews were recorded, in code font without @, so the header adds no mentions (the tag table below it @-mentions reviewers, as before)
  • it ends "Ready for a maintainer's review" instead of "ready to merge"
• poll.py (do_settle) and daily_bot.py both use it. The HTML marker the table code looks for is unchanged.
• pr_table.py's default header is what remains after a conflict rebuild. It said the tags "were approved 🟢 in review"; it now says they are "the tags kept at its last settle".
• Docstrings follow the code. The settle.py rule docstring now states the real gate and drops the "≥24h since it opened" condition, which was never checked. The push_property.py docstring now says a merged tag "was approved for merge by a Mathlib maintainer (bors r+, or d+ delegation) after Mathlib CI".
• The property seed export stops claiming ≥2 reviewers. export_property_seed.py's docstring and the QuickStatements header it emits now say each merged tag was "merged after Mathlib review and CI", and that the rows include external (non-bot) PRs. Only the header comment line of the committed bot/data/property_seed_quickstatements.csv changes; the rows are not regenerated.
• "Ready-to-merge comment" is gone from the docs. bot/README.md, daily_bot.py, poll.py and ops/poll-once.sh now describe the tag table under a ready-for-maintainer-review header.

The draft rule change ("count real reviewers") is stacked on this PR and rewrites the same function, so this fix stands even if that one is declined.

How tested

• New ReadyHeaderTest in bot/test_poll.py checks the header's statements (including the narrowed objection and override wording), that it contains no @ mention, no "≥2 reviewers" and no "unresolved objection" claim, and that it keeps the marker. It also checks that do_settle posts exactly ready_header(cls).
• The full bot/test_poll.py, bot/test_state_branch.py and bot/test_triage.py pass locally.

Risks

• The text the bot posts on mathlib4 changes; the next settle comment uses it.
• It is longer and openly says that an author's own approval or a single reaction can keep a tag. That is the point.

What Jack must do

Nothing beyond review: no secrets, settings or operator steps.

[Deicyde]

Review status: merged in f3f5ddae; one follow-up remains

Update 2026-10-14 (re-checked at be2ceca1):

• Landed and verified (23f5518, 5e57b6b; unchanged on main): bot/settle.py:291-297 drops the "no unresolved objection" claim. It now says what the bot actually counts, notes that Request-changes reviews and free-text comments are not counted, and limits the override to per-tag verdicts or reactions from seeded or org-role maintainers ("a GitHub PR approval never does"). I checked this wording against classify().
• bot/test_poll.py:404-418 pins the new clauses, rejects "unresolved objection" and any user mention.
• bot/README.md:17-19, the seed export docstring and header, and the comments in daily_bot.py, poll.py and poll-once.sh no longer say "ready to merge" or ">=2 reviewers".
• Departure: the override sentence was narrowed instead of deleted. Reasonable, since it now matches the code.
• Still open: bot/settle.py:298 still says "recycled to the next batch", which is wrong for tags that triage cuts.
• Before pinging a maintainer, check that the live mathlib4#42608 table header has been replaced.

Original review (2026-10-14)

Independent adversarial review of fb78e775 (since rebased onto #48 without content changes; current head 8210b3e1): a defect reviewer with skeptics, a design reviewer with a devil's advocate, and an arbiter.

Verdict: right fix, but the new settle header still makes two promises the code doesn't keep, to the maintainers it asks for a review.

Required before merge

• In bot/settle.py ready_header() (lines 291-297), delete "and no unresolved objection" and the sentence saying one approval is enough and a maintainer's verdict overrides the others. classify() never reads Request-changes reviews or plain comments, a maintainer's GitHub Approve never overrides, and unseeded maintainers with private org membership get no override at all. Keep the disclosure that a tag's approval can be the author's own or a single 👍, say "removed from this PR" instead of "recycled to the next batch" (wrong for tags triage cuts), and update ReadyHeaderTest with assertNotIn checks for "overrides" and "objection".
• bot/README.md:18 still says "post a ready-to-merge comment". Docs should ship with the code they describe.

Decisions for the maintainer

• Approve the final header wording; it posts on mathlib4 at the next settle or re-settle.
• The live comment on mathlib4 PR 42608 still opens with the old "ready to merge" header: let the first conflict rebuild after the token rotation replace it, or hand-edit its first line now. Read it before pinging a maintainer either way.

Merge order: after #48 (merge commit), retarget to main by hand, then merge before MATHLIB_FORK_PAT is rotated; touches only bot/, so it is release-neutral.

Fixes are in progress; this comment will be updated.

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

[Deicyde]

Status review (2026-10-14): ✅ Ready (stacked on #48)

This is a wording-only change that fixes a real public overclaim on mathlib4#42608. The header is deterministic, adds no @-mentions and keeps the marker. The test checks the text and that do_settle posts exactly this header.

Nits / follow-ups

• The same overclaim still exists in three places: bot/export_property_seed.py:7 (docstring), :286 (the QuickStatements header it writes), and the committed bot/data/property_seed_quickstatements.csv:4, which says "each reviewed by >=2 humans incl. a maintainer". That CSV also includes "external" rows that never went through the bot gate. bot/README.md:18, bot/daily_bot.py:11 and bot/ops/poll-once.sh:10 still mention a "ready-to-merge comment".
• The header claims a wider override than the code grants. It says a Mathlib maintainer, or anyone GitHub lists as an owner, member or collaborator, overrides the others. The code grants that only to the seeded logins and to users whose association GitHub reports, so an unseeded maintainer with private org membership doesn't count. Usually that errs on the safe side (their approve can't keep a tag someone objected to), but their reject also loses to an approve from a counted maintainer or collaborator, the batch-6 pattern described at settle.py:18-22. The header also doesn't say who did the overriding. Settle rule: recognise all 28 Mathlib maintainers; keep every tag in a conflict rebuild #57 addresses both.

Order: after #48. Then retarget this PR's base to main by hand: head branches aren't auto-deleted, so GitHub won't retarget it.

#42608 still conflicts with master, so the first working poller tick after #48's rollout should rebuild it and repost its table with pr_table's default header: this PR's "kept at its last settle" wording if this PR has landed by then, main's "approved 🟢 in review" wording if not. Either way, the old "≥2 reviewers … ready to merge" line goes away.

---

_{🤖 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: 8210b3e1.}

[Deicyde]

Fixes pushed (2026-10-14)

This addresses, from the PR swarm's review, the two ready_header overclaims, the test and bot/README.md:18, and from the "Status review (2026-10-14)" comment, the override clause, the seed export's ≥2-reviewer claim and the "ready-to-merge comment" wording.

What changed

• ready_header(): "no unresolved objection" becomes "no reject/revise/flag recorded by this bot that a maintainer's verdict did not override"; it adds that "Request changes" reviews and free-text comments are not counted. (swarm, 23f55184)
• The override sentence is narrowed, not deleted: only a per-tag verdict or 👍/👎 from jcommelin, faenuccio or a mathlib4 owner, member or collaborator (as GitHub shows the bot) overrides; a PR approval never does. (both reviews, 23f55184)
• ReadyHeaderTest pins both clauses, asserts "unresolved objection" is gone and rejects any @-mention. (swarm, 23f55184)
• export_property_seed.py (docstring and emitted header) and line 4 of property_seed_quickstatements.csv now say "merged after Mathlib review and CI"; the CSV rows are not regenerated. (status review, 5e57b6b1)
• "Ready-to-merge comment" is reworded in bot/README.md, daily_bot.py, poll.py and ops/poll-once.sh. (both reviews, 5e57b6b1)

Verification

• bot/test_poll.py (43 tests), test_state_branch.py (18) and test_triage.py (1) pass; the new ReadyHeaderTest fails against the old settle.py.
• Ad-hoc classify() fixture runs (not committed) match the new wording (Request-changes reviews, free-text objections, PR approvals, per-tag overrides).
• CI on 5e57b6b1: all checks green (worker, python, browser, required).

Not changed / still open

• "N recycled to the next batch" is kept, since main's header already uses it.
• Naming who overrode is left to Settle rule: recognise all 28 Mathlib maintainers; keep every tag in a conflict rebuild #57.
• The ≥2-reviewer claim remains in docs/research/mathdb-unification-research.json; Docs: record the Brain activation and correct project status #53 rewords it in docs/wikidata_property_proposal.md.
• Owner decision: approve the final header wording, which posts on mathlib4 at the next settle.

Merge notes

• Make the wikidata poller fail closed #48 has merged; this PR now targets main. Settle rule: recognise all 28 Mathlib maintainers; keep every tag in a conflict rebuild #57 conflicts with it in settle.py and test_poll.py: after this merges, rebase Settle rule: recognise all 28 Mathlib maintainers; keep every tag in a conflict rebuild #57 and retarget it to main.

---

_{🤖 Posted by Claude Code for the repo owner. Each fix was checked by an independent verifier before it was pushed. Head: 5e57b6b1.}