API rate limit exceeded for user ID 129911861

Stream: lean4 dev

[Markus Schmaus]

The Mathlib CI for lean#4500 has now failed twice due to an API rate limit on GitHub.

This is a 'lean-pr-testing-4500' branch, so we need to adjust labels and write a comment.
Removing label awaiting-mathlib
{
  "message": "API rate limit exceeded for user ID 129911861. If you reach out to GitHub Support for help, please include the request ID AEAE:2C4C71:14589EC:26430D0:6672EE71 and timestamp 2024-06-19 14:42:57 UTC.",
  "documentation_url": "https://docs.github.com/rest/overview/rate-limits-for-the-rest-api",
  "status": "403"
}
Removing label breaks-mathlib
{
  "message": "API rate limit exceeded for user ID 129911861. If you reach out to GitHub Support for help, please include the request ID AEB8:2F7584:14C2E21:2701355:6672EE71 and timestamp 2024-06-19 14:42:57 UTC.",
  "documentation_url": "https://docs.github.com/rest/overview/rate-limits-for-the-rest-api",
  "status": "403"
}
Adding label builds-mathlib
{
  "message": "API rate limit exceeded for user ID 129911861. If you reach out to GitHub Support for help, please include the request ID AEBA:2F5EB1:14C02EE:27027DE:6672EE71 and timestamp 2024-06-19 14:42:57 UTC.",
  "documentation_url": "https://docs.github.com/rest/overview/rate-limits-for-the-rest-api",
  "status": "403"
}
jq: error (at <stdin>:5): Cannot index string with string "body"

Is this a known issue? Is there something I can do to fix this?

[Kim Morrison]

I encountered the same thing yesterday, so I guess it is known but new, and as yet unsolved. Suggestions welcome!

[Markus Schmaus]

The user ID points, as expected to leanprover-community-mathlib4-bot (https://api.github.com/user/129911861). It's hard to come up with suggestions without access to the bots code.

[Eric Wieser]

The obvious suggestion is to have a designated bot for lean4 CI, separate from the community bot; but maybe 90% of the rate limit is used up by the lean4 CI stuff anyway, in which case that won't help much

[Kim Morrison]

The code is all in Mathlib, in .github/workflows (sometimes calling scripts from scripts). This one is called running from - name: Post comments for lean-pr-testing branch in build.yml.

[Markus Schmaus]

The error happened three times after being triggered by a commit. I restarted the job manually and it succeeded.