[Merged by Bors] - ci: fix delegated reaction being triggered by bors failure message

[bryangingechen]

Follow-up to #29606.

The reaction script step was being skipped because bors was not counted as a bot: cf. log.

---

[github-actions]

PR summary 655a116e90

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[adomani]

Ah, good catch! Is the community-bot even needed or could we simply get away with just the bors-bot?

bors d+

[mathlib-bors]

✌️ bryangingechen can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[bryangingechen]

I just thought of an improvement we could make here, but maybe we should do this in another PR. The bors failure message should probably remove ready-to-merge as well. Unfortunately the conditionals here are quite hairy so we probably need to refactor things a bit first.

[bryangingechen]

I believe leanprover-community-mathlib4-bot and leanprover-community-bot-assistant are both needed there since they sometimes run bors r+ (the former for auto-merge-after-CI and the latter for the update nolints job).

[bryangingechen]

bors r+

[adomani]

I'm happy to err on the side of cautiousness and allowing both bots, but isn't author the bot that posted the Build failed: line? Wouldn't this be always the bors bot?

[bryangingechen]

Not sure if I understand your question, but the conditional I edited is a different one from the one that checks for "Build failed:". The one edited in this PR just sets the bot=true output.

[adomani]

With respect to removing the ready-to-merge label I'm a bit conflicted, as I find it useful to know that a failing PR had the label. Maybe we could replace the ready-to-merge label with a merge-failed label? That would convey both meanings: it was sent to bors and then something went wrong.

[adomani]

Not sure if I understand your question, but the conditional I edited is a different one from the one that checks for "Build failed:". The one edited in this PR just sets the bot=true output.

Ah, you're totally right! I got confused and I agree that my suggestion was wrong!

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• CI Success

[bryangingechen]

Maybe we could replace the ready-to-merge label with a merge-failed label? That would convey both meanings: it was sent to bors and then something went wrong.

That sounds reasonable, though do we need to then remove the label again when someone tries to merge? In any case, assuming the delegated reaction is now actually fixed, I'll probably take a break from this workflow for a bit.

To be honest the transitions between various labeled / unlabeled states are starting to confuse me; maybe adding another label to manage will feel less scary to me after I get some sleep.

[adomani]

I agree with leaving this for a bit.

Let's see how the new code works in the wild for a bit, before deciding what works, what doesn't and what can still be improved.