Stream: coqbot devs & users

Topic: ✔ Issue with coqbot not closing stale PRs today, etc.

Théo Zimmermann (Aug 25 2021 at 17:38):

Hey @Pierre-Marie Pédrot, you said that coqbot acted on too many PRs today. I suppose you were the one to trigger it and you triggered it only once. But did it actually mark more than ten PRs as stale? Or did it just say that it would close many many PRs (you didn't put any limitation on the latter).

Pierre-Marie Pédrot (Aug 25 2021 at 17:41):

I did not trigger it myself in any case.

Pierre-Marie Pédrot (Aug 25 2021 at 17:41):

but I did see a lot of notifications on modified PRs

Pierre-Marie Pédrot (Aug 25 2021 at 17:42):

mechanically this couldn't have been more than 20 (10 stale labels + 10 closures) but I think it was more in the ~30 range, and most of them were not closures anyways

Théo Zimmermann (Aug 25 2021 at 17:43):

Then the question is who triggered it (since it wasn't me and the PR to automatically trigger it every day hasn't been merged yet).

Théo Zimmermann (Aug 25 2021 at 17:47):

If someone triggers it several times, then there is nothing that prevents it to mark more than 10 PRs as stale.

Emilio Jesús Gallego Arias (Aug 25 2021 at 18:03):

I saw 50 PRs updated

Théo Zimmermann (Aug 25 2021 at 18:16):

Indeed, the logs show that someone triggered it twice in a row today.

Théo Zimmermann (Aug 25 2021 at 18:43):

OK so the reason why some PRs were not closed was because we have hit a secondary rate limit: https://docs.github.com/en/rest/overview/resources-in-the-rest-api#secondary-rate-limits

Théo Zimmermann (Aug 25 2021 at 18:46):

The solution seems to be to implement a throttle also for closing PRs and to lower the limit of PRs that can be touched in one triggering to coqbot.

Théo Zimmermann (Aug 25 2021 at 18:47):

And if needed, we could add a secret to be able to trigger the bot.

Enrico Tassi (Aug 26 2021 at 05:36):

How do you trigger it? I have no clue, I hope it cannot be done by misake

Théo Zimmermann (Aug 26 2021 at 09:44):

To trigger it, you need to do a specific curl request (see the PR adding a GitHub Action to trigger it every day).

Théo Zimmermann (Aug 26 2021 at 09:44):

I'd say it is impossible to do by mistake.

Pierre-Marie Pédrot (Aug 26 2021 at 09:59):

Who's been triggering it on a daily basis these days? I've not. Is that you @Théo Zimmermann ?

Théo Zimmermann (Aug 26 2021 at 10:00):

Yes, but only on days when I was not on vacations, i.e. not in the last few days.

Pierre-Marie Pédrot (Aug 26 2021 at 10:00):

Maybe Google or some bot accessed the URL while crawling?

Théo Zimmermann (Aug 26 2021 at 10:00):

You can't trigger it with a simple GET request, you need a POST request with coq:coq as the body.

Pierre-Marie Pédrot (Aug 26 2021 at 10:00):

Right.

Pierre-Marie Pédrot (Aug 26 2021 at 10:00):

The plot thickens.

Pierre-Marie Pédrot (Aug 26 2021 at 10:01):

You obviously don't have the IP of the client in the logs either?

Pierre-Marie Pédrot (Aug 26 2021 at 10:02):

Maybe some three-letter agency that thought that Coq was critical for their plans and things were not going as fast as possible...

Enrico Tassi (Aug 26 2021 at 10:03):

all your PRs are mine

Théo Zimmermann (Aug 26 2021 at 10:11):

Pierre-Marie Pédrot said:

You obviously don't have the IP of the client in the logs either?

Actually, I have. The request came from Mougins, Alpes-Maritimes. I guess that's Inria Sophia then.

Théo Zimmermann (Aug 26 2021 at 10:12):

Also, it started with a GET request (something that I had overlooked yesterday), which was therefore ill-formed.

Théo Zimmermann (Aug 26 2021 at 10:13):

It followed by a request to /favicon, which is a 404.

Théo Zimmermann (Aug 26 2021 at 10:13):

And only then a well-formed POST request.

Théo Zimmermann (Aug 26 2021 at 10:15):

And contrary to what I said earlier, there was only one POST request, so this doesn't explain why it marked more than 10 PRs as stale.

Théo Zimmermann (Aug 26 2021 at 10:29):

So what really happened is that the bot was triggered only once (which is OK then), but this had the following consequence:

• 10 PRs got marked as stale
• 38 PRs received a comment saying they were getting closed but only the first 4 were actually closed because GitHub has a really low rate limit for this kind of operation.

Théo Zimmermann (Aug 26 2021 at 12:16):

Fixed (limit is now at 6 new stale PRs and 4 closed PRs).

Notification Bot (Aug 26 2021 at 12:16):

Théo Zimmermann has marked this topic as resolved.

Enrico Tassi (Aug 26 2021 at 12:17):

Mugins could be me or Laurence. But are you saying this is a bug and the log entry you mentioned was somehting else?

Enrico Tassi (Aug 26 2021 at 12:18):

I could have clicked on any GH button by mistake, but I did not do a curl request for sure

Enrico Tassi (Aug 26 2021 at 12:18):

So, if there is a silly request from my IP address, there must be a link to it from GH. (I did re-run a few CI jobs for example using the bot links)

Théo Zimmermann (Aug 26 2021 at 12:22):

Enrico Tassi said:

Mugins could be me or Laurence. But are you saying this is a bug and the log entry you mentioned was somehting else?

I can give you the exact IP address if you want to check if it's yours.

Théo Zimmermann (Aug 26 2021 at 12:23):

Who is Laurence?

Enrico Tassi (Aug 26 2021 at 14:07):

Laurence Rideau, not runnig curl by hand either

Last updated: May 28 2023 at 18:29 UTC