a `please-shake` label?

Stream: mathlib4

[Kim Morrison]

I wonder if anyone would be interested in writing a bot which:

1. watches for PRs with a please-shake label.
2. does nothing unless that PR is building, except that the shake step of CI is failing
3. checks out the PR, runs lake exe shake --fix, and then tries a lake build again
4. if that succeeds, commit and push the changes, and remove the please-shake label
5. if that fails, post a comment to the PR saying "I attempted to run lake exe shake --fix, but it failed", with a link to the workflow, and remove the label.

If it worked well, perhaps we'd eventually just remove the label and have this run automatically.

[Ruben Van de Velde]

Theoretically yes, but shake has been pretty flaky recently. Probably you'd also want the bot to push even if shake still failed afterwards

[Kim Morrison]

Oh, no, we definitely can't do that. Too often shake --update is what is needed, and if you already push the result of shake --fix then the author will find it hard to recover.

[Edward van de Meent]

still, having these issues marked presumably might help improve shake?