Zulip Chat Archive

Since a week or two the bit keeps posting new comments to lean PRs, e.g. https://github.com/leanprover/lean4/pull/5241.
I had a quick look but didn't see obvious changes to the comment posting script. Does anyone know what's going on?

Damiano Testa (Sep 03 2024 at 08:43):

I think that some tokens were recently updated/modified: could it be that now they are posting more reliably (and, as a consequence, excessively)?

Joachim Breitner (Sep 03 2024 at 08:48):

No, the script has provisions to check for an existing comment and only append to it if it finds one:
https://github.com/leanprover-community/mathlib4/blob/b191738f9875e429b3680fecf251652a03f77cee/scripts/lean-pr-testing-comments.sh#L71

Joachim Breitner (Sep 03 2024 at 08:49):

Ah, but maybe the bot name has changed? The line

| jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "leanprover-community-mathlib4-bot"))')

doesn’t match https://github.com/leanprover-community-bot

Joachim Breitner (Sep 03 2024 at 08:50):

It should probably check for both names, because the “no mathlib ci attempted” check is still done from the old name:
https://github.com/leanprover/lean4/pull/5207#issuecomment-2318398108
And the same code exists in the lean4 repo, and should also be updated, it seems:
https://github.com/leanprover/lean4/blob/b053403238c1e8fb3148634de13a0b96b80a6aa9/.github/workflows/pr-release.yml#L170

Damiano Testa (Sep 03 2024 at 08:53):

There seem to be two names for this bot: here (if you are in the "maintainers" group) is a similar issue, I think.

Damiano Testa (Sep 03 2024 at 08:54):

It refers to #14860 that had the bot make a modification and therefore the PR being labeled as new-contributor, since the bot was picked up. There also there was a mismatch between the "name" of the bot and what the script had.

Joachim Breitner (Sep 03 2024 at 12:20):

I don't have access to that thread. But this “edit by” clearly shows that there are now two separate bots involved.
Screenshot_20240903-141733.png

Should the lean4 repo maybe also use the ”new” bot, the one with the nice icon? Maybe just a matter of setting the right token (and adjusting the expected user names in the scripts)?

Joachim Breitner (Sep 26 2024 at 12:57):

We still get duplicate comments, @Kim Morrison .

Kim Morrison (Sep 27 2024 at 06:23):

Hopefully #17182

Joachim Breitner (Sep 27 2024 at 06:25):

Remember that the lean repo also posts to this comment, so if you change the bot name, rather than filter for either, then the lean4 workflow needs to use the same token as the mathlib workflow, and also needs to check for the new name.